Modern eyes on λ-calculus
presents detail on the three level signature as applied to formalism implicitly appearing in classic work
like
Schönfinkel's Bausteine (1924),
Curry's functionality (1934)
and
Church's simple types
(1940).
"Fuzzy λ-calculus" can be easily developed. Modern type theory, including
Martin-Löf's Type theory (MLTT) and Homotopy Type Theory (HoTT), ignores the use of levels of
signature, and also allows for incompleteness in the use of a "universe". This
basically falls down on a restricted understanding of the semantics of
Church's 'ι' (iota), and on a informal notion related to Church's 'ο'
(omicron). Modern type theory departs from Church's 1940 work and also from
Grothendieck's view on universes.
PhD thesis work on Generalized General Logics
provide background and powerful tools for a broader view of lative logic as generalizing the logical frameworks
by Goguen and
Burstall on 'institutions' (1984) and by Meseguer on 'entailment systems' (1987).