Type theories, normal forms, and D_-lambda-models
From MaRDI portal
Publication:1102936
The study of a special filter model for the \(\lambda\)-calculus (in the sense of H. Barendregt), denoted \({\mathcal F}^*\), is the main objective of this paper. The type assignement system, on which the definition of \({\mathcal F}^*\) is based, is the classical Curry's type assignement to which \(\omega\) (the universal type), the operator \(\Lambda\) (intersection) - for type formation, and an ``inclusion relation on types are added. Much more, the initial set of atomic types is a two- element set. It is proved that \({\mathcal F}^*\) is isomorphic with an inverse limit space \(D^*_{\infty}\) constructed from a (three point) lattice with a nonstandard initial projection, which is not (Hilbert- Post) complete. A nice characterization (the first purely semantic one?) for a term to be normalizable is also given.
Recommendations
Cites work
- -calculus and computer science theory. Proceedings of the symposium held in Rome, March 25-27, 1975
- A filter lambda model and the completeness of type assignment
- A new type assignment for λ-terms
- A Syntactic Characterization of the Equality in Some Models for the Lambda Calculus
- Combinators, \(\lambda\)-terms and proof theory
- Combinatory logic. With two sections by William Craig.
- Data Types as Lattices
- Functional Characters of Solvable Terms
- scientific article; zbMATH DE number 3831284 (Why is no real title available?)
- scientific article; zbMATH DE number 3835992 (Why is no real title available?)
- scientific article; zbMATH DE number 3889501 (Why is no real title available?)
- scientific article; zbMATH DE number 3889502 (Why is no real title available?)
- scientific article; zbMATH DE number 3880074 (Why is no real title available?)
- scientific article; zbMATH DE number 3811535 (Why is no real title available?)
- scientific article; zbMATH DE number 3780545 (Why is no real title available?)
- scientific article; zbMATH DE number 3523517 (Why is no real title available?)
- scientific article; zbMATH DE number 3532922 (Why is no real title available?)
- scientific article; zbMATH DE number 3596799 (Why is no real title available?)
- scientific article; zbMATH DE number 3637819 (Why is no real title available?)
- scientific article; zbMATH DE number 3379785 (Why is no real title available?)
- Intensional interpretations of functionals of finite type I
- Lambda‐Calculus Models and Extensionality
- The completeness theorem for typing lambda-terms
- The lambda calculus. Its syntax and semantics. Rev. ed.
- 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?
Cited in
(44)- A characterization of F-complete type assignments
- Recursion over realizability structures
- Filter models with polymorphic types
- Complete restrictions of the intersection type discipline
- Intersection types for combinatory logic
- Types with intersection: An introduction
- Infinite \(\lambda\)-calculus and types
- Semantical analysis of perpetual strategies in -calculus
- Type inference, abstract interpretation and strictness analysis
- Set-theoretical and other elementary models of the \(\lambda\)-calculus
- Intersection type assignment systems
- Intersection types and domain operators
- Behavioural inverse limit -models
- Generalized filter models
- From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models
- Discrimination by parallel observers: the algorithm.
- Intersection types and lambda models
- Compositional characterisations of \(\lambda\)-terms using intersection types
- Logical semantics for stability
- Relational graph models, Taylor expansion and extensionality
- Simple easy terms
- Filter models: non-idempotent intersection types, orthogonality and polymorphism
- scientific article; zbMATH DE number 3889502 (Why is no real title available?)
- A filter lambda model and the completeness of type assignment
- 2008 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '08
- Effective λ-models versus recursively enumerable λ-theories
- scientific article; zbMATH DE number 2003154 (Why is no real title available?)
- Relational graph models at work
- Degrees of extensionality in the theory of Böhm trees and Sallé's conjecture
- On the characterization of models of \(\mathcal{H}^*\)
- From Böhm's theorem to observational equivalences: an informal account
- Intersection types and computational rules
- scientific article; zbMATH DE number 7204439 (Why is no real title available?)
- Every \(\lambda \)-term is meaningful for the infinitary relational model
- The infinitary lambda calculus of the infinite eta Böhm trees
- On equivalence and canonical forms in the LF type theory
- Strong normalization from an unusual point of view
- Recursive Domain Equations of Filter Models
- Cut-elimination in the strict intersection type assignment system is strongly normalizing
- Intersection types for -trees
- Intersection types and denotational semantics: an extended abstract (invited paper)
- Lambda galore
- Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca
- An irregular filter model
This page was built for publication: Type theories, normal forms, and \(D_{\infty}\)-lambda-models
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1102936)
