1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
4 <meta content="text/html; charset=UTF-8" http-equiv="content-type">
5 <title>lambda_delta home page</title>
6 <meta content="Ferruccio Guidi" name="author">
7 <meta content="The formal system lambda_delta" name="description">
8 <link rel="shortcut icon" href="download/crux_16.ico">
11 <div style="text-align: center;">
13 <a href="http://lambda-delta.info"><img alt="[Crux Logo]"
14 title="The Crux" src="download/crux_32.png"
15 style="border: 0px solid ; width: 32px; height: 32px;"></a>
16 <h1>The Formal System λδ (lambda_delta)<br>
18 <h2>Towards the unification of terms, types, environments and contexts</h2>
19 <img style="width: 95%; height: 4px;" alt="[Separator]"
20 title="Separator" src="download/rainbow.png"><br>
22 style="text-align: left; width: 95%; margin-left: auto; margin-right: auto;"
23 border="0" cellpadding="2" cellspacing="20">
26 <td style="vertical-align: top;">
31 <li><a href="news.html">News</a></li>
34 <li><a href="documentation.html">Papers</a></li>
37 <li><a href="implementation.html">Resources</a><br>
41 <td style="vertical-align: top; text-align: left;">
42 <h3 style="text-align: right;">Foreword <img
43 style="width: 37px; height: 37px;" alt="[Butterfly]" title="Butterfly"
44 src="download/b9.png"></h3>
46 (lambda_delta) is a typed lambda calculus that pursues the static and
47 dynamic unification of terms, types, environments and contexts while
48 enjoying a well-conceived meta-theory, which includes the commonly
49 desired properties.<br>
51 λδ takes some features from the calculi of the Automath family and
52 some from the pure type systems, but it differs from both in that it
53 does not include the Π construction while it provides for an
54 abbreviation mechanism at the level of terms.<br>
56 λδ features explicit type annotations, which are borrowed from
57 realistic type checker implementations and with which type checking is
58 reduced to type inference.<br>
60 The reduction steps of λδ include β-contraction, δ-expansion,
61 ζ-contraction and θ-swap. On the other hand,
62 η-contraction is not included.<br>
64 The meta-theory of λδ includes important properties such as the
65 confluence of reduction, the correctness of types, the
66 uniqueness of types up to conversion, the subject reduction of the type
67 assignment, the strong normalization of the typed terms. The
68 decidability of type inference and of type checking come as corollaries.<br>
70 λδ features uniformly dependent types and a predicative abstraction
71 mechanism, so the calculus can serve as a formal specification language
72 for the type theories that need a predicative foundation. λδ is
73 expected to have the expressive power of λ→.<br>
75 λδ comes in several versions listed in the following table, which
76 includes the major milestones:<br>
78 <table style="text-align: left; width: 100%;" border="1"
79 cellpadding="2" cellspacing="0">
83 style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Version<br>
86 style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Name<br>
89 style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Started<br>
92 style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Released<br>
95 style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Dismissed<br>
100 style="vertical-align: top; background-color: rgb(255, 223, 191);">2<br>
103 style="vertical-align: top; background-color: rgb(255, 223, 191);">basic_2<br>
106 style="vertical-align: top; background-color: rgb(255, 223, 191);">April
110 style="vertical-align: top; background-color: rgb(255, 223, 191);">planned
115 style="vertical-align: top; background-color: rgb(255, 223, 191);">not
121 style="vertical-align: top; background-color: rgb(255, 191, 191);">1<br>
124 style="vertical-align: top; background-color: rgb(255, 191, 191);">basic_1<br>
127 style="vertical-align: top; background-color: rgb(255, 191, 191);">May
131 style="vertical-align: top; background-color: rgb(255, 191, 191);">November
135 style="vertical-align: top; background-color: rgb(255, 191, 191);">May
142 <h3 style="text-align: right;">Notice
147 user <img style="width: 37px; height: 37px;" alt="[Butterfly]"
148 title="Butterfly" src="download/b3.png"></h3>
150 correctly, please select a font with <a href="http://www.unicode.org/">Unicode</a>
152 For example <span style="font-weight: bold;">Lucida Sans Unicode</span>
153 (it should be already installed on your system).
154 To change the current font follow: <span style="font-weight: bold;">"Tools"
157 Options" entry → "General" tab → "Fonts" button.</span><br>
163 <a href="http://validator.w3.org/check?uri=referer"><img
164 alt="[Valid HTML 4.01 Transitional]"
165 title="Valid HTML 4.01 Transitional"
166 src="http://www.w3.org/Icons/valid-html401"
167 style="border: 0px solid ; width: 88px; height: 31px;"></a> <a
168 href="http://www.anybrowser.org/campaign/"><img
169 alt="[Use Any Browser Here]" title="Use Any Browser Here"
170 src="download/globe_trans.png"
171 style="border: 0px solid ; width: 147px; height: 42px;"></a> <img
172 style="width: 88px; height: 31px;" alt="[PNG Used Here]"
173 title="PNG Used Here" src="download/PNGnow2.png"><br>
175 Last update 2012-11-20 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio