inria-00073601, version 1

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

Jean Goubault-Larrecq ¹

N° RR-3090 (1997)

• 1:  COQ (INRIA Rocquencourt)
• 
  INRIA France

Bibliographic reference

• Type of document: Research reports
• Domain: Computer Science/Other
• Title: A Proof of Weak Termination of the Simply-Typed {$\lambda\sigma$}-Calculus
• Abstract: 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.
• Full text language: English
• Report type: Research Report
• Publication date: 1997
• Keywords: LAMBDA-SIGMA-CALCULUS / EXPLICIT SUBSTITUTIONS / TERMINATION / LAMBDA-CALCULUS / SIMPLE TYPES
• Writing date: 1997-01
• Comment: Projet COQ
• Internal note: RR-3090

Attached file list to this document: 

• inria-00073601, version 1
• http://hal.inria.fr/inria-00073601
• oai:hal.inria.fr:inria-00073601
• From: Rapport De Recherche Inria <>
• Submitted on: Wednesday, 24 May 2006 13:17:40
• Updated on: Tuesday, 24 April 2007 13:22:07