A filter lambda model and the completeness of type assignment
From MaRDI portal
Publication:3335753
DOI10.2307/2273659zbMath0545.03004MaRDI QIDQ3335753
Mariangiola Dezani-Ciancaglini, Mario Coppo, H. P. 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
03B40: Combinatory logic and lambda calculus
Related Items
2002 European Summer Meeting of the Association for Symbolic Logic Logic Colloquium '02, A classification of intersection type systems, 2002 Annual Conference of the Australasian Association for Logic, The emptiness problem for intersection types, Type inference with simple subtypes, Call-by-value Solvability, Recursive Domain Equations of Filter Models, Types for Hereditary Head Normalizing Terms, Full intersection types and topologies in lambda calculus, 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, Cut-elimination in the strict intersection type assignment system is strongly normalizing, Computability in higher types, P\(\omega\) and the completeness of type assignment, Higher-order subtyping and its decidability, Ternary relations and relevant semantics, Filter models for conjunctive-disjunctive \(\lambda\)-calculi, Intersection type assignment systems with higher-order algebraic rewriting, The semantics of second-order lambda calculus, Type inference with recursive types: Syntax and semantics, Coppo-Dezani types do not correspond to propositional logic, Principal type schemes for an extended type theory, Completeness of type assignment in continuous lambda models, Weak completeness of type assignment in \(\lambda\)-calculus models: A generalization of Hindley's result, A completeness result for a realisability semantics for an intersection type system, 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, A domain model characterising strong normalisation, Set-theoretical models of lambda-calculus: theories, expansions, isomorphisms, A characterization of F-complete type assignments, Type theories, normal forms, and \(D_{\infty}\)-lambda-models, Principal type scheme and unification for intersection type discipline, Polymorphic type inference and containment, On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory, Domain theory in logical form, Implementing the `Fool's model' of combinatory logic, Filter models with polymorphic types, Complete restrictions of the intersection type discipline, An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus, Constructing type systems over an operational semantics, Intersection types for combinatory logic, Types with intersection: An introduction, Full abstractness for a functional/concurrent language with higher-order value-passing, From constructivism to computer science, Infinite \(\lambda\)-calculus and types, Semantical analysis of perpetual strategies in \(\lambda\)-calculus, Type inference, abstract interpretation and strictness analysis, Set-theoretical and other elementary models of the \(\lambda\)-calculus, An algebraic semantics of higher-order types with subtypes, \(F\)-semantics for type assignment systems, Proof-functional connectives and realizability, Intersection type assignment systems, Normalization results for typeable rewrite systems, Comparing cubes of typed and type assignment systems, Typed operational semantics for higher-order subtyping., A binary modal logic for the intersection types of lambda-calculus., The semantics of entailment omega, Intersection types and domain operators, Behavioural inverse limit \(\lambda\)-models, Generalized filter models, From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models, Typing and computational properties of lambda expressions, On the semantics of polymorphism, The completeness theorem for typing lambda-terms, Normalization without reducibility, Normalization, approximation, and semantics for combinator systems, Discrimination by parallel observers: the algorithm., Dependent types with subtyping and late-bound overloading, Intersection and singleton type assignment characterizing finite Böhm-trees, Infinite intersection types, Strong normalization and typability with intersection types, Easiness in graph models, Intersection types and lambda models, Intersection-types à la Church, Logical equivalence for subtyping object and recursive types, On the unity of duality, Compositional characterisations of \(\lambda\)-terms using intersection types, Combinatory logic and the semantics of substructural logics, Graph lambda theories, On Isomorphisms of Intersection Types, 2008 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '08, Meeting of the Association for Symbolic Logic Florence, Italy 1982, Constructive natural deduction and its ‘ω-set’ interpretation
Cites Work
