The formal system λδ (\lambda\delta) is a typed λ-calculus aiming to support
the foundations of Mathematics that require an underlying specification language
(for example the
Minimal Type Theory
and its predecessors).
λδ is developed in the context of the
Hypertextual Electronic Library of Mathematics
as a machine-checked digital specification
that is not the formal counterpart of some previously published informal material.
To view this site correctly, please select a font
with
Unicode support.
For example "Lucida Sans Unicode" (it should be already installed on your system).
To change the current font follow:
"Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button.