scientific article; zbMATH DE number 139605

MaRDI QIDQ4029583zbMATH OpenFDO

Authors Andrea Asperti, Giuseppe Longo

Publication date 28 March 1993

zbMATH Keywords

\(PER_ \omega\)categories withpartial morphismscomplete objectspartial computationspartial retraction systemstyped \(\lambda\)-calculus

Mathematics Subject Classification ID

Categories of sets, characterizations (18B05) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

[For the entire collection see Zbl 0745.00057.] The aim of this paper is to compare type-structures, i.e., models of typed \(\lambda\)-calculus, when data types are taken to be (possibly structured) countable sets and morphisms to be effective transformations. This will be done by tools related to Friedman's homomorphisms and Plotkin-Statman's logical relations by \textit{H. Friedman} [Lect. Notes Math. 453, 22-37 (1975; Zbl 0311.02040)], \textit{G. Plotkin} [Notes on completeness of the full continuous type hierarchy, Manuscript, Lab. for Comput. Sci., M.I.T. (1982)] and \textit{R. Statman} [Logical relations and typed lambda-calculus, Inform. and Control (1984)].

Recommendations

• Publication:3026332
• scientific article; zbMATH DE number 4021100
• Types, abstraction, and parametric polymorphism, part 2
• scientific article; zbMATH DE number 3898875
• scientific article; zbMATH DE number 4027428

Cited in

(5)

• On Church's formal theory of functions and functionals. The - calculus: Connections to higher type recursion theory, proof theory, category theory
• scientific article; zbMATH DE number 4014020 (Why is no real title available?)
• scientific article; zbMATH DE number 2070556 (Why is no real title available?)
• Thickness, and a categoric view of type-space functors
• A category-theoretic characterization of functional completeness

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4029583)