Dependent types and explicit substitutions: a meta-theoretical development

DOI10.1017/S0960129500003261zbMath0976.03014OpenAlexW2106803738MaRDI QIDQ2713354

César A. Muñoz

Publication date: 21 December 2001

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129500003261

zbMATH Keywords

weak normalizationconfluenceexplicit substitutionsde Bruijn indicesmeta-variables

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Related Items (2)

Strongly-Normalizing Higher-Order Relational Queries ⋮ Pure type systems with explicit substitutions

Uses Software

• Automath
• ALF

This page was built for publication: Dependent types and explicit substitutions: a meta-theoretical development