The weak normalization of the simply typed λse-calculus

Ariel Arbiser, Fairouz Kamareddine, Alejandro Rios

Research output: Contribution to journalArticle

Abstract

In this paper, we show the weak normalization (WN) of the simply-typed ?se-calculus with open terms where abstractions are decorated with types, and metavariables, de Bruijn indices and updating operators are decorated with environments. We show a proof of WN using the ??e-calculus, a calculus isomorphic to ?se?. This proof is strongly influenced by Goubault-Larrecq's proof of WN for the ?s-calculus but with subtle differences which show that the two styles require different attention. Furthermore, we give a new calculus ??'e which works like ?se but which is closer to ?s than ??e. For both ??e and ??'e we prove WN for typed semi-open terms (i.e. those which allow term variables but no substitution variables), unlike the result of Goubault-Larrecq which covered all ?s open terms. © The Author, 2007. Published by Oxford University Press. All rights reserved.

Original languageEnglish
Pages (from-to)121-147
Number of pages27
JournalLogic Journal of the IGPL
Volume15
Issue number2
DOIs
Publication statusPublished - Mar 2007

Keywords

  • Explicit substitution
  • Lambda calculus
  • Normalization
  • Simple typing

Fingerprint Dive into the research topics of 'The weak normalization of the simply typed λs<sub>e</sub>-calculus'. Together they form a unique fingerprint.

  • Cite this