zbMATH — the first resource for mathematics

Semantics for classical AUTOMATH und related systems. (English) Zbl 0564.68060
The authors give a model for the language AUTOMATH by interpreting types as elements in the model \(P\omega\) that are closures and objects as arbitrary elements of \(P\omega\). The construction is based on the universal closure of all closures, due to P. Hancock, P. Martin-Löf and D. Scott. The interpretation is stronger than the intended one of AUTOMATH: all types are inhabited. In fact, in this way a model for the second order lambda calculus is obtained.

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B40 Combinatory logic and lambda calculus
Full Text: DOI