ITU

Guarded recursion in Agda via sized types

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

Standard

Guarded recursion in Agda via sized types. / Veltri, Niccolò; van der Weide, Niels.

In: Leibniz International Proceedings in Informatics (LIPIcs), Vol. 131, 32, 2019, p. 32:1–32:19.

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

Harvard

APA

Vancouver

Author

Bibtex

@inproceedings{b50625a95b39486186795d77c6264e33,
title = "Guarded recursion in Agda via sized types",
abstract = "In type theory, programming and reasoning with possibly non-terminating programs and potentially infinite objects is achieved using coinductive types. Recursively defined programs of these types need to be productive to guarantee the consistency of the type system. Proof assistants such as Agda and Coq traditionally employ strict syntactic productivity checks, which often make programming with coinductive types convoluted. One way to overcome this issue is by encoding productivity at the level of types so that the type system forbids the implementation of non-productive corecursive programs. In this paper we compare two different approaches to type-based productivity: guarded recursion and sized types. More specifically, we show how to simulate guarded recursion in Agda using sized types. We formalize the syntax of a simple type theory for guarded recursion, which is a variant of Atkey and McBride{\textquoteright}s calculus for productive coprogramming. Then we give a denotational semantics using presheaves over the preorder of sizes. Sized types are fundamentally used to interpret the characteristic features of guarded recursion, notably the fixpoint combinator.",
author = "Niccol{\`o} Veltri and {van der Weide}, Niels",
year = "2019",
doi = "10.4230/LIPIcs.FSCD.2019.32",
language = "English",
volume = "131",
pages = "32:1–32:19",
journal = "Leibniz International Proceedings in Informatics",
issn = "1868-8969",
publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH",

}

RIS

TY - GEN

T1 - Guarded recursion in Agda via sized types

AU - Veltri, Niccolò

AU - van der Weide, Niels

PY - 2019

Y1 - 2019

N2 - In type theory, programming and reasoning with possibly non-terminating programs and potentially infinite objects is achieved using coinductive types. Recursively defined programs of these types need to be productive to guarantee the consistency of the type system. Proof assistants such as Agda and Coq traditionally employ strict syntactic productivity checks, which often make programming with coinductive types convoluted. One way to overcome this issue is by encoding productivity at the level of types so that the type system forbids the implementation of non-productive corecursive programs. In this paper we compare two different approaches to type-based productivity: guarded recursion and sized types. More specifically, we show how to simulate guarded recursion in Agda using sized types. We formalize the syntax of a simple type theory for guarded recursion, which is a variant of Atkey and McBride’s calculus for productive coprogramming. Then we give a denotational semantics using presheaves over the preorder of sizes. Sized types are fundamentally used to interpret the characteristic features of guarded recursion, notably the fixpoint combinator.

AB - In type theory, programming and reasoning with possibly non-terminating programs and potentially infinite objects is achieved using coinductive types. Recursively defined programs of these types need to be productive to guarantee the consistency of the type system. Proof assistants such as Agda and Coq traditionally employ strict syntactic productivity checks, which often make programming with coinductive types convoluted. One way to overcome this issue is by encoding productivity at the level of types so that the type system forbids the implementation of non-productive corecursive programs. In this paper we compare two different approaches to type-based productivity: guarded recursion and sized types. More specifically, we show how to simulate guarded recursion in Agda using sized types. We formalize the syntax of a simple type theory for guarded recursion, which is a variant of Atkey and McBride’s calculus for productive coprogramming. Then we give a denotational semantics using presheaves over the preorder of sizes. Sized types are fundamentally used to interpret the characteristic features of guarded recursion, notably the fixpoint combinator.

U2 - 10.4230/LIPIcs.FSCD.2019.32

DO - 10.4230/LIPIcs.FSCD.2019.32

M3 - Conference article

VL - 131

SP - 32:1–32:19

JO - Leibniz International Proceedings in Informatics

JF - Leibniz International Proceedings in Informatics

SN - 1868-8969

M1 - 32

ER -

ID: 84226711