Type theories, normal forms, and D_-lambda-models

DOI10.1016/0890-5401(87)90042-3zbMATH Open0645.03011OpenAlexW1979206410MaRDI QIDQ1102936FDOQ1102936

Authors: Mariangiola Dezani-Ciancaglini, Mario Coppo, Maddalena Zacchi 

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

Recommendations

• scientific article; zbMATH DE number 3889502
• A filter lambda model and the completeness of type assignment
• Infinite \(\lambda\)-calculus and types
• Generalized filter models
• A Filter Model for Concurrent $\lambda$-Calculus

zbMATH Keywords

\(\lambda \)-calculusfilter modelnormalizable termtype assignement

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (42)

• 2008 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '08
• Set-theoretical and other elementary models of the \(\lambda\)-calculus
• Strong normalization from an unusual point of view
• Filter models with polymorphic types
• Logical semantics for stability
• Type inference, abstract interpretation and strictness analysis
• Complete restrictions of the intersection type discipline
• Effective λ-models versus recursively enumerable λ-theories
• Intersection type assignment systems
• Compositional characterisations of \(\lambda\)-terms using intersection types
• Relational graph models, Taylor expansion and extensionality
• Recursive Domain Equations of Filter Models
• Title not available (Why is that?)
• The infinitary lambda calculus of the infinite eta Böhm trees
• Intersection types for \(\lambda\)-trees
• A characterization of F-complete type assignments
• Infinite \(\lambda\)-calculus and types
• From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models
• Degrees of extensionality in the theory of Böhm trees and Sallé's conjecture
• Recursion over realizability structures
• On the characterization of models of \(\mathcal{H}^*\)
• Intersection types and computational rules
• Title not available (Why is that?)
• On equivalence and canonical forms in the LF type theory
• Filter models: non-idempotent intersection types, orthogonality and polymorphism
• Intersection types and lambda models
• An irregular filter model
• Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca
• Every \(\lambda \)-term is meaningful for the infinitary relational model
• Simple easy terms
• Relational graph models at work
• Intersection types for combinatory logic
• Types with intersection: An introduction
• Semantical analysis of perpetual strategies in \(\lambda\)-calculus
• Behavioural inverse limit \(\lambda\)-models
• Intersection types and domain operators
• A filter lambda model and the completeness of type assignment
• Generalized filter models
• Title not available (Why is that?)
• From Böhm's theorem to observational equivalences: an informal account
• Cut-elimination in the strict intersection type assignment system is strongly normalizing
• Discrimination by parallel observers: the algorithm.

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)