A filter lambda model and the completeness of type assignment
From MaRDI portal
Publication:3335753
DOI10.2307/2273659zbMATH Open0545.03004OpenAlexW1970227944MaRDI QIDQ3335753FDOQ3335753
Authors: Mario Coppo, Mariangiola Dezani-Ciancaglini, Henk Barendregt 
Publication date: 1983
Published in: Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2307/2273659
Recommendations
- Completeness of type assignment in continuous lambda models
- Weak completeness of type assignment in \(\lambda\)-calculus models: A generalization of Hindley's result
- A characterization of F-complete type assignments
- Type theories, normal forms, and \(D_{\infty}\)-lambda-models
- Complete restrictions of the intersection type discipline
Cites Work
Cited In (only showing first 100 items - show all)
- A domain model characterising strong normalisation
- Dependent types with subtyping and late-bound overloading
- Logical semantics for stability
- Title not available (Why is that?)
- Modularity of termination and confluence in combinations of rewrite systems with \(\lambda_\omega\)
- Compositional characterisations of \(\lambda\)-terms using intersection types
- Full abstractness for a functional/concurrent language with higher-order value-passing
- How to think of intersection types as Cartesian products
- Strong normalization through intersection types and memory
- The relevance of semantic subtyping
- \(F\)-semantics for type assignment systems
- A binary modal logic for the intersection types of lambda-calculus.
- Constructing type systems over an operational semantics
- Elaborating intersection and union types
- Nominal essential intersection types
- A classification of intersection type systems
- Principal types for nominal theories
- Intersection types for the resource control lambda calculi
- Term-space semantics of typed lambda calculus
- Taming the merge operator
- Approximation and normalization results for typeable term rewriting systems
- (Head-)normalization of typeable rewrite systems
- Intersection types and computational rules
- An algebraic semantics of higher-order types with subtypes
- Refinement types for program analysis
- Intersection and union types
- May and must convergency in concurrent λ-calculus
- A realizability interpretation for intersection and union types
- Proof-functional connectives and realizability
- Towards lambda calculus order-incompleteness
- Applicative intersection types
- On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory
- Intersection types and lambda models
- A typed lambda calculus with intersection types
- An irregular filter model
- Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca
- On strong normalization and type inference in the intersection type discipline
- Intersection types for combinatory logic
- Types with intersection: An introduction
- Semantical analysis of perpetual strategies in \(\lambda\)-calculus
- Intersection-types à la Church
- Behavioural inverse limit \(\lambda\)-models
- Intersection types and domain operators
- Intersection and singleton type assignment characterizing finite Böhm-trees
- Generalized filter models
- Hyperformulae, parallel deductions and intersection types
- On the semantics of polymorphism
- Discrimination by parallel observers: the algorithm.
- Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)
- Set-theoretical and other elementary models of the \(\lambda\)-calculus
- A fully abstract model for mobile ambients
- Strong normalization from an unusual point of view
- Type inference with recursive types: Syntax and semantics
- The emptiness problem for intersection types
- The heart of intersection type assignment: Normalisation proofs revisited
- Filter models with polymorphic types
- Principal type scheme and unification for intersection type discipline
- Type inference, abstract interpretation and strictness analysis
- Complete restrictions of the intersection type discipline
- A Filter Model for the λμ-Calculus
- Ternary relations and relevant semantics
- Intersection type assignment systems
- Filter models for conjunctive-disjunctive \(\lambda\)-calculi
- Full abstraction for lambda calculus with resources and convergence testing
- Title not available (Why is that?)
- Approximation semantics and expressive predicate assignment for object-oriented programming (extended abstract)
- Type inference with simple subtypes
- Domain theory in logical form
- Graph easy sets of mute lambda terms
- Normalization, approximation, and semantics for combinator systems
- A type assignment system for game semantics
- From constructivism to computer science
- Principal type schemes for an extended type theory
- Intersection types for \(\lambda\)-trees
- Computability in higher types, P\(\omega\) and the completeness of type assignment
- Typing and computational properties of lambda expressions
- A characterization of F-complete type assignments
- Completeness of type assignment in continuous lambda models
- Type theories, normal forms, and \(D_{\infty}\)-lambda-models
- Polymorphic type inference and containment
- Higher-order subtyping and its decidability
- A completeness result for a realisability semantics for an intersection type system
- Infinite \(\lambda\)-calculus and types
- Set-theoretical models of lambda-calculus: theories, expansions, isomorphisms
- Logical equivalence for subtyping object and recursive types
- The semantics of entailment omega
- From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models
- A semantics for type checking
- An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus
- Implementing the `Fool's model' of combinatory logic
- The semantics of second-order lambda calculus
- Intersection type assignment systems with higher-order algebraic rewriting
- Strong normalization and typability with intersection types
- Typed operational semantics for higher-order subtyping.
- The completeness theorem for typing lambda-terms
- Higher-order processes and their models
- Title not available (Why is that?)
- Combinatory logic and the semantics of substructural logics
- The untyped computational \(\lambda \)-calculus and its intersection type discipline
- Coppo-Dezani types do not correspond to propositional logic
This page was built for publication: A filter lambda model and the completeness of type assignment
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3335753)
