1 <?xml version="1.0" encoding="UTF-8"?>
2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
3 <html xmlns="http://www.w3.org/1999/xhtml" dir="ltr" lang="en-us">
5 <meta http-equiv="Content-Language" content="en-us" />
6 <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
7 <meta http-equiv="Content-Style-Type" content="text/css" />
8 <meta name="author" content="Ferruccio Guidi" />
9 <meta name="description" content="applications of lambdadelta version 2" />
10 <title>applications of lambdadelta version 2</title>
11 <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/ld_web.css" />
12 <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/lddl.css" />
13 <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/xhtbl.css" />
14 <link rel="shortcut icon" href="http://lambdadelta.info/images/crux_16.ico" />
18 <a href="http://lambdadelta.info/">
19 <img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
22 <div class="head1">cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)</div>
24 <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
26 <div xmlns:ld="http://lambdadelta.info/" class="head2">Contents of the Specification</div>
27 <div xmlns:ld="http://lambdadelta.info/" class="text">This specification comprises a collection of checked
28 applications of λδ version 2.
29 In particular it contains the components below.
31 <ul xmlns:ld="http://lambdadelta.info/">
33 <span class="date">MLTT1.</span>
34 Martin-Löf's Type Theory with one universe
35 using λδ as theory of expressions.
38 <ul xmlns:ld="http://lambdadelta.info/">
40 <span class="date">Functional.</span>
41 The validation algorithm for λδ as implemented in
42 <a href="http://lambdadelta.info/implementation.html#helena">Helena 0.8</a>.
46 <div xmlns:ld="http://lambdadelta.info/" class="head2">Summary of the Specification</div>
47 <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical acount of the specification's contents
50 <div xmlns:ld="http://lambdadelta.info/" class="text">
51 <table cellpadding="4" cellspacing="0">
54 <td class="snns component grey">category</td>
55 <td class="snns plane grey">objects</td>
56 <td class="snnn number grey">
59 <td class="snnn plane grey">
62 <td class="snnn number grey">
65 <td class="snnn plane grey">
68 <td class="ssnn number grey">
73 <td class="snns component cyan">sizes</td>
74 <td class="snns plane cyan">files</td>
75 <td class="snnn number cyan">5 </td>
76 <td class="snns plane cyan">characters</td>
77 <td class="snnn number cyan">5613</td>
78 <td class="snns plane cyan">nodes</td>
79 <td class="ssnn number cyan">9846</td>
82 <td class="snns component green">propositions</td>
83 <td class="snns plane green">theorems</td>
84 <td class="snnn number green">4</td>
85 <td class="snns plane green">lemmas</td>
86 <td class="snnn number green">1</td>
87 <td class="snns plane green">total</td>
88 <td class="ssnn number green">5</td>
91 <td class="snss component yellow">concepts</td>
92 <td class="snss plane yellow">declared</td>
93 <td class="snsn number yellow">3</td>
94 <td class="snss plane yellow">defined</td>
95 <td class="snsn number yellow">10</td>
96 <td class="snss plane yellow">total</td>
97 <td class="sssn number yellow">13</td>
102 <ul xmlns:ld="http://lambdadelta.info/">
104 <span class="date">2012 February 24.</span>
105 The Applications directory is started.
108 <ul xmlns:ld="http://lambdadelta.info/">
110 <span class="date">2011 December 20.</span>
111 The Functional component is started
112 inside the specification of λδ version 2.
115 <ul xmlns:ld="http://lambdadelta.info/">
117 <span class="date">2011 December 12.</span>
118 The MLTT1 component is started.
122 <div xmlns:ld="http://lambdadelta.info/" class="head2">Logical Structure of the Specification</div>
123 <div xmlns:ld="http://lambdadelta.info/" class="text">The source files are grouped in planes and components
124 according to the following table.
125 Each component contains its own notation file.
126 The notation for the relations or functions introduced in each file
127 is shown in parentheses (? are placeholders).
129 <div xmlns:ld="http://lambdadelta.info/" class="text">
130 <table cellpadding="4" cellspacing="0">
133 <td class="snns component grey">component</td>
134 <td class="snns plane grey">plane</td>
135 <td class="snns file grey">files</td>
136 <td class="ssnn file grey">
141 <td class="snns component yellow">MLTT1</td>
142 <td class="snns plane yellow" />
143 <td class="snns file yellow">genv_primitive</td>
144 <td class="ssnn file yellow">judgement</td>
147 <td class="snns component orange">functional</td>
148 <td class="snns plane orange">reduction and type machine</td>
149 <td class="snns file orange">rtm</td>
150 <td class="ssnn file orange">rtm_step ( ? ⇨ ? )</td>
153 <td class="nnns component orange">
156 <td class="snns plane orange">unfold</td>
157 <td class="snns file orange">lift ( ↑[?,?] ? )</td>
158 <td class="ssnn file orange">subst ( [?←?] ? )</td>
161 <td class="snss component red">examples</td>
162 <td class="snss plane red" />
163 <td class="snss file red" />
164 <td class="sssn file red">
172 <div xmlns:ld="http://lambdadelta.info/" class="head2">Physical Structure of the Specification</div>
173 <div xmlns:ld="http://lambdadelta.info/" class="text">The source files are grouped in directories,
174 one for each component.
177 <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
179 <div xmlns:ld="http://lambdadelta.info/" class="spacer">
182 <div xmlns:ld="http://lambdadelta.info/" class="spacer">
183 <a href="http://validator.w3.org/check?uri=referer">
184 <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
186 <a href="http://jigsaw.w3.org/css-validator/check/referer">
187 <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
189 <a href="http://www.w3.org/XML/">
190 <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
192 <a href="http://www.w3.org/Graphics/PNG/">
193 <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
195 <a href="http://www.anybrowser.org/campaign/">
196 <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
199 <div xmlns:ld="http://lambdadelta.info/" class="spacer">
202 <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 16 Apr 2013 21:51:34 +0200</div>