### Skapa referens, olika format (klipp och klistra)

**Harvard**

Kamareddine, F. och Qiao, H. (2003) *Formalizing strong normalization proofs of explicit substitution calculi in ALF*.

** BibTeX **

@article{

Kamareddine2003,

author={Kamareddine, F. and Qiao, Haiyan},

title={Formalizing strong normalization proofs of explicit substitution calculi in ALF},

journal={Journal of automated reasoning},

issn={0168-7433},

volume={30},

issue={1},

pages={59-98},

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: σ 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 σ has not yet been found. These termination methods for σ and s are formalized in the proof checker ALF. During our process of formally checking the termination of σ and s we comment on what is needed to make a proof formally checkable.},

year={2003},

keywords={ALF, Explicit substitution, Formalizing proofs, Theorem proving},

}

** RefWorks **

RT Journal Article

SR Electronic

ID 173734

A1 Kamareddine, F.

A1 Qiao, Haiyan

T1 Formalizing strong normalization proofs of explicit substitution calculi in ALF

YR 2003

JF Journal of automated reasoning

SN 0168-7433

VO 30

IS 1

SP 59

OP 98

AB 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: σ 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 σ has not yet been found. These termination methods for σ and s are formalized in the proof checker ALF. During our process of formally checking the termination of σ and s we comment on what is needed to make a proof formally checkable.

LA eng

DO 10.1023/A:1022527914293

LK http://dx.doi.org/10.1023/A:1022527914293

OL 30