Skip to content

Commit

Permalink
deploy: 7367992
Browse files Browse the repository at this point in the history
  • Loading branch information
jonsterling committed Nov 17, 2024
1 parent adcaea6 commit 8b2456b
Show file tree
Hide file tree
Showing 2,165 changed files with 66,640 additions and 66,570 deletions.
16 changes: 8 additions & 8 deletions aagaard-sterling-birkedal-2023.xml
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ type="local">Jon Sterling</fr:link></fr:author><fr:author><fr:link
href="larsbirkedal.xml"
title="Lars Birkedal"
addr="larsbirkedal"
type="local">Lars Birkedal</fr:link></fr:author></fr:authors><fr:date><fr:year>2023</fr:year><fr:month>11</fr:month><fr:day>23</fr:day></fr:date><fr:anchor>12571</fr:anchor><fr:addr
type="local">Lars Birkedal</fr:link></fr:author></fr:authors><fr:date><fr:year>2023</fr:year><fr:month>11</fr:month><fr:day>23</fr:day></fr:date><fr:anchor>12572</fr:anchor><fr:addr
type="user">aagaard-sterling-birkedal-2023</fr:addr><fr:route>aagaard-sterling-birkedal-2023.xml</fr:route><fr:title
text="A denotationally-based program logic for higher-order store">A denotationally-based program logic for higher-order store</fr:title><fr:taxon>Reference</fr:taxon><fr:meta
name="doi">10.46298/entics.12232</fr:meta><fr:meta
Expand All @@ -26,7 +26,7 @@ type="local">recent discovery</fr:link> of simple denotational semantics for gen
display="inline"><![CDATA[\textbf {F}^{\mu ,\textit {ref}}]]></fr:tex>. The <fr:strong>Tulip</fr:strong> logic differs from operationally-based program logics in two ways: predicates range over the meanings of typed terms rather than over the raw code of untyped terms, and they are automatically invariant under the equational congruence of higher-order store, which applies even underneath a binder. As a result, “pure” proof steps that conventionally require focusing the Hoare triple on an operational redex are replaced by a simple equational rewrite in <fr:strong>Tulip</fr:strong>. We have evaluated <fr:strong>Tulip</fr:strong> against standard examples involving linked lists in the heap, comparing our abstract equational reasoning with more familiar operational-style reasoning. Our main result is the soundness of <fr:strong>Tulip</fr:strong>, which we establish by constructing a BI-hyperdoctrine over the denotational semantics of <fr:tex
display="inline"><![CDATA[\textbf {F}^{\mu ,\textit {ref}}]]></fr:tex> in an impredicative version of synthetic guarded domain theory.</fr:p></fr:mainmatter><fr:backmatter><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>12565</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>12566</fr:anchor><fr:title
text="References">References</fr:title></fr:frontmatter><fr:mainmatter><fr:tree
show-metadata="true"
expanded="false"
Expand All @@ -43,7 +43,7 @@ type="local">Daniel Gratzer</fr:link></fr:author><fr:author><fr:link
href="larsbirkedal.xml"
title="Lars Birkedal"
addr="larsbirkedal"
type="local">Lars Birkedal</fr:link></fr:author></fr:authors><fr:date><fr:year>2022</fr:year><fr:month>10</fr:month><fr:day>6</fr:day></fr:date><fr:anchor>12564</fr:anchor><fr:addr
type="local">Lars Birkedal</fr:link></fr:author></fr:authors><fr:date><fr:year>2022</fr:year><fr:month>10</fr:month><fr:day>6</fr:day></fr:date><fr:anchor>12565</fr:anchor><fr:addr
type="user">sterling-gratzer-birkedal-2022</fr:addr><fr:route>sterling-gratzer-birkedal-2022.xml</fr:route><fr:title
text="Denotational semantics of general store and polymorphism">Denotational semantics of general store and polymorphism</fr:title><fr:taxon>Reference</fr:taxon><fr:meta
name="doi">10.48550/arXiv.2210.02169</fr:meta><fr:meta
Expand All @@ -59,10 +59,10 @@ title="Paul Blain Levy"
addr="paulblainlevy"
type="local">Levy</fr:link>'s possible worlds model construction; what is new in relation to prior typed denotational models of higher-order store is that our Kripke worlds need not be syntactically definable, and are thus compatible with relational reasoning in the heap. Our work combines recent advances in the operational semantics of state with the purely denotational viewpoint of <fr:em>synthetic guarded domain theory</fr:em>.</fr:p></fr:mainmatter></fr:tree></fr:mainmatter></fr:tree><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>12566</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>12567</fr:anchor><fr:title
text="Context">Context</fr:title></fr:frontmatter><fr:mainmatter /></fr:tree><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>12568</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>12569</fr:anchor><fr:title
text="Backlinks">Backlinks</fr:title></fr:frontmatter><fr:mainmatter><fr:tree
show-metadata="true"
expanded="false"
Expand All @@ -71,7 +71,7 @@ numbered="false"><fr:frontmatter><fr:authors><fr:author><fr:link
href="jonmsterling.xml"
title="Jon Sterling"
addr="jonmsterling"
type="local">Jon Sterling</fr:link></fr:author></fr:authors><fr:date><fr:year>2023</fr:year><fr:month>8</fr:month><fr:day>15</fr:day></fr:date><fr:anchor>12567</fr:anchor><fr:addr
type="local">Jon Sterling</fr:link></fr:author></fr:authors><fr:date><fr:year>2023</fr:year><fr:month>8</fr:month><fr:day>15</fr:day></fr:date><fr:anchor>12568</fr:anchor><fr:addr
type="user">jms-0079</fr:addr><fr:route>jms-0079.xml</fr:route><fr:title
text="Equational higher-order separation logic for higher-order store">Equational higher-order separation logic for higher-order store</fr:title></fr:frontmatter><fr:mainmatter><fr:p>In collaboration with my colleagues <fr:link
href="flaagaard.xml"
Expand Down Expand Up @@ -103,8 +103,8 @@ title="A denotationally-based program logic for higher-order store"
addr="aagaard-sterling-birkedal-2023"
type="local">TULIP</fr:link> logic is a strong first step in this direction.</fr:p></fr:mainmatter></fr:tree></fr:mainmatter></fr:tree><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>12569</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>12570</fr:anchor><fr:title
text="Related">Related</fr:title></fr:frontmatter><fr:mainmatter /></fr:tree><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>12570</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>12571</fr:anchor><fr:title
text="Contributions">Contributions</fr:title></fr:frontmatter><fr:mainmatter /></fr:tree></fr:backmatter></fr:tree>
16 changes: 8 additions & 8 deletions abbes-2006.xml
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ root="false"><fr:frontmatter><fr:authors><fr:author><fr:link
href="samyabbes.xml"
title="Samy Abbes"
addr="samyabbes"
type="local">Samy Abbes</fr:link></fr:author></fr:authors><fr:date><fr:year>2006</fr:year><fr:month>1</fr:month><fr:day>1</fr:day></fr:date><fr:anchor>15482</fr:anchor><fr:addr
type="local">Samy Abbes</fr:link></fr:author></fr:authors><fr:date><fr:year>2006</fr:year><fr:month>1</fr:month><fr:day>1</fr:day></fr:date><fr:anchor>15474</fr:anchor><fr:addr
type="user">abbes-2006</fr:addr><fr:route>abbes-2006.xml</fr:route><fr:title
text="A Cartesian closed category of event structures with quotients">A Cartesian closed category of <fr:link
href="jms-00BN.xml"
Expand All @@ -22,13 +22,13 @@ type="local">event structures</fr:link>. The category obtained is cartesian clos
display="inline"><![CDATA[E]]></fr:tex> is a minimal event structure with the same space of maximal configurations as <fr:tex
display="inline"><![CDATA[E]]></fr:tex>.</fr:p></fr:mainmatter><fr:backmatter><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>15475</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>15467</fr:anchor><fr:title
text="References">References</fr:title></fr:frontmatter><fr:mainmatter /></fr:tree><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>15476</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>15468</fr:anchor><fr:title
text="Context">Context</fr:title></fr:frontmatter><fr:mainmatter /></fr:tree><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>15478</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>15470</fr:anchor><fr:title
text="Backlinks">Backlinks</fr:title></fr:frontmatter><fr:mainmatter><fr:tree
show-metadata="true"
expanded="false"
Expand All @@ -37,7 +37,7 @@ numbered="false"><fr:frontmatter><fr:authors><fr:author><fr:link
href="jonmsterling.xml"
title="Jon Sterling"
addr="jonmsterling"
type="local">Jon Sterling</fr:link></fr:author></fr:authors><fr:date><fr:year>2023</fr:year><fr:month>10</fr:month><fr:day>26</fr:day></fr:date><fr:anchor>15477</fr:anchor><fr:addr
type="local">Jon Sterling</fr:link></fr:author></fr:authors><fr:date><fr:year>2023</fr:year><fr:month>10</fr:month><fr:day>26</fr:day></fr:date><fr:anchor>15469</fr:anchor><fr:addr
type="user">jms-00BT</fr:addr><fr:route>jms-00BT.xml</fr:route><fr:title
text="Event structures and prime algebraic domains"><fr:link
href="jms-00BN.xml"
Expand All @@ -53,7 +53,7 @@ title="A Cartesian closed category of event structures with quotients"
addr="abbes-2006"
type="local">paper of Abbes</fr:link>.</fr:p></fr:mainmatter></fr:tree></fr:mainmatter></fr:tree><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>15480</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>15472</fr:anchor><fr:title
text="Related">Related</fr:title></fr:frontmatter><fr:mainmatter><fr:tree
show-metadata="true"
expanded="false"
Expand All @@ -62,7 +62,7 @@ numbered="false"><fr:frontmatter><fr:authors><fr:author><fr:link
href="jonmsterling.xml"
title="Jon Sterling"
addr="jonmsterling"
type="local">Jon Sterling</fr:link></fr:author></fr:authors><fr:date><fr:year>2023</fr:year><fr:month>10</fr:month><fr:day>26</fr:day></fr:date><fr:anchor>15479</fr:anchor><fr:addr
type="local">Jon Sterling</fr:link></fr:author></fr:authors><fr:date><fr:year>2023</fr:year><fr:month>10</fr:month><fr:day>26</fr:day></fr:date><fr:anchor>15471</fr:anchor><fr:addr
type="user">jms-00BN</fr:addr><fr:route>jms-00BN.xml</fr:route><fr:title
text="Event structure">Event structure</fr:title><fr:taxon>Definition</fr:taxon><fr:meta
name="source"><fr:link
Expand All @@ -84,5 +84,5 @@ display="inline"><![CDATA[e\leq e']]></fr:tex> with <fr:tex
display="inline"><![CDATA[e'\in x]]></fr:tex>, we have <fr:tex
display="inline"><![CDATA[x\cup {\mathopen {}\left \{e\right \}\mathclose {}}\in \mathsf {Con}_{E}]]></fr:tex>.</fr:li></fr:ol></fr:mainmatter></fr:tree></fr:mainmatter></fr:tree><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>15481</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>15473</fr:anchor><fr:title
text="Contributions">Contributions</fr:title></fr:frontmatter><fr:mainmatter /></fr:tree></fr:backmatter></fr:tree>
18 changes: 9 additions & 9 deletions abchfl-2021.xml
Original file line number Diff line number Diff line change
Expand Up @@ -26,21 +26,21 @@ type="local">Kuen-Bang Hou (Favonia)</fr:link></fr:author><fr:author><fr:link
href="danlicata.xml"
title="Daniel R. Licata"
addr="danlicata"
type="local">Daniel R. Licata</fr:link></fr:author></fr:authors><fr:date><fr:year>2021</fr:year><fr:month>4</fr:month><fr:day>1</fr:day></fr:date><fr:anchor>17890</fr:anchor><fr:addr
type="local">Daniel R. Licata</fr:link></fr:author></fr:authors><fr:date><fr:year>2021</fr:year><fr:month>4</fr:month><fr:day>1</fr:day></fr:date><fr:anchor>17891</fr:anchor><fr:addr
type="user">abchfl-2021</fr:addr><fr:route>abchfl-2021.xml</fr:route><fr:title
text="Syntax and models of Cartesian cubical type theory">Syntax and models of Cartesian cubical type theory</fr:title><fr:taxon>Reference</fr:taxon></fr:frontmatter><fr:mainmatter><fr:p>We present a cubical type theory based on the Cartesian cube category (faces, degeneracies, symmetries, diagonals, but no connections or reversal) with univalent universes, each containing <fr:tex
display="inline"><![CDATA[\Pi ]]></fr:tex>, <fr:tex
display="inline"><![CDATA[\Sigma ]]></fr:tex>, path, identity, natural number, boolean, suspension, and glue (equivalence extension) types. The type theory includes a syntactic description of a uniform Kan operation, along with judgmental equality rules defining the Kan operation on each type. The Kan operation uses both a different set of generating trivial cofibrations and a different set of generating cofibrations than the Cohen, Coquand, Huber, and Mörtberg (CCHM) model. Next, we describe a constructive model of this type theory in Cartesian cubical sets. We give a mechanized proof, using Agda as the internal language of cubical sets in the style introduced by Orton and Pitts, that glue, <fr:tex
display="inline"><![CDATA[\Pi ]]></fr:tex>, <fr:tex
display="inline"><![CDATA[\Sigma ]]></fr:tex>, path, identity, boolean, natural number, suspension types, and the universe itself are Kan in this model, and that the universe is univalent. An advantage of this formal approach is that our construction can also be interpreted in a range of other models, including cubical sets on the connections cube category and the De Morgan cube category, as used in the CCHM model, and bicubical sets, as used in directed type theory.</fr:p></fr:mainmatter><fr:backmatter><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>17884</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>17885</fr:anchor><fr:title
text="References">References</fr:title></fr:frontmatter><fr:mainmatter /></fr:tree><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>17885</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>17886</fr:anchor><fr:title
text="Context">Context</fr:title></fr:frontmatter><fr:mainmatter /></fr:tree><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>17887</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>17888</fr:anchor><fr:title
text="Backlinks">Backlinks</fr:title></fr:frontmatter><fr:mainmatter><fr:tree
show-metadata="true"
expanded="false"
Expand All @@ -49,7 +49,7 @@ numbered="false"><fr:frontmatter><fr:authors><fr:author><fr:link
href="jonmsterling.xml"
title="Jon Sterling"
addr="jonmsterling"
type="local">Jon Sterling</fr:link></fr:author></fr:authors><fr:date><fr:year>2023</fr:year><fr:month>1</fr:month><fr:day>19</fr:day></fr:date><fr:anchor>17886</fr:anchor><fr:addr
type="local">Jon Sterling</fr:link></fr:author></fr:authors><fr:date><fr:year>2023</fr:year><fr:month>1</fr:month><fr:day>19</fr:day></fr:date><fr:anchor>17887</fr:anchor><fr:addr
type="user">jms-000R</fr:addr><fr:route>jms-000R.xml</fr:route><fr:title
text="Background on homotopy and cubical type theory">Background on homotopy and cubical type theory</fr:title></fr:frontmatter><fr:mainmatter><fr:p>For more than four decades, dependent type theory has been positioned as the “common language” that can finally <fr:link
href="martin-loef-1982.xml"
Expand Down Expand Up @@ -101,15 +101,15 @@ href="cchm-2017.xml"
title="Cubical type theory: a constructive interpretation of the univalence axiom"
addr="cchm-2017"
type="local">theory</fr:link></fr:strong> that reorganizes the higher-dimensional structure discussed by considering all the points, lines, squares, cubes, hypercubes, and so-on that one can draw in a given type. The computational interpretation of the new cubical type theory can be split into two different conjectures:</fr:p><fr:tree
show-metadata="false"><fr:frontmatter><fr:authors /><fr:date><fr:year>2023</fr:year><fr:month>1</fr:month><fr:day>19</fr:day></fr:date><fr:anchor>7351</fr:anchor><fr:addr
show-metadata="false"><fr:frontmatter><fr:authors /><fr:date><fr:year>2023</fr:year><fr:month>1</fr:month><fr:day>19</fr:day></fr:date><fr:anchor>7352</fr:anchor><fr:addr
type="user">jms-000S</fr:addr><fr:route>jms-000S.xml</fr:route><fr:title
text="Cubical canonicity">Cubical canonicity</fr:title><fr:taxon>Conjecture</fr:taxon></fr:frontmatter><fr:mainmatter><fr:p>For any closed term <fr:tex
display="inline"><![CDATA[\cdot \vdash N:\mathsf {nat}]]></fr:tex> of cubical type theory, there exists a unique natural number <fr:tex
display="inline"><![CDATA[n\in \mathbb {N}]]></fr:tex> such that <fr:tex
display="inline"><![CDATA[\cdot \vdash N\equiv \bar {n}:\mathsf {nat}]]></fr:tex> where <fr:tex
display="inline"><![CDATA[\bar {n}]]></fr:tex> is the encoding of the number <fr:tex
display="inline"><![CDATA[n]]></fr:tex> as a term in the type theory.</fr:p></fr:mainmatter></fr:tree><fr:tree
show-metadata="false"><fr:frontmatter><fr:authors /><fr:date><fr:year>2023</fr:year><fr:month>1</fr:month><fr:day>19</fr:day></fr:date><fr:anchor>7352</fr:anchor><fr:addr
show-metadata="false"><fr:frontmatter><fr:authors /><fr:date><fr:year>2023</fr:year><fr:month>1</fr:month><fr:day>19</fr:day></fr:date><fr:anchor>7353</fr:anchor><fr:addr
type="user">jms-000T</fr:addr><fr:route>jms-000T.xml</fr:route><fr:title
text="Decidability of cubical type theory">Decidability of cubical type theory</fr:title><fr:taxon>Conjecture</fr:taxon></fr:frontmatter><fr:mainmatter><fr:p>The assertions <fr:tex
display="inline"><![CDATA[\Gamma \vdash {A}\ \textit {type}]]></fr:tex>, <fr:tex
Expand All @@ -133,8 +133,8 @@ title="Decidability of cubical type theory"
addr="jms-000T"
type="local">decidability conjecture</fr:link> is no less important, as it is a necessary ingredient to implement a <fr:em>typechecker</fr:em> or a <fr:em>compiler</fr:em> for a programming language based on cubical type theory.</fr:p></fr:mainmatter></fr:tree></fr:mainmatter></fr:tree><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>17888</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>17889</fr:anchor><fr:title
text="Related">Related</fr:title></fr:frontmatter><fr:mainmatter /></fr:tree><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>17889</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>17890</fr:anchor><fr:title
text="Contributions">Contributions</fr:title></fr:frontmatter><fr:mainmatter /></fr:tree></fr:backmatter></fr:tree>
14 changes: 7 additions & 7 deletions abigailpribisova.xml
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
<?xml-stylesheet type="text/xsl" href="default.xsl"?>
<fr:tree
xmlns:fr="http://www.jonmsterling.com/jms-005P.xml"
root="false"><fr:frontmatter><fr:authors /><fr:anchor>7962</fr:anchor><fr:addr
root="false"><fr:frontmatter><fr:authors /><fr:anchor>7934</fr:anchor><fr:addr
type="user">abigailpribisova</fr:addr><fr:route>abigailpribisova.xml</fr:route><fr:title
text="Abigail Pribisova">Abigail Pribisova</fr:title><fr:meta
name="position">MPhil Student</fr:meta><fr:meta
Expand All @@ -12,24 +12,24 @@ title="University of Cambridge"
addr="ucam"
type="local">University of Cambridge</fr:link></fr:meta></fr:frontmatter><fr:mainmatter /><fr:backmatter><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>7956</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>7928</fr:anchor><fr:title
text="References">References</fr:title></fr:frontmatter><fr:mainmatter /></fr:tree><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>7957</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>7929</fr:anchor><fr:title
text="Context">Context</fr:title></fr:frontmatter><fr:mainmatter /></fr:tree><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>7958</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>7930</fr:anchor><fr:title
text="Backlinks">Backlinks</fr:title></fr:frontmatter><fr:mainmatter /></fr:tree><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>7960</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>7932</fr:anchor><fr:title
text="Related">Related</fr:title></fr:frontmatter><fr:mainmatter><fr:tree
show-metadata="true"
expanded="false"
toc="false"
numbered="false"><fr:frontmatter><fr:authors /><fr:anchor>7959</fr:anchor><fr:addr
numbered="false"><fr:frontmatter><fr:authors /><fr:anchor>7931</fr:anchor><fr:addr
type="user">ucam</fr:addr><fr:route>ucam.xml</fr:route><fr:title
text="University of Cambridge">University of Cambridge</fr:title><fr:taxon>Institution</fr:taxon><fr:meta
name="external">https://www.cam.ac.uk/</fr:meta></fr:frontmatter><fr:mainmatter /></fr:tree></fr:mainmatter></fr:tree><fr:tree
show-metadata="false"
hidden-when-empty="true"><fr:frontmatter><fr:anchor>7961</fr:anchor><fr:title
hidden-when-empty="true"><fr:frontmatter><fr:anchor>7933</fr:anchor><fr:title
text="Contributions">Contributions</fr:title></fr:frontmatter><fr:mainmatter /></fr:tree></fr:backmatter></fr:tree>
Loading

0 comments on commit 8b2456b

Please sign in to comment.