Aarhus University Seal / Aarhus Universitets segl

Relational Interpretations of Recursive Types in an Operational Setting

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

Standard

Relational Interpretations of Recursive Types in an Operational Setting. / Birkedal, Lars; Harper, Robert.

In: Information and Computation, Vol. 155, No. 1-2, 25.11.1999, p. 3-63.

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

Harvard

APA

CBE

Birkedal L, Harper R. 1999. Relational Interpretations of Recursive Types in an Operational Setting. Information and Computation. 155(1-2):3-63.

MLA

Birkedal, Lars and Robert Harper. "Relational Interpretations of Recursive Types in an Operational Setting". Information and Computation. 1999, 155(1-2). 3-63.

Vancouver

Birkedal L, Harper R. Relational Interpretations of Recursive Types in an Operational Setting. Information and Computation. 1999 Nov 25;155(1-2):3-63.

Author

Birkedal, Lars ; Harper, Robert. / Relational Interpretations of Recursive Types in an Operational Setting. In: Information and Computation. 1999 ; Vol. 155, No. 1-2. pp. 3-63.

Bibtex

@article{b8f7da767f1e48f3a27ff3908bebdbfb,
title = "Relational Interpretations of Recursive Types in an Operational Setting",
abstract = "Relational interpretations of type systems are useful for establishing properties of programming languages. For languages with recursive types it is difficult to establish the existence of a relational interpretation. The usual approach is to pass to a domain-theoretic model of the language and, exploiting the structure of the model, to derive relational properties of it. We investigate the construction of relational interpretations of recursive types in a purely operational setting, drawing on recent ideas from domain theory and operational semantics as a guide. We prove syntactic minimal invariance for an extension of PCF with a recursive type, a syntactic analogue of the minimal invariance property used by Freyd and Pitts to characterize the domain interpretation of a recursive type. As Pitts has shown in the setting of domains, syntactic minimal invariance suffices to establish the existence of relational interpretations. We give two applications of this construction. First, we derive a notion of logical equivalence for expressions of the language that we show coincides with experimental equivalence and which, by virtue of its construction, validates useful induction and coinduction principles for reasoning about the recursive type. Second, we give a relational proof of correctness of the continuation-passing transformation, which is used in some compilers for functional languages.",
author = "Lars Birkedal and Robert Harper",
year = "1999",
month = nov,
day = "25",
language = "English",
volume = "155",
pages = "3--63",
journal = "Information and Computation",
issn = "0890-5401",
publisher = "Academic Press",
number = "1-2",

}

RIS

TY - JOUR

T1 - Relational Interpretations of Recursive Types in an Operational Setting

AU - Birkedal, Lars

AU - Harper, Robert

PY - 1999/11/25

Y1 - 1999/11/25

N2 - Relational interpretations of type systems are useful for establishing properties of programming languages. For languages with recursive types it is difficult to establish the existence of a relational interpretation. The usual approach is to pass to a domain-theoretic model of the language and, exploiting the structure of the model, to derive relational properties of it. We investigate the construction of relational interpretations of recursive types in a purely operational setting, drawing on recent ideas from domain theory and operational semantics as a guide. We prove syntactic minimal invariance for an extension of PCF with a recursive type, a syntactic analogue of the minimal invariance property used by Freyd and Pitts to characterize the domain interpretation of a recursive type. As Pitts has shown in the setting of domains, syntactic minimal invariance suffices to establish the existence of relational interpretations. We give two applications of this construction. First, we derive a notion of logical equivalence for expressions of the language that we show coincides with experimental equivalence and which, by virtue of its construction, validates useful induction and coinduction principles for reasoning about the recursive type. Second, we give a relational proof of correctness of the continuation-passing transformation, which is used in some compilers for functional languages.

AB - Relational interpretations of type systems are useful for establishing properties of programming languages. For languages with recursive types it is difficult to establish the existence of a relational interpretation. The usual approach is to pass to a domain-theoretic model of the language and, exploiting the structure of the model, to derive relational properties of it. We investigate the construction of relational interpretations of recursive types in a purely operational setting, drawing on recent ideas from domain theory and operational semantics as a guide. We prove syntactic minimal invariance for an extension of PCF with a recursive type, a syntactic analogue of the minimal invariance property used by Freyd and Pitts to characterize the domain interpretation of a recursive type. As Pitts has shown in the setting of domains, syntactic minimal invariance suffices to establish the existence of relational interpretations. We give two applications of this construction. First, we derive a notion of logical equivalence for expressions of the language that we show coincides with experimental equivalence and which, by virtue of its construction, validates useful induction and coinduction principles for reasoning about the recursive type. Second, we give a relational proof of correctness of the continuation-passing transformation, which is used in some compilers for functional languages.

M3 - Journal article

AN - SCOPUS:0000650306

VL - 155

SP - 3

EP - 63

JO - Information and Computation

JF - Information and Computation

SN - 0890-5401

IS - 1-2

ER -