The Formal System λδ version 1
foreword
news
documentation
implementation
Formats
The formal specification of λδ version 1 is available in the following formats:
lambdadelta_1 for Coq 7.3.1
(revised
2012-10
). Source scripts.
BibTeX entry
lambdadelta_1 for Matita 0.5"
(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
.
lambdadelta_1 for Matita 0.5"
(revised
2011-09
).
HELM
directory.
Notice: the HELM rendering engine is offline.
Last update: Sun, 06 Jul 2014 20:36:00 +0200