-
-
-
-
λδ version 3 (proposed)
+ ![\lambda\delta butterfly [spacer]](http://lambdadelta.info/images/b8.png)
![\lambda\delta butterfly [butterfly]](http://lambdadelta.info/images/b8.png)
The formal specification of λδ version 3
is forthcoming.
-
λδ version 2 (active)
+ ![\lambda\delta butterfly [spacer]](http://lambdadelta.info/images/b4.png)
![\lambda\delta butterfly [butterfly]](http://lambdadelta.info/images/b4.png)
The formal specification of λδ version 2
is available in the following formats:
@@ -284,7 +280,7 @@
-
λδ version 1 (superseded)
+ ![\lambda\delta butterfly [spacer]](http://lambdadelta.info/images/b6.png)
![\lambda\delta butterfly [butterfly]](http://lambdadelta.info/images/b6.png)
The formal specification of λδ version 1
is available in the following formats:
@@ -297,7 +293,7 @@
Source scripts.
Documentation (J1a).
-
-
- +
- 2015 January 15. 17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg". @@ -314,28 +310,28 @@ (revised 2011-09). Static HTML pages generated by the HELM rendering engine.
- +
- Confluence of reduction (Church-Rosser property). -
- +
- Correctness of types. -
- +
- Uniqueness of types up to conversion. -
- +
- Subject reduction of the type assignment. -
- +
- Strong normalization of the typed terms. -
- +
- Decidability of the type inference problem. @@ -382,6 +378,6 @@
-
-
Last update: Fri, 08 Apr 2016 22:51:19 +0200
+ Last update: Fri, 22 Jul 2016 19:34:08 +0200