A filter lambda model and the completeness of type assignment
From MaRDI portal
Publication:3335753
Recommendations
- Completeness of type assignment in continuous lambda models
- Weak completeness of type assignment in -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)- Cut-elimination in the strict intersection type assignment system is strongly normalizing
- Constructive natural deduction and its ‘ω-set’ interpretation
- On the semantics of polymorphism
- A domain model characterising strong normalisation
- Discrimination by parallel observers: the algorithm.
- Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)
- Hyperformulae, parallel deductions and intersection types
- Structural rules and algebraic properties of intersection types
- Dependent types with subtyping and late-bound overloading
- Set-theoretical and other elementary models of the \(\lambda\)-calculus
- scientific article; zbMATH DE number 7561342 (Why is no real title available?)
- 2008 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '08
- Strong normalization from an unusual point of view
- Type inference with recursive types: Syntax and semantics
- A fully abstract model for mobile ambients
- The heart of intersection type assignment: Normalisation proofs revisited
- Filter models with polymorphic types
- The emptiness problem for intersection types
- Full intersection types and topologies in lambda calculus
- Logical semantics for stability
- Types for Hereditary Head Normalizing Terms
- Principal type scheme and unification for intersection type discipline
- Type inference, abstract interpretation and strictness analysis
- Characterization of the principal type of normal forms in an intersection type system
- Résultats de complétude pour des classes de types du système $\mathcal {AF}2$
- Complete restrictions of the intersection type discipline
- Ternary relations and relevant semantics
- The approximation theorem for the \(\Lambda_{\mu}\)-calculus
- A Filter Model for the λμ-Calculus
- A calculus with recursive types, record concatenation and subtyping
- scientific article; zbMATH DE number 7559294 (Why is no real title available?)
- Filter models for conjunctive-disjunctive \(\lambda\)-calculi
- Intersection type assignment systems
- 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
- Full abstraction for lambda calculus with resources and convergence testing
- How to think of intersection types as Cartesian products
- Strong normalization through intersection types and memory
- Recursive Domain Equations of Filter Models
- scientific article; zbMATH DE number 3889502 (Why is no real title available?)
- The relevance of semantic subtyping
- Domain theory in logical form
- Precise subtyping for synchronous multiparty sessions
- Infinite intersection types
- Graph easy sets of mute lambda terms
- Approximation semantics and expressive predicate assignment for object-oriented programming (extended abstract)
- \(F\)-semantics for type assignment systems
- Normalization, approximation, and semantics for combinator systems
- A binary modal logic for the intersection types of lambda-calculus.
- Type inference with simple subtypes
- A type assignment system for game semantics
- Constructing type systems over an operational semantics
- From constructivism to computer science
- Principal type schemes for an extended type theory
- scientific article; zbMATH DE number 4087626 (Why is no real title available?)
- lambda!-calculus, Intersection Types, and Involutions
- Finite combinatory logic with intersection types
- Computability in higher types, P and the completeness of type assignment
- Typing and computational properties of lambda expressions
- Intersection types for \(\lambda\)-trees
- Elaborating intersection and union types
- 2002 European Summer Meeting of the Association for Symbolic Logic Logic Colloquium '02
- Completeness of type assignment in continuous lambda models
- A characterization of F-complete type assignments
- Higher-order subtyping and its decidability
- Type theories, normal forms, and \(D_{\infty}\)-lambda-models
- Polymorphic type inference and containment
- Nominal essential intersection types
- Meeting of the Association for Symbolic Logic Florence, Italy 1982
- A classification of intersection type systems
- A completeness result for a realisability semantics for an intersection type system
- Infinite \(\lambda\)-calculus and types
- Principal types for nominal theories
- Intersection types for the resource control lambda calculi
- Set-theoretical models of lambda-calculus: theories, expansions, isomorphisms
- Type inference for set theory
- Logical equivalence for subtyping object and recursive types
- The semantics of entailment omega
- Term-space semantics of typed lambda calculus
- Solvability = typability + inhabitation
- From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models
- An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus
- Reasoning about call-by-need by means of types
- Functional type assignment for Featherweight Java. To Rinus Plasmeijer, in honour of his 61st birthday
- A semantics for type checking
- Implementing the `Fool's model' of combinatory logic
- Taming the merge operator
- The semantics of second-order lambda calculus
- Intersection type assignment systems with higher-order algebraic rewriting
- Node Replication: Theory And Practice
- Strong normalization and typability with intersection types
- Approximation and normalization results for typeable term rewriting systems
- Typed operational semantics for higher-order subtyping.
- (Head-)normalization of typeable rewrite systems
- An algebraic semantics of higher-order types with subtypes
- Intersection types and computational rules
- The completeness theorem for typing lambda-terms
- Type Inference for Rank 2 Gradual Intersection Types
- Combinatory logic and the semantics of substructural logics
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)
