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       logo = "crux"
   7       head = "cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)"
   8 >
   9    <sitemap name="sitemap"/>
  10
  11    <section4 name="contents">Contents of the Specification</section4>
  12    <body>This specification comprises a collection of checked
  13          applications of λδ version 2.
  14          In particular it contains the components below.
  15    </body>
  16    <topitem name="models">
  17       <notice class="alpha" notice="Models."/>
  18       Denotational semantics for λδ.
  19    </topitem>
  20    <topitem name="MLTT1">
  21       <notice class="alpha" notice="MLTT1."/>
  22       Martin-Löf's Type Theory with one universe
  23       using λδ as theory of expressions.
  24    </topitem>
  25    <topitem name="functional">
  26       <notice class="alpha" notice="Functional."/>
  27       The validation algorithm for λδ as implemented in
  28       <rlink to="implementation.html#helena">Helena 0.8</rlink>.
  29    </topitem>
  30    <topitem name="examples">
  31       <notice class="alpha" notice="Examples."/>
  32       Terms of λδ with special features.
  33    </topitem>
  34
  35    <section4 name="summary">Summary of the Specification</section4>
  36    <body>Here is a numerical account of the specification's contents
  37          and its timeline.
  38    </body>
  39    <table name="apps_2_sum"/>
  40    <news class="alpha" date="2018 April 30.">
  41          The Models component is started for λδ version 2.
  42    </news>
  43    <news class="alpha" date="2017 March 6.">
  44          The Examples component is moved from the Core directory.
  45    </news>
  46    <news class="alpha" date="2012 February 24.">
  47          The Applications directory is started.
  48    </news>
  49    <news class="alpha" date="2011 December 20.">
  50          The Functional component is started
  51          inside the specification of λδ version 2.
  52    </news>
  53    <news class="alpha" date="2011 December 12.">
  54          The MLTT1 component is started.
  55    </news>
  56
  57    <section4 name="structure">Logical Structure of the Specification</section4>
  58    <body>This table reports the specification's components and their planes.
  59    </body>
  60    <table name="apps_2_src"/>
  61
  62    <footer/>
  63 </page>