1 <?xml version="1.0" encoding="UTF-8"?>
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)"
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.
13 <topitem name="MLTT1">
14 <notice class="alpha" notice="MLTT1."/>
15 Martin-Löf's Type Theory with one universe
16 using λδ as theory of expressions.
18 <topitem name="functional">
19 <notice class="alpha" notice="Functional."/>
20 The validation algorithm for λδ as implemented in
21 <rlink to="implementation.html#helena">Helena 0.8</rlink>.
24 <section>Summary of the Specification</section>
25 <body>Here is a numerical acount of the specification's contents
28 <table name="apps_2_sum"/>
29 <news class="alpha" date="2012 February 24.">
30 The Applications directory is started.
32 <news class="alpha" date="2011 December 20.">
33 The Functional component is started
34 inside the specification of λδ version 2.
36 <news class="alpha" date="2011 December 12.">
37 The MLTT1 component is started.
40 <section>Logical Structure of the Specification</section>
41 <body>The source files are grouped in planes and components
42 according to the following table.
43 Each component contains its own notation file.
44 The notation for the relations or functions introduced in each file
45 is shown in parentheses (? are placeholders).
47 <table name="apps_2_src"/>