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)- scientific article; zbMATH DE number 7526056 (Why is no real title available?)
- Higher-order processes and their models
- scientific article; zbMATH DE number 3938562 (Why is no real title available?)
- Refinement types for program analysis
- scientific article; zbMATH DE number 3905869 (Why is no real title available?)
- Intersection and union types
- May and must convergency in concurrent λ-calculus
- A realizability interpretation for intersection and union types
- Proof-functional connectives and realizability
- On sets of terms having a given intersection type
- From semantics to types: the case of the imperative \(\lambda\)-calculus
- Towards lambda calculus order-incompleteness
- Coppo-Dezani types do not correspond to propositional logic
- The untyped computational \(\lambda \)-calculus and its intersection type discipline
- Applicative intersection types
- On Church's formal theory of functions and functionals. The - calculus: Connections to higher type recursion theory, proof theory, category theory
- Implicit self-adjusting computation for purely functional programs
- Precise Subtyping for Asynchronous Multiparty Sessions
- Implicative algebras: a new foundation for realizability and forcing
- Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage
- Completeness of intersection and union type assignment systems for call-by-value \(\lambda\)-models
- Easiness in graph models
- Subtyping in logical form
- Preface to the special volume
- Type assignment and conservation properties
- Completeness of type assignment systems with intersection, union, and type quantifiers
- Intersection types and lambda models
- Strongly normalising cut-elimination with strict intersection types
- On Isomorphisms of Intersection Types
- Type inference for rank-2 intersection types using set unification
- scientific article; zbMATH DE number 7155170 (Why is no real title available?)
- Comparing cubes of typed and type assignment systems
- 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
- Simple easy terms
- A resource aware semantics for a focused intuitionistic calculus
- Strong normalizability as a finiteness structure via the Taylor expansion of \(\lambda\)-terms
- Easy lambda-terms are not always simple
- Strictness, totality, and non-standard-type inference
- Intersection types for combinatory logic
- Types with intersection: An introduction
- Reducibility: a ubiquitous method in lambda calculus with intersection types
- Normalization without reducibility
- Relational graph models at work
- Semantical analysis of perpetual strategies in -calculus
- 2002 Annual Conference of the Australasian Association for Logic
- Weak completeness of type assignment in -calculus models: A generalization of Hindley's result
- From semantics to types: the case of the imperative \(\lambda\)-calculus
- On the unity of duality
- Normalization results for typeable rewrite systems
- Intersection-types à la Church
- Behavioural inverse limit \(\lambda\)-models
- Intersection types and domain operators
- The better bubbling lemma
- Some reasons for generalising domain theory
- Intersection and singleton type assignment characterizing finite Böhm-trees
- Generalized filter models
- Semantic types and approximation for Featherweight Java
- Call-by-value Solvability
- Linearity and iterator types for Gödel's system \(\mathcal T\)
- Graph lambda theories
- Functional programs as compressed data
- 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
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)
