Dependent types and explicit substitutions: A meta-theoretical development (Q2713354)

This is an interesting paper which appears in a special issue of MSCS on explicit substitutions. The author considers a system \(\lambda \Pi_\mathcal L \), a variant of \(\lambda P\) that supports explicit substitutions and meta-variables. Meta-variables are place holders in a proof-term and explicit substitution is necessary to delay the application of substitutions of meta-variables waiting to be instantiated. The syntax of \(\lambda \Pi_\mathcal L \) ist presented using de Bruijn indices instead of name variables as for the original calculus \(\lambda \sigma\) in the paper ``Explicit substitution'' by \textit{M. Abadi, L. Cardelli, P.-L. Curien} and \textit{J.-J. Lévy} [J. Funct. Program. 1, 375-416 (1991; Zbl 0941.68542)]. NEWLINENEWLINENEWLINEIn this paper the author studies the properties of confluence (on typed terms) and weak normalization.