CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Formalizing strong normalization proofs of explicit substitution calculi in ALF

F. Kamareddine ; Haiyan Qiao (Institutionen för datavetenskap)
Journal of automated reasoning (0168-7433). Vol. 30 (2003), 1, p. 59-98.
[Artikel, refereegranskad vetenskaplig]

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.

Nyckelord: ALF, Explicit substitution, Formalizing proofs, Theorem proving

Denna post skapades 2013-02-18.
CPL Pubid: 173734


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för datavetenskap (2002-2004)


Data- och informationsvetenskap

Chalmers infrastruktur