matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml

   1 <?xml version="1.0" encoding="UTF-8"?>
   2
   3 <page xmlns="http://lambdadelta.info/"
   4       description = "\lambda\delta home page"
   5       title = "\lambda\delta home page"
   6       head = "cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)"
   7 >
   8    <sitemap name="sitemap"/>
   9
  10    <section4 name="contents">Contents of the Specification</section4>
  11    <body>This specification comprises a collection of checked
  12          applications of λδ version 2.
  13          In particular it contains the components below.
  14    </body>
  15    <topitem name="MLTT1">
  16       <notice class="alpha" notice="MLTT1."/>
  17       Martin-Löf's Type Theory with one universe
  18       using λδ as theory of expressions.
  19    </topitem>
  20    <topitem name="functional">
  21       <notice class="alpha" notice="Functional."/>
  22       The validation algorithm for λδ as implemented in
  23       <rlink to="implementation.html#helena">Helena 0.8</rlink>.
  24    </topitem>
  25
  26    <section4 name="summary">Summary of the Specification</section4>
  27    <body>Here is a numerical account of the specification's contents
  28          and its timeline.
  29    </body>
  30    <table name="apps_2_sum"/>
  31    <news class="alpha" date="2012 February 24.">
  32          The Applications directory is started.
  33    </news>
  34    <news class="alpha" date="2011 December 20.">
  35          The Functional component is started
  36          inside the specification of λδ version 2.
  37    </news>
  38    <news class="alpha" date="2011 December 12.">
  39          The MLTT1 component is started.
  40    </news>
  41
  42    <section4 name="structure">Logical Structure of the Specification</section4>
  43    <body>This table reports the specification's components and their planes.
  44    </body>
  45    <table name="apps_2_src"/>
  46
  47    <footer/>
  48 </page>