Automath and pure type systems

Fairouz Kamareddine; Twan Laan; Rob Nederpelt

doi:10.1016/S1571-0661(04)80756-4

Automath and pure type systems

Fairouz Kamareddine
, Twan Laan
, Rob Nederpelt

Research output: Contribution to journal › Article › peer-review

Abstract

We study the position of the AUTOMATH systems within the framework of Pure Type Systems (PTSs). In [1,15], a rough relationship has been given between AUTOMATH and PTSs. That relationship ignores three of the most important features of AUTOMATH: definitions, parameters and Pi-reduction, because at the time, PTSs did not have these features. Since, PTSs have been extended with these features and in view of this, we revisit the correspondence between AUTOMATH and PTSs. This paper gives the most accurate description of AUTOMATH as a PTS so far. ©2003 Published by Elsevier Science B. V.

Original language	English
Pages (from-to)	33-52
Number of pages	20
Journal	Electronic Notes in Theoretical Computer Science
Volume	85
Issue number	7
DOIs	https://doi.org/10.1016/S1571-0661(04)80756-4
Publication status	Published - Sept 2003

Access to Document

10.1016/S1571-0661(04)80756-4

Cite this

@article{dab11c197f164a5a95c226401e3fd894,

title = "Automath and pure type systems",

abstract = "We study the position of the AUTOMATH systems within the framework of Pure Type Systems (PTSs). In [1,15], a rough relationship has been given between AUTOMATH and PTSs. That relationship ignores three of the most important features of AUTOMATH: definitions, parameters and Pi-reduction, because at the time, PTSs did not have these features. Since, PTSs have been extended with these features and in view of this, we revisit the correspondence between AUTOMATH and PTSs. This paper gives the most accurate description of AUTOMATH as a PTS so far. {\textcopyright}2003 Published by Elsevier Science B. V.",

author = "Fairouz Kamareddine and Twan Laan and Rob Nederpelt",

year = "2003",

month = sep,

doi = "10.1016/S1571-0661(04)80756-4",

language = "English",

volume = "85",

pages = "33--52",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier B.V.",

number = "7",

}

TY - JOUR

T1 - Automath and pure type systems

AU - Kamareddine, Fairouz

AU - Laan, Twan

AU - Nederpelt, Rob

PY - 2003/9

Y1 - 2003/9

N2 - We study the position of the AUTOMATH systems within the framework of Pure Type Systems (PTSs). In [1,15], a rough relationship has been given between AUTOMATH and PTSs. That relationship ignores three of the most important features of AUTOMATH: definitions, parameters and Pi-reduction, because at the time, PTSs did not have these features. Since, PTSs have been extended with these features and in view of this, we revisit the correspondence between AUTOMATH and PTSs. This paper gives the most accurate description of AUTOMATH as a PTS so far. ©2003 Published by Elsevier Science B. V.

AB - We study the position of the AUTOMATH systems within the framework of Pure Type Systems (PTSs). In [1,15], a rough relationship has been given between AUTOMATH and PTSs. That relationship ignores three of the most important features of AUTOMATH: definitions, parameters and Pi-reduction, because at the time, PTSs did not have these features. Since, PTSs have been extended with these features and in view of this, we revisit the correspondence between AUTOMATH and PTSs. This paper gives the most accurate description of AUTOMATH as a PTS so far. ©2003 Published by Elsevier Science B. V.

UR - https://www.scopus.com/pages/publications/19044384187

U2 - 10.1016/S1571-0661(04)80756-4

DO - 10.1016/S1571-0661(04)80756-4

M3 - Article

SN - 1571-0661

VL - 85

SP - 33

EP - 52

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

IS - 7

ER -

Automath and pure type systems

Abstract

Access to Document

Other files and links

Fingerprint

Cite this