The completeness theorem for typing lambda-terms
From MaRDI portal
Publication:1839242
DOI10.1016/0304-3975(83)90136-6zbMath0512.03009OpenAlexW2090790829MaRDI QIDQ1839242
Publication date: 1983
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(83)90136-6
Related Items (35)
Typed equivalence, type assignment, and type containment ⋮ \(F\)-semantics for type assignment systems ⋮ Precise Subtyping for Asynchronous Multiparty Sessions ⋮ A characterization of F-complete type assignments ⋮ Intersection type assignment systems ⋮ Type theories, normal forms, and \(D_{\infty}\)-lambda-models ⋮ Principal type scheme and unification for intersection type discipline ⋮ Polymorphic type inference and containment ⋮ Constructive natural deduction and its ‘ω-set’ interpretation ⋮ A completeness result for a realisability semantics for an intersection type system ⋮ A semantics for type checking ⋮ Intersection and union types ⋮ Precise subtyping for synchronous multiparty sessions ⋮ Primitive recursive functional with dependent types ⋮ A category-theoretic characterization of functional completeness ⋮ Filter models for conjunctive-disjunctive \(\lambda\)-calculi ⋮ Term-space semantics of typed lambda calculus ⋮ Complete restrictions of the intersection type discipline ⋮ Constructing type systems over an operational semantics ⋮ Type inference with simple subtypes ⋮ Computability in higher types, P\(\omega\) and the completeness of type assignment ⋮ Completeness of type assignment systems with intersection, union, and type quantifiers ⋮ A completeness result for the simply typed \(\lambda \mu \)-calculus ⋮ Unnamed Item ⋮ The semantics of second-order lambda calculus ⋮ Type inference with recursive types: Syntax and semantics ⋮ Infinite \(\lambda\)-calculus and types ⋮ On the semantics of polymorphism ⋮ Subtypes in fuzzy type theory ⋮ Curry's type-rules are complete with respect to the F-semantics too ⋮ Completeness of type assignment in continuous lambda models ⋮ Type inference, abstract interpretation and strictness analysis ⋮ Meeting of the Association for Symbolic Logic Florence, Italy 1982 ⋮ Weak completeness of type assignment in \(\lambda\)-calculus models: A generalization of Hindley's result ⋮ An algebraic semantics of higher-order types with subtypes
Uses Software
Cites Work
- A theory of type polymorphism in programming
- Foliations on open manifolds. II
- Functionals defined by recursion
- A filter lambda model and the completeness of type assignment
- Lambda‐Calculus Models and Extensionality
- Data Types as Lattices
- The Principal Type-Scheme of an Object in Combinatory Logic
- Resolution in type theory
- Modified basic functionality in combinatory logic
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: The completeness theorem for typing lambda-terms
