A new type assignment for λ-terms
From MaRDI portal
Publication:3208623
DOI10.1007/BF02011875zbMath0418.03010OpenAlexW1981303668MaRDI QIDQ3208623
Mariangiola Dezani-Ciancaglini, Mario Coppo
Publication date: 1978
Published in: Archiv für Mathematische Logik und Grundlagenforschung (Search for Journal in Brave)
Full work available at URL: https://eudml.org/doc/137952
Related Items (50)
A classification of intersection type systems ⋮ A characterization of F-complete type assignments ⋮ Intersection types for explicit substitutions ⋮ Infinite intersection types ⋮ Call-by-Value Non-determinism in a Linear Logic Type Discipline ⋮ Unnamed Item ⋮ Nominal essential intersection types ⋮ Type theories, normal forms, and \(D_{\infty}\)-lambda-models ⋮ A model for syntactic control of interference ⋮ A resource aware semantics for a focused intuitionistic calculus ⋮ Higher-order subtyping and its decidability ⋮ On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory ⋮ A completeness result for a realisability semantics for an intersection type system ⋮ Higher-order subtyping ⋮ Characterising Strongly Normalising Intuitionistic Sequent Terms ⋮ Non-Deterministic Functions as Non-Deterministic Processes (Extended Version) ⋮ Unnamed Item ⋮ System ST toward a type system for extraction and proofs of programs ⋮ Node Replication: Theory And Practice ⋮ Quantitative global memory ⋮ Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\) ⋮ Tight typings and split bounds, fully developed ⋮ Unnamed Item ⋮ Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation ⋮ Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca ⋮ A typed lambda calculus with intersection types ⋮ Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage ⋮ Implementing the `Fool's model' of combinatory logic ⋮ The spirit of node replication ⋮ From CML to its process algebra ⋮ How to think of intersection types as Cartesian products ⋮ Type reconstruction in finite rank fragments of the second-order \(\lambda\)-calculus ⋮ Full abstraction for polymorphic \(\pi \)-calculus ⋮ Constructing type systems over an operational semantics ⋮ Types with intersection: An introduction ⋮ Hyperformulae, Parallel Deductions and Intersection Types ⋮ Classical \(F_{\omega}\), orthogonality and symmetric candidates ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The bang calculus revisited ⋮ Unnamed Item ⋮ Reasoning About Call-by-need by Means of Types ⋮ Ordinal analysis of simple cases of bar recursion ⋮ Intersection Types for the Resource Control Lambda Calculi ⋮ Reducibility ⋮ Typing untyped \(\lambda\)-terms, or reducibility strikes again! ⋮ Normalization without reducibility ⋮ Coppo-Dezani types do not correspond to propositional logic ⋮ Definability and Full Abstraction
Cites Work
This page was built for publication: A new type assignment for λ-terms
