A Direct Proof of Strong Normalization for an Extended Herbelin's Calculus

Research output: Chapter in Book/Report/Conference proceedingChapter

4 Citations (Scopus)

Abstract

Herbelin presented (at CSL'94) an explicit substitution calculus with a sequent calculus as a type system, in which reduction steps correspond to cut-elimination steps. The calculus, extended with some rules for substitution propagation, simulates β-reduction of ordinary λcalculus. In this paper we present a proof of strong normalization for the typable terms of the calculus. The proof is a direct one in the sense that it does not depend on the result of strong normalization for the simply typed A-calculus, unlike an earlier proof by Dyckhoff and Urban.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsYukiyoshi Kameyama, Peter J. Stuckey
PublisherSpringer Verlag
Pages244-259
Number of pages16
ISBN (Electronic)354021402X, 9783540214021
DOIs
Publication statusPublished - 2004 Jan 1
Externally publishedYes

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2998
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A Direct Proof of Strong Normalization for an Extended Herbelin's Calculus'. Together they form a unique fingerprint.

Cite this