A filter lambda model and the completeness of type assignment
From MaRDI portal
Publication:3335753
DOI10.2307/2273659zbMath0545.03004OpenAlexW1970227944MaRDI QIDQ3335753
Mario Coppo, Mariangiola Dezani-Ciancaglini, Hendrik Pieter 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
Related Items (only showing first 100 items - show all)
Precise Subtyping for Asynchronous Multiparty Sessions ⋮ On sets of terms having a given intersection type ⋮ A classification of intersection type systems ⋮ (Head-)normalization of typeable rewrite systems ⋮ A Realizability Interpretation for Intersection and Union Types ⋮ Unnamed Item ⋮ A resource aware semantics for a focused intuitionistic calculus ⋮ Constructive natural deduction and its ‘ω-set’ interpretation ⋮ Unnamed Item ⋮ A semantics for type checking ⋮ Intersection and union types ⋮ May and must convergency in concurrent λ-calculus ⋮ Type Inference for Rank 2 Gradual Intersection Types ⋮ From semantics to types: the case of the imperative \(\lambda\)-calculus ⋮ Type inference for rank-2 intersection types using set unification ⋮ Structural rules and algebraic properties of intersection types ⋮ Applicative intersection types ⋮ A calculus with recursive types, record concatenation and subtyping ⋮ Node Replication: Theory And Practice ⋮ Graph lambda theories ⋮ On Isomorphisms of Intersection Types ⋮ Implicative algebras: a new foundation for realizability and forcing ⋮ Modularity of termination and confluence in combinations of rewrite systems with λω ⋮ Higher-order processes and their models ⋮ Approximation Semantics and Expressive Predicate Assignment for Object-Oriented Programming ⋮ Some reasons for generalising domain theory ⋮ Approximation and normalization results for typeable term rewriting systems ⋮ 2002 Annual Conference of the Australasian Association for Logic ⋮ Functional Type Assignment for Featherweight Java ⋮ Towards Lambda Calculus Order-Incompleteness ⋮ Hyperformulae, Parallel Deductions and Intersection Types ⋮ Intersection Types and Computational Rules ⋮ Unnamed Item ⋮ Full intersection types and topologies in lambda calculus ⋮ The emptiness problem for intersection types ⋮ Type inference with simple subtypes ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Intersection types for \(\lambda\)-trees ⋮ Strictness, totality, and non-standard-type inference ⋮ Completeness of intersection and union type assignment systems for call-by-value \(\lambda\)-models ⋮ Completeness of type assignment systems with intersection, union, and type quantifiers ⋮ Type inference for set theory ⋮ Recursive Domain Equations of Filter Models ⋮ Call-by-value Solvability ⋮ 2002 European Summer Meeting of the Association for Symbolic Logic Logic Colloquium '02 ⋮ 2008 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '08 ⋮ Types for Hereditary Head Normalizing Terms ⋮ Unnamed Item ⋮ Principal Types for Nominal Theories ⋮ lambda!-calculus, Intersection Types, and Involutions ⋮ Intersection Types for the Resource Control Lambda Calculi ⋮ Taming the Merge Operator ⋮ Meeting of the Association for Symbolic Logic Florence, Italy 1982 ⋮ The approximation theorem for the Λμ-calculus ⋮ Refinement types for program analysis ⋮ Full abstraction for lambda calculus with resources and convergence testing ⋮ \(F\)-semantics for type assignment systems ⋮ Proof-functional connectives and realizability ⋮ Easy lambda-terms are not always simple ⋮ Graph easy sets of mute lambda terms ⋮ Easiness in graph models ⋮ Intersection types and lambda models ⋮ A characterization of F-complete type assignments ⋮ Infinite intersection types ⋮ Intersection type assignment systems ⋮ Intersection-types à la Church ⋮ Nominal essential intersection types ⋮ Normalization results for typeable rewrite systems ⋮ Type theories, normal forms, and \(D_{\infty}\)-lambda-models ⋮ Combinatory logic and the semantics of substructural logics ⋮ Principal type scheme and unification for intersection type discipline ⋮ Polymorphic type inference and containment ⋮ Comparing cubes of typed and type assignment systems ⋮ Higher-order subtyping and its decidability ⋮ Ternary relations and relevant semantics ⋮ On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory ⋮ Strong normalization and typability with intersection types ⋮ A completeness result for a realisability semantics for an intersection type system ⋮ Semantic types and approximation for Featherweight Java ⋮ Typing Weak MSOL Properties ⋮ Precise subtyping for synchronous multiparty sessions ⋮ Typed operational semantics for higher-order subtyping. ⋮ Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\) ⋮ The untyped computational \(\lambda \)-calculus and its intersection type discipline ⋮ A binary modal logic for the intersection types of lambda-calculus. ⋮ The semantics of entailment omega ⋮ Linearity and iterator types for Gödel's system \(\mathcal T\) ⋮ Domain theory in logical form ⋮ 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 ⋮ The heart of intersection type assignment: Normalisation proofs revisited ⋮ A typed lambda calculus with intersection types ⋮ Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage ⋮ An irregular filter model ⋮ A type assignment system for game semantics ⋮ Intersection types and domain operators ⋮ Behavioural inverse limit \(\lambda\)-models ⋮ Implementing the `Fool's model' of combinatory logic ⋮ Filter models with polymorphic types
Cites Work
This page was built for publication: A filter lambda model and the completeness of type assignment
