Simple proofs of characterizing strong normalization for explicit substitution calculi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)

Abstract

We present a method of lifting to explicit substitution calculi some characterizations of the strongly normalizing terms of A-calculus by means of intersection type systems. The method is first illustrated by applying to a composition-free calculus of explicit substitutions, yielding a simpler proof than the previous one by Lengrand et al. Then we present a new intersection type system in the style of sequent calculus, and show that it characterizes the strongly normalizing terms of Dyckhoff and Urban's extension of Herbelin's explicit substitution calculus.

Original languageEnglish
Title of host publicationTerm Rewriting and Applications - 18th International Conference, RTA 2007, Proceedings
Pages257-272
Number of pages16
Publication statusPublished - 2007 Dec 1
Event18th International Conference on Rewriting Techniques and Applications, RTA 2007 - Paris, France
Duration: 2007 Jun 262007 Jun 28

Publication series

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

Other

Other18th International Conference on Rewriting Techniques and Applications, RTA 2007
CountryFrance
CityParis
Period07/6/2607/6/28

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Simple proofs of characterizing strong normalization for explicit substitution calculi'. Together they form a unique fingerprint.

Cite this