Type theories, normal forms, and \(D_{\infty}\)-lambda-models

DOI10.1016/0890-5401(87)90042-3zbMath0645.03011OpenAlexW1979206410MaRDI QIDQ1102936

Mariangiola Dezani-Ciancaglini, Maddalena Zacchi, Mario Coppo

Publication date: 1987

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0890-5401(87)90042-3

zbMATH Keywords

filter model\(\lambda \)-calculusnormalizable termtype assignement

Mathematics Subject Classification ID

Logical aspects of lattices and related structures (03G10) Combinatory logic and lambda calculus (03B40)

Related Items (34)

Relational graph models, Taylor expansion and extensionality ⋮ Intersection types and lambda models ⋮ A characterization of F-complete type assignments ⋮ Intersection type assignment systems ⋮ Recursion over realizability structures ⋮ Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca ⋮ An irregular filter model ⋮ Intersection types and domain operators ⋮ Filter models with polymorphic types ⋮ Complete restrictions of the intersection type discipline ⋮ Intersection types for combinatory logic ⋮ Types with intersection: An introduction ⋮ From Böhm's Theorem to Observational Equivalences ⋮ Strong normalization from an unusual point of view ⋮ Intersection Types and Computational Rules ⋮ Cut-elimination in the strict intersection type assignment system is strongly normalizing ⋮ Intersection types for \(\lambda\)-trees ⋮ Recursive Domain Equations of Filter Models ⋮ 2008 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '08 ⋮ Logical Semantics for Stability ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Effective λ-models versus recursively enumerable λ-theories ⋮ Infinite \(\lambda\)-calculus and types ⋮ Semantical analysis of perpetual strategies in \(\lambda\)-calculus ⋮ Generalized filter models ⋮ Simple Easy Terms ⋮ Compositional characterisations of \(\lambda\)-terms using intersection types ⋮ From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models ⋮ Unnamed Item ⋮ Discrimination by parallel observers: the algorithm. ⋮ Type inference, abstract interpretation and strictness analysis ⋮ Set-theoretical and other elementary models of the \(\lambda\)-calculus ⋮ The infinitary lambda calculus of the infinite eta Böhm trees

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Combinatory logic. With two sections by William Craig.
• The lambda calculus. Its syntax and semantics. Rev. ed.
• \(\lambda\)-calculus and computer science theory. Proceedings of the symposium held in Rome, March 25-27, 1975
• The completeness theorem for typing lambda-terms
• Combinators, \(\lambda\)-terms and proof theory
• A new type assignment for λ-terms
• A filter lambda model and the completeness of type assignment
• Lambda‐Calculus Models and Extensionality
• Functional Characters of Solvable Terms
• A Syntactic Characterization of the Equality in Some Models for the Lambda Calculus
• Data Types as Lattices
• The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
• What is a model of the lambda calculus?
• Intensional interpretations of functionals of finite type I

This page was built for publication: Type theories, normal forms, and \(D_{\infty}\)-lambda-models