Pure Type Systems with Judgemental Equality. / Adams, Robin.

In: Journal of Functional Programming, Vol. 16, No. 2, 2006, p. 219-246.

Research output: Contribution to journalArticle

Published

Documents

Abstract

In a typing system, there are two approaches that may be taken to the
notion of equality. One can use some external relation of
convertibility defined on the terms of the grammar, such as
beta-convertibility or beta-eta-convertiblity; or one can
introduce a judgement form for equality into the rules of the typing
system itself.

For quite some time, it has been an open problem whether the two systems
produced by these two choices are equivalent. This problem is
essentially the problem of proving the Subject Reduction property
holds in the system with judgemental equality.

In this paper, we shall
prove that the equivalence holds for all functional Pure Type
Systems (PTSs). The proof essentially consists of proving the
Church-Rosser Theorem for a typed version of parallel one-step
reduction. This method should generalise easily to many typing
systems which satisfy the Uniqueness of Types property.
Original languageEnglish
Pages (from-to)219-246
Number of pages28
JournalJournal of Functional Programming
Volume16
Issue number2
DOIs
Publication statusPublished - 2006
This open access research output is licenced under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.

ID: 398780