A characterization of F-complete type assignments

DOI10.1016/0304-3975(86)90043-5zbMATH Open0619.03014OpenAlexW2091240930MaRDI QIDQ1089331FDOQ1089331

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

Recommendations

• scientific article; zbMATH DE number 3880074
• \(F\)-semantics for type assignment systems
• Principal Typing in a ∀Λ-Discipline
• Complete restrictions of the intersection type discipline
• scientific article; zbMATH DE number 1361533

zbMATH Keywords

completenesssoundnesstype assignmentF-semantics of typesintersection type disciplinelambda models

Mathematics Subject Classification ID

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

Cites Work

• A theory of type polymorphism in programming
• An algebraic interpretation of the \(\lambda\beta K\)-calculus; and an application of a labelled \(\lambda\)-calculus
• Title not available (Why is that?)
• The lambda calculus. Its syntax and semantics. Rev. ed.
• An extension of basic functionality theory for \(\lambda\)-calculus
• Data Types as Lattices
• Type theories, normal forms, and \(D_{\infty}\)-lambda-models
• A Syntactic Characterization of the Equality in Some Models for the Lambda Calculus
• Title not available (Why is that?)
• Set-theoretical models of lambda-calculus: theories, expansions, isomorphisms
• A filter lambda model and the completeness of type assignment
• Combinatory logic. Vol. II
• Title not available (Why is that?)
• The Principal Type-Scheme of an Object in Combinatory Logic
• 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?)
• The Expressiveness of Simple and Second-Order Type Structures
• Lambda‐Calculus Models and Extensionality
• Title not available (Why is that?)
• The completeness theorem for typing lambda-terms
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Completeness of type assignment in continuous lambda models
• A new type assignment for λ-terms
• Title not available (Why is that?)
• Title not available (Why is that?)
• Curry's type-rules are complete with respect to the F-semantics too
• Combinators, \(\lambda\)-terms and proof theory
• On the semantics of polymorphism
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (15)

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

Uses Software

• ML

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

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