Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

TLCA

2009

Springer

2009

Springer

Abstract. Programming languages theory is full of problems that reduce to proving the consistency of a logic, such as the normalization of typed lambda-calculi, the decidability of equality in type theory, equivalence testing of traces in security, etc. Although the principle of transﬁnite induction is routinely employed by logicians in proving such theorems, it is rarely used by programming languages researchers who often prefer alternatives such as proofs by logical relations and model theoretic constructions. In this paper we harness the well-foundedness of the lexicographic path ordering to derive an induction principle that combines the comfort of structural induction with the expressive strength of transﬁnite induction. Using lexicographic path induction, we give a consistency proof of Martin-L¨of’s intuitionistic theory of inductive deﬁnitions. The consistency of Heyting arithmetic follows directly, and weak normalization for G¨odel’s T follows indirectly; both have ...

Related Content

Added |
27 May 2010 |

Updated |
27 May 2010 |

Type |
Conference |

Year |
2009 |

Where |
TLCA |

Authors |
Jeffrey Sarnat, Carsten Schürmann |

Comments (0)