A characterization of F-complete type assignments

DOI10.1016/0304-3975(86)90043-5zbMath0619.03014OpenAlexW2091240930MaRDI QIDQ1089331

Mariangiola Dezani-Ciancaglini, Ines Margaria

Publication date: 1986

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(86)90043-5

zbMATH Keywords

completenesssoundnesstype assignmentF-semantics of typesintersection type disciplinelambda models

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models of other mathematical theories (03C65) Combinatory logic and lambda calculus (03B40)

Related Items (11)

\(F\)-semantics for type assignment systems ⋮ Intersection type assignment systems ⋮ Typed operational semantics for higher-order subtyping. ⋮ Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca ⋮ Complete restrictions of the intersection type discipline ⋮ Types with intersection: An introduction ⋮ Cut-elimination in the strict intersection type assignment system is strongly normalizing ⋮ Generalized filter models ⋮ From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models ⋮ Discrimination by parallel observers: the algorithm. ⋮ Type inference, abstract interpretation and strictness analysis

Uses Software

• ML

Cites Work

• Completeness of type assignment in continuous lambda models
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Set-theoretical models of lambda-calculus: theories, expansions, isomorphisms
• Type theories, normal forms, and \(D_{\infty}\)-lambda-models
• An extension of basic functionality theory for \(\lambda\)-calculus
• An algebraic interpretation of the \(\lambda\beta K\)-calculus; and an application of a labelled \(\lambda\)-calculus
• A theory of type polymorphism in programming
• On the semantics of polymorphism
• The completeness theorem for typing lambda-terms
• Curry's type-rules are complete with respect to the F-semantics too
• Combinatory logic. Vol. II
• Combinators, \(\lambda\)-terms and proof theory
• A new type assignment for λ-terms
• A filter lambda model and the completeness of type assignment
• The Expressiveness of Simple and Second-Order Type Structures
• 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
• Intensional interpretations of functionals of finite type I
• The Principal Type-Scheme of an Object in Combinatory Logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A characterization of F-complete type assignments