| The HELM project [1/1] |
| Aims [1/2] [2/2] |
| Application Centric Architecture [1/3] [2/3] [3/3] |
| Content Centric Architecture [1/5] [2/5] [3/5] [4/5] [5/5] |
| General Overview [1/1] |
| The eXtensible Markup Language (XML) [1/4] [2/4] [3/4] [4/4] [example no. 1] [example no. 2] |
| Encoding CIC in XML: what must NOT be exported from Coq [1/4] [2/4] [3/4] [4/4] |
| Encoding CIC in XML: terms and objects [1/4] [2/4] [3/4] [4/4] |
| Encoding CIC in XML: an example of exported object [1/2] [2/2] |
| Encoding CIC in XML: theories [1/5] [2/5] [3/5] [4/5] [5/5] |
| Encoding CIC in XML: an example of theory [1/1] |
| Encoding CIC in XML: cooking and naming [1/5] [2/5] [3/5] [4/5] [5/5] [a cooking example] |
| A Type Checker for the exported files [1/5] [2/5] [3/5] [4/5] [5/5] [A strange behaviour of Coq] |
| eXtensible Stylesheet Language Transformations (XSLT) [1/5] [2/5] [3/5] [4/5] [5/5] [An example of XSLT rule] |
| The Mathematical Markup Language (MathML) [1/5] [2/5] [3/5] [4/5] [5/5] [An example of content markup] [An example of presentation markup] |
| General overview of the transformations [1/1] |
| The model of distribution [1/5] [2/5] [3/5] [4/5] [5/5] |
| Interfaces to the library [1/5] [2/5] [3/5] [4/5] [5/5] [A snapshot of our interface] |
| The exported Standard Library of Coq online |
![[A snapshot of our interface]](snapshot.jpg){kind=link}