Intersection types for explicit substitutions
From MaRDI portal
Recommendations
- scientific article; zbMATH DE number 2086241
- Reductions, intersection types, and explicit substitutions
- Intersection type systems and explicit substitutions calculi
- Simple Proofs of Characterizing Strong Normalization for Explicit Substitution Calculi
- An elementary proof of strong normalization for intersection types
Cites work
- scientific article; zbMATH DE number 1722651 (Why is no real title available?)
- scientific article; zbMATH DE number 2185670 (Why is no real title available?)
- scientific article; zbMATH DE number 2086241 (Why is no real title available?)
- scientific article; zbMATH DE number 3659007 (Why is no real title available?)
- scientific article; zbMATH DE number 3735770 (Why is no real title available?)
- scientific article; zbMATH DE number 46869 (Why is no real title available?)
- scientific article; zbMATH DE number 47007 (Why is no real title available?)
- scientific article; zbMATH DE number 108434 (Why is no real title available?)
- scientific article; zbMATH DE number 192927 (Why is no real title available?)
- scientific article; zbMATH DE number 3596799 (Why is no real title available?)
- scientific article; zbMATH DE number 1229489 (Why is no real title available?)
- scientific article; zbMATH DE number 1342288 (Why is no real title available?)
- scientific article; zbMATH DE number 482822 (Why is no real title available?)
- scientific article; zbMATH DE number 1070568 (Why is no real title available?)
- scientific article; zbMATH DE number 1130260 (Why is no real title available?)
- scientific article; zbMATH DE number 1759417 (Why is no real title available?)
- A new type assignment for λ-terms
- An extension of basic functionality theory for -calculus
- Complete restrictions of the intersection type discipline
- Explicit substitution. On the edge of strong normalization
- Explicit substitutions
- Explicit substitutions and reducibility
- Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms
- Intensional interpretations of functionals of finite type I
- Intersection type assignment systems
- Proving termination with multiset orderings
- Reductions, intersection types, and explicit substitutions
- Strong normalization and typability with intersection types
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Typing and computational properties of lambda expressions
- Typing untyped \(\lambda\)-terms, or reducibility strikes again!
- λν, a calculus of explicit substitutions which preserves strong normalisation
Cited in
(17)- Types, potency, and idempotency: why nonlinearity and amnesia make a type system work
- Quantitative types for the linear substitution calculus
- Factoring derivation spaces via intersection types
- Reductions, intersection types, and explicit substitutions
- Characterising Strongly Normalising Intuitionistic Sequent Terms
- Nominal essential intersection types
- Principal Typings for Explicit Substitutions Calculi
- Simple Proofs of Characterizing Strong Normalization for Explicit Substitution Calculi
- Intersection types for the resource control lambda calculi
- Computation with classical sequents
- On realisability semantics for intersection types with expansion variables
- Non-idempotent intersection types and strong normalisation
- Intersection type systems and explicit substitutions calculi
- Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca
- Resource operators for \(\lambda\)-calculus
- A resource aware semantics for a focused intuitionistic calculus
- Intersection type system with de Bruijn indices
This page was built for publication: Intersection types for explicit substitutions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1887145)
