A new type assignment for λ-terms
From MaRDI portal
Publication:3208623
Cites work
- scientific article; zbMATH DE number 3532922 (Why is no real title available?)
- scientific article; zbMATH DE number 3557747 (Why is no real title available?)
- scientific article; zbMATH DE number 3423994 (Why is no real title available?)
- scientific article; zbMATH DE number 3103212 (Why is no real title available?)
- A formulation of the simple theory of types
- Combinatory logic. Vol. II
- Combinatory logic. With two sections by William Craig.
Cited in
(49)- Classical \(F_{\omega}\), orthogonality and symmetric candidates
- Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)
- Hyperformulae, parallel deductions and intersection types
- Ordinal analysis of simple cases of bar recursion
- scientific article; zbMATH DE number 7561342 (Why is no real title available?)
- System ST toward a type system for extraction and proofs of programs
- Tight typings and split bounds, fully developed
- scientific article; zbMATH DE number 7526055 (Why is no real title available?)
- scientific article; zbMATH DE number 7204443 (Why is no real title available?)
- 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
- A characterization of F-complete type assignments
- Characterising Strongly Normalising Intuitionistic Sequent Terms
- Higher-order subtyping and its decidability
- Type theories, normal forms, and \(D_{\infty}\)-lambda-models
- Nominal essential intersection types
- A classification of intersection type systems
- A completeness result for a realisability semantics for an intersection type system
- Typing untyped \(\lambda\)-terms, or reducibility strikes again!
- Intersection types for the resource control lambda calculi
- scientific article; zbMATH DE number 3697079 (Why is no real title available?)
- Reasoning about call-by-need by means of types
- Implementing the `Fool's model' of combinatory logic
- The bang calculus revisited
- Node Replication: Theory And Practice
- 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 - 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 -calculus
- scientific article; zbMATH DE number 3720894 (Why is no real title available?)
- scientific article; zbMATH DE number 7155170 (Why is no real title available?)
- 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
- Types with intersection: An introduction
- Reducibility: a ubiquitous method in lambda calculus with intersection types
- Normalization without reducibility
- A model for syntactic control of interference
- scientific article; zbMATH DE number 7526053 (Why is no real title available?)
- Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation
- From CML to its process algebra
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)