Intersection type system with de Bruijn indices

MaRDI QIDQ3086726zbMATH OpenFDO

Authors Daniel Lima Ventura, Mauricio Ayala-Rincón, Fairouz Kamareddine

Publication date 30 March 2011

zbMATH Keywords

\(\lambda\)-calculussubject reduction propertyfree indexde Bruijn notationintersection type system

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• Intersection type systems and explicit substitutions calculi
• Explicit substitution calculi with de Bruijn indices and intersection type systems
• Intersection types for explicit substitutions
• Bridging de Bruijn indices and variable names in explicit substitutions calculi
• Reviewing the classical and the de Bruijn notation for \(\lambda\)-calculus and pure type systems

Cited in

(5)

• Explicit substitution calculi with de Bruijn indices and intersection type systems
• de Bruijn notation as a nested datatype
• Reviewing the classical and the de Bruijn notation for \(\lambda\)-calculus and pure type systems
• Pure Type Systems with de Bruijn Indices
• Intersection type systems and explicit substitutions calculi

Describes a project that uses

Uses Software

• Automath

This page was built for publication: Intersection type system with de Bruijn indices

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3086726)