Aarhus University Seal / Aarhus Universitets segl

Guarded dependent type theory with coinductive types

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

We present guarded dependent type theory, gDTT, an extensional dependent type theory with a ‘later’ modality and clock quantifiers for programming and proving with guarded recursive and coinductive types. The later modality is used to ensure the productivity of recursive definitions in a modular, type based, way. Clock quantifiers are used for controlled elimination of the later modality and for encoding coinductive types using guarded recursive types. Key to the development of gDTT are novel type and term formers involving what we call ‘delayed substitutions’. These generalise the applicative functor rules for the later modality considered in earlier work, and are crucial for programming and proving with dependent types. We show soundness of the type theory with respect to a denotational model.

Original languageEnglish
Title of host publicationFoundations of Software Science and Computation Structures : 19th International Conference, FOSSACS 2016
EditorsBart Jacobs, Christof Löding
Number of pages16
Volume9634
PublisherSpringer VS
Publication year2016
Pages20-35
ISBN (print)9783662496299
ISBN (Electronic)978-3-662-49630-5
DOIs
Publication statusPublished - 2016
Event19th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016 - Eindhoven, Netherlands
Duration: 2 Apr 20168 Apr 2016

Conference

Conference19th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016
LandNetherlands
ByEindhoven
Periode02/04/201608/04/2016
SeriesLecture Notes in Computer Science
Volume9634
ISSN0302-9743

See relations at Aarhus University Citationformats

ID: 108753827