Intersection type system with de Bruijn indices

zbMATH Open1226.03029MaRDI QIDQ3086726FDOQ3086726

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

Publication date: 30 March 2011

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

zbMATH Keywords

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

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Cited In (5)

• 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
• Explicit substitution calculi with de Bruijn indices and intersection type systems

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)