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

Research output: Contribution to journal › Article

Published

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

Research output: Contribution to journal › Article

Adams, R 2006, 'Pure Type Systems with Judgemental Equality', *Journal of Functional Programming*, vol. 16, no. 2, pp. 219-246. https://doi.org/10.1017/S0956796805005770

Adams, R. (2006). Pure Type Systems with Judgemental Equality. *Journal of Functional Programming*, *16*(2), 219-246. https://doi.org/10.1017/S0956796805005770

Adams R. Pure Type Systems with Judgemental Equality. Journal of Functional Programming. 2006;16(2):219-246. https://doi.org/10.1017/S0956796805005770

@article{f4497770102244e7a592ad850fc7fa36,

title = "Pure Type Systems with Judgemental Equality",

abstract = "In a typing system, there are two approaches that may be taken to thenotion of equality. One can use some external relation ofconvertibility defined on the terms of the grammar, such asbeta-convertibility or beta-eta-convertiblity; or one canintroduce a judgement form for equality into the rules of the typingsystem itself.For quite some time, it has been an open problem whether the two systemsproduced by these two choices are equivalent. This problem isessentially the problem of proving the Subject Reduction propertyholds in the system with judgemental equality.In this paper, we shallprove that the equivalence holds for all functional Pure TypeSystems (PTSs). The proof essentially consists of proving theChurch-Rosser Theorem for a typed version of parallel one-stepreduction. This method should generalise easily to many typingsystems which satisfy the Uniqueness of Types property.",

keywords = "type theory, pure type systems, subject reduction",

author = "Robin Adams",

year = "2006",

doi = "10.1017/S0956796805005770",

language = "English",

volume = "16",

pages = "219--246",

journal = "Journal of Functional Programming",

issn = "0956-7968",

publisher = "Cambridge University Press",

number = "2",

}

TY - JOUR

T1 - Pure Type Systems with Judgemental Equality

AU - Adams, Robin

PY - 2006

Y1 - 2006

N2 - In a typing system, there are two approaches that may be taken to thenotion of equality. One can use some external relation ofconvertibility defined on the terms of the grammar, such asbeta-convertibility or beta-eta-convertiblity; or one canintroduce a judgement form for equality into the rules of the typingsystem itself.For quite some time, it has been an open problem whether the two systemsproduced by these two choices are equivalent. This problem isessentially the problem of proving the Subject Reduction propertyholds in the system with judgemental equality.In this paper, we shallprove that the equivalence holds for all functional Pure TypeSystems (PTSs). The proof essentially consists of proving theChurch-Rosser Theorem for a typed version of parallel one-stepreduction. This method should generalise easily to many typingsystems which satisfy the Uniqueness of Types property.

AB - In a typing system, there are two approaches that may be taken to thenotion of equality. One can use some external relation ofconvertibility defined on the terms of the grammar, such asbeta-convertibility or beta-eta-convertiblity; or one canintroduce a judgement form for equality into the rules of the typingsystem itself.For quite some time, it has been an open problem whether the two systemsproduced by these two choices are equivalent. This problem isessentially the problem of proving the Subject Reduction propertyholds in the system with judgemental equality.In this paper, we shallprove that the equivalence holds for all functional Pure TypeSystems (PTSs). The proof essentially consists of proving theChurch-Rosser Theorem for a typed version of parallel one-stepreduction. This method should generalise easily to many typingsystems which satisfy the Uniqueness of Types property.

KW - type theory

KW - pure type systems

KW - subject reduction

U2 - 10.1017/S0956796805005770

DO - 10.1017/S0956796805005770

M3 - Article

VL - 16

SP - 219

EP - 246

JO - Journal of Functional Programming

JF - Journal of Functional Programming

SN - 0956-7968

IS - 2

ER -