# 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.

##### MSC:
 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 03B40 Combinatory logic and lambda calculus
##### Keywords:
semantics; AUTOMATH; second order lambda calculus
Full Text: