Formalizing strong normalization proofs of explicit substitution calculi in ALF

Fairouz Kamareddine, Haiyan Qiao

Research output: Contribution to journalArticle

1 Citation (Scopus)

Abstract

The past decade has given rise to a number of explicit substitution calculi. An important question of explicit substitution calculi is that of the termination of the underlying calculus of substitution. Proofs of termination of substitutions fall in two categories: those that are easy because a decreasing measure can be established and those that are difficult because such a decreasing measure is not easy to establish. This paper considers two styles of explicit substitution: s and s, for which different termination proof methods apply. The termination of s is guaranteed by a decreasing weight, while a decreasing weight for showing the termination of s has not yet been found. These termination methods for s and s are formalized in the proof checker ALF. During our process of formally checking the termination of s and s we comment on what is needed to make a proof formally checkable.

Original languageEnglish
Pages (from-to)59-98
Number of pages40
JournalJournal of Automated Reasoning
Volume30
Issue number1
DOIs
Publication statusPublished - Jan 2003

Keywords

  • ALF
  • Explicit substitution
  • Formalizing proofs
  • Theorem proving

Fingerprint Dive into the research topics of 'Formalizing strong normalization proofs of explicit substitution calculi in ALF'. Together they form a unique fingerprint.

Cite this