An extension of basic functionality theory for \(\lambda\)-calculus
From MaRDI portal
Publication:1134141
DOI10.1305/ndjfl/1093883253zbMath0423.03010OpenAlexW2085670481MaRDI QIDQ1134141
Mariangiola Dezani-Ciancaglini, Mario Coppo
Publication date: 1980
Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1305/ndjfl/1093883253
Related Items
\(F\)-semantics for type assignment systems, Proof-functional connectives and realizability, A semantic account of strong normalization in linear logic, A type assignment for \(\lambda\)-calculus complete both for FPTIME and strong normalization, Easy lambda-terms are not always simple, Principality and type inference for intersection types using expansion variables, A characterization of F-complete type assignments, Intersection types for explicit substitutions, A Datalog Recognizer for Almost Affine λ-CFGs, A Realizability Interpretation for Intersection and Union Types, Intersection type assignment systems, Intersection-types à la Church, Unnamed Item, Normalization results for typeable rewrite systems, A resource aware semantics for a focused intuitionistic calculus, Principal type scheme and unification for intersection type discipline, Higher-order subtyping and its decidability, A completeness result for a realisability semantics for an intersection type system, Semantic types and approximation for Featherweight Java, Type Inference for Rank 2 Gradual Intersection Types, Type inference for rank-2 intersection types using set unification, A strong call-by-need calculus, Structural rules and algebraic properties of intersection types, Quantitative weak linearisation, Non-idempotent intersection types in logical form, Tight typings and split bounds, fully developed, Linear dependent types in a call-by-value scenario, Graph lambda theories, A metamodel of access control for distributed environments: applications and properties, On Isomorphisms of Intersection Types, Linearity and iterator types for Gödel's system \(\mathcal T\), 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, 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, Intersection type assignment systems with higher-order algebraic rewriting, Finite Combinatory Logic with Intersection Types, A Filter Model for the λμ-Calculus, Approximation Semantics and Expressive Predicate Assignment for Object-Oriented Programming, Strong normalization through intersection types and memory, Approximation and normalization results for typeable term rewriting systems, Complete restrictions of the intersection type discipline, Functional Type Assignment for Featherweight Java, Types with intersection: An introduction, Strong normalization from an unusual point of view, Intersection Types and Computational Rules, Unnamed Item, Cut-elimination in the strict intersection type assignment system is strongly normalizing, The bang calculus revisited, The emptiness problem for intersection types, Unnamed Item, Unnamed Item, Strictness, totality, and non-standard-type inference, Recursive Domain Equations of Filter Models, The bang calculus revisited, Logical Semantics for Stability, Unnamed Item, Unnamed Item, Reasoning About Call-by-need by Means of Types, Inhabitation of Low-Rank Intersection Types, Typing and computational properties of lambda expressions, Effective λ-models versus recursively enumerable λ-theories, Intersection, Universally Quantified, and Reference Types, Intersection Types for the Resource Control Lambda Calculi, Generalized filter models, Simple Easy Terms, Strongly Normalising Cut-Elimination with Strict Intersection Types, Reducibility, Intersection Typed λ-calculus, Weak linearization of the lambda calculus, Compositional characterisations of \(\lambda\)-terms using intersection types, Typing untyped \(\lambda\)-terms, or reducibility strikes again!, Pre-grammars and inhabitation for a subset of rank 2 intersection types, Dependent types with subtyping and late-bound overloading, Combining type disciplines, Implicit computation complexity in higher-order programming languages, Refinement types for program analysis, Full abstraction for lambda calculus with resources and convergence testing
