A new type assignment for λ-terms
From MaRDI portal
Publication:3208623
DOI10.1007/BF02011875zbMATH Open0418.03010OpenAlexW1981303668MaRDI QIDQ3208623FDOQ3208623
Authors: Mario Coppo, Mariangiola Dezani-Ciancaglini 
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
Cites Work
Cited In (49)
- Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)
- Ordinal analysis of simple cases of bar recursion
- Title not available (Why is that?)
- System ST toward a type system for extraction and proofs of programs
- Tight typings and split bounds, fully developed
- Title not available (Why is that?)
- Title not available (Why is that?)
- How to think of intersection types as Cartesian products
- The spirit of node replication
- Infinite intersection types
- Call-by-value non-determinism in a linear logic type discipline
- Constructing type systems over an operational semantics
- Full abstraction for polymorphic \(\pi \)-calculus
- Characterising Strongly Normalising Intuitionistic Sequent Terms
- A characterization of F-complete type assignments
- Type theories, normal forms, and \(D_{\infty}\)-lambda-models
- Nominal essential intersection types
- A classification of intersection type systems
- Higher-order subtyping and its decidability
- Typing untyped \(\lambda\)-terms, or reducibility strikes again!
- A completeness result for a realisability semantics for an intersection type system
- Intersection types for the resource control lambda calculi
- Title not available (Why is that?)
- Reasoning about call-by-need by means of types
- Node Replication: Theory And Practice
- Implementing the `Fool's model' of combinatory logic
- The bang calculus revisited
- Definability and full abstraction
- Higher-order subtyping
- Quantitative global memory
- Intersection types for explicit substitutions
- Coppo-Dezani types do not correspond to propositional logic
- On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory
- Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage
- Type reconstruction in finite rank fragments of the second-order \(\lambda\)-calculus
- Title not available (Why is that?)
- Title not available (Why is that?)
- A typed lambda calculus with intersection types
- Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca
- A resource aware semantics for a focused intuitionistic calculus
- Reducibility: a ubiquitous method in lambda calculus with intersection types
- Types with intersection: An introduction
- Normalization without reducibility
- A model for syntactic control of interference
- Title not available (Why is that?)
- Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation
- From CML to its process algebra
- Hyperformulae, parallel deductions and intersection types
- Classical \(F_{\omega}\), orthogonality and symmetric candidates
This page was built for publication: A new type assignment for λ-terms
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3208623)
