ITU

Denotational semantics of recursive types in synthetic guarded domain theory

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

Standard

Denotational semantics of recursive types in synthetic guarded domain theory. / Møgelberg, Rasmus Ejlers; Paviotti, Marco.

In: Mathematical Structures in Computer Science, 15.05.2018.

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

Harvard

APA

Vancouver

Author

Bibtex

@article{5c14d286520849afafd856e30301a05f,
title = "Denotational semantics of recursive types in synthetic guarded domain theory",
abstract = "Just like any other branch of mathematics, denotational semantics of programming languages should be formalised in type theory, but adapting traditional domain theoretic semantics, as originally formulated in classical set theory to type theory has proven challenging. This paper is part of a project on formulating denotational semantics in type theories with guarded recursion. This should have the benefit of not only giving simpler semantics and proofs of properties such as adequacy, but also hopefully in the future to scale to languages with advanced features, such as general references, outside the reach of traditional domain theoretic techniques.Working in Guarded Dependent Type Theory (GDTT), we develop denotational semantics for Fixed Point Calculus (FPC), the simply typed lambda calculus extended with recursive types, modelling the recursive types of FPC using the guarded recursive types of GDTT. We prove soundness and computational adequacy of the model in GDTT using a logical relation between syntax and semantics constructed also using guarded recursive types. The denotational semantics is intensional in the sense that it counts the number of unfold-fold reductions needed to compute the value of a term, but we construct a relation relating the denotations of extensionally equal terms, i.e., pairs of terms that compute the same value in a different number of steps. Finally, we show how the denotational semantics of terms can be executed inside type theory and prove that executing the denotation of a boolean term computes the same value as the operational semantics of FPC.",
author = "M{\o}gelberg, {Rasmus Ejlers} and Marco Paviotti",
year = "2018",
month = may,
day = "15",
doi = "10.1017/S0960129518000087",
language = "Dansk",
journal = "Mathematical Structures in Computer Science",
issn = "0960-1295",
publisher = "Cambridge University Press",

}

RIS

TY - JOUR

T1 - Denotational semantics of recursive types in synthetic guarded domain theory

AU - Møgelberg, Rasmus Ejlers

AU - Paviotti, Marco

PY - 2018/5/15

Y1 - 2018/5/15

N2 - Just like any other branch of mathematics, denotational semantics of programming languages should be formalised in type theory, but adapting traditional domain theoretic semantics, as originally formulated in classical set theory to type theory has proven challenging. This paper is part of a project on formulating denotational semantics in type theories with guarded recursion. This should have the benefit of not only giving simpler semantics and proofs of properties such as adequacy, but also hopefully in the future to scale to languages with advanced features, such as general references, outside the reach of traditional domain theoretic techniques.Working in Guarded Dependent Type Theory (GDTT), we develop denotational semantics for Fixed Point Calculus (FPC), the simply typed lambda calculus extended with recursive types, modelling the recursive types of FPC using the guarded recursive types of GDTT. We prove soundness and computational adequacy of the model in GDTT using a logical relation between syntax and semantics constructed also using guarded recursive types. The denotational semantics is intensional in the sense that it counts the number of unfold-fold reductions needed to compute the value of a term, but we construct a relation relating the denotations of extensionally equal terms, i.e., pairs of terms that compute the same value in a different number of steps. Finally, we show how the denotational semantics of terms can be executed inside type theory and prove that executing the denotation of a boolean term computes the same value as the operational semantics of FPC.

AB - Just like any other branch of mathematics, denotational semantics of programming languages should be formalised in type theory, but adapting traditional domain theoretic semantics, as originally formulated in classical set theory to type theory has proven challenging. This paper is part of a project on formulating denotational semantics in type theories with guarded recursion. This should have the benefit of not only giving simpler semantics and proofs of properties such as adequacy, but also hopefully in the future to scale to languages with advanced features, such as general references, outside the reach of traditional domain theoretic techniques.Working in Guarded Dependent Type Theory (GDTT), we develop denotational semantics for Fixed Point Calculus (FPC), the simply typed lambda calculus extended with recursive types, modelling the recursive types of FPC using the guarded recursive types of GDTT. We prove soundness and computational adequacy of the model in GDTT using a logical relation between syntax and semantics constructed also using guarded recursive types. The denotational semantics is intensional in the sense that it counts the number of unfold-fold reductions needed to compute the value of a term, but we construct a relation relating the denotations of extensionally equal terms, i.e., pairs of terms that compute the same value in a different number of steps. Finally, we show how the denotational semantics of terms can be executed inside type theory and prove that executing the denotation of a boolean term computes the same value as the operational semantics of FPC.

U2 - 10.1017/S0960129518000087

DO - 10.1017/S0960129518000087

M3 - Tidsskriftartikel

JO - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

SN - 0960-1295

ER -

ID: 83279672