zbMATH — the first resource for mathematics

Domain-free pure type systems. (English) Zbl 0979.03013
In order to obtain a uniform presentation of a certain group of Curry-style type systems, the domains of the abstractions of a pure type system (PTS) are plainly omitted. These variants of PTSs are called domain-free pure type systems (DFPTSs). Amongst the examples of DFPTSs there are predicative type systems and proof assistants based on Martin Löf’s type theory. The consequence of this approach is somewhat unusual for impredicative systems. Although it is possible to define them as DFPTSs these do not correspond to the usual way of writing polymorphic functions. For instance the polymorphic identity \(\lambda x {:} *. \lambda y {:} x.y\) becomes \(\lambda xy.y\).
The authors develop an extensive meta-theory for DFPTSs. They compare them with PTSs [H. Barendregt, “Lambda calculi with types”, in: S. Abramsky et al. (eds.), Handbook of logic in computer science, Vol. 2, 117-309 (1992; Zbl 0777.68001)] and type assignment systems [S. van Bakel, L. Liquori, S. Ronchi della Rocca and P. Krzyczyn, Lect. Notes Comput. Sci. 813, 353-365 (1994; Zbl 0947.03022)]. Many results are deduced with the help of the comparision with PTSs.
This paper is an extended and updated version of Lect. Notes Comput. Sci. 1234, 9-20 (1997; Zbl 0887.03010).

03B40 Combinatory logic and lambda calculus
03B15 Higher-order logic; type theory (MSC2010)
68N18 Functional programming and lambda calculus
03B70 Logic in computer science
Full Text: DOI