1 <?xml version="1.0" encoding="UTF-8"?>
3 <page xmlns="http://lambdadelta.info/"
4 description = "\lambda\delta home page"
5 title = "\lambda\delta home page"
7 head = "cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)"
9 <sitemap name="sitemap"/>
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.
16 <topitem name="MLTT1">
17 <notice class="alpha" notice="MLTT1."/>
18 Martin-Löf's Type Theory with one universe
19 using λδ as theory of expressions.
21 <topitem name="functional">
22 <notice class="alpha" notice="Functional."/>
23 The validation algorithm for λδ as implemented in
24 <rlink to="implementation.html#helena">Helena 0.8</rlink>.
26 <topitem name="examples">
27 <notice class="alpha" notice="Examples."/>
28 Terms of λδ with special features.
31 <section4 name="summary">Summary of the Specification</section4>
32 <body>Here is a numerical account of the specification's contents
35 <table name="apps_2_sum"/>
36 <news class="alpha" date="2017 March 6.">
37 The Examples component is moved from the Core directory.
39 <news class="alpha" date="2012 February 24.">
40 The Applications directory is started.
42 <news class="alpha" date="2011 December 20.">
43 The Functional component is started
44 inside the specification of λδ version 2.
46 <news class="alpha" date="2011 December 12.">
47 The MLTT1 component is started.
50 <section4 name="structure">Logical Structure of the Specification</section4>
51 <body>This table reports the specification's components and their planes.
53 <table name="apps_2_src"/>