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 = "applications of \lambda\delta version 2"
   5       title = "applications of \lambda\delta version 2"
   6       head = "cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)"
   7 >
   8    <section>Contents of the Specification</section>
   9    <body>This specification comprises a collection of checked
  10          applications of λδ version 2.
  11          In particular it contains the components below.
  12    </body>
  13    <news date="MLTT1.">
  14          Martin-Löf's Type Theory with one universe
  15          using λδ as theory of expressions.
  16    </news>
  17    <news date="Functional.">
  18          The validation algorithm for λδ as implemented in
  19          <rlink to="implementation.html#helena">Helena 0.8</rlink>.
  20    </news>
  21
  22    <section>Summary of the Specification</section>
  23    <body>Here is a numerical acount of the specification's contents
  24          and its timeline.
  25          Nodes are counted according to the "intrinsinc complexity measure"
  26          [F. Guidi: "Procedural Representation of CIC Proof Terms"
  27          Journal of Automated Reasoning 44(1-2), Springer (February 2010),
  28          pp. 53-78].
  29    </body>
  30    <table name="apps_2_sum"/>
  31    <news date="2012 February 24.">
  32          The Applications directory is started.
  33    </news>
  34    <news date="2011 December 20.">
  35          The Functional component is started
  36          inside the specification of λδ version 2.
  37    </news>
  38    <news date="2011 December 12.">
  39          The MLTT1 component is started.
  40    </news>
  41
  42    <section>Logical Structure of the Specification</section>
  43    <body>The source files are grouped in planes and components
  44          according to the following table.
  45          Each component contains its own notation file.
  46          The notation for the relations or functions introduced in each file
  47          is shown in parentheses (? are placeholders).
  48    </body>
  49    <table name="apps_2_src"/>
  50
  51    <section>Physical Structure of the Specification</section>
  52    <body>The source files are grouped in directories,
  53          one for each component.
  54    </body>
  55    <footer/>
  56 </page>