8485 articles  [english version]

inria-00073601, version 1

## A Proof of Weak Termination of the Simply-Typed {$\lambda\sigma$}-Calculus

Jean Goubault-Larrecq 1

N° RR-3090 (1997)

Résumé : We show that reducing any simply-typed $\lambda\sigma$-term by applying the rules in $\sigma$ eagerly always terminates, by a translation to the simply-typed $\lambda$-calculus, and similarly for $\lambda\sigma_\lift$-terms with $\sigma_\lift$-eager rewrites. This holds even with term and substitution meta-variables. In fact, every reduction terminates provided that $(\beta)$-redexes are only contracted under so-called safe contexts. The previous results follow because in $\sigma$, resp. $\sigma_{\lift}$-normal forms, all contexts around terms of sort $T$ are safe.

• 1 :  COQ (INRIA Rocquencourt)
• INRIA
• Domaine : Informatique/Autre
• Mots-clés : LAMBDA-SIGMA-CALCULUS / EXPLICIT SUBSTITUTIONS / TERMINATION / LAMBDA-CALCULUS / SIMPLE TYPES
• Référence interne : RR-3090
• Commentaire : Projet COQ

• inria-00073601, version 1
• oai:hal.inria.fr:inria-00073601
• Contributeur :
• Soumis le : Mercredi 24 Mai 2006, 13:17:40
• Dernière modification le : Mardi 24 Avril 2007, 13:22:07