A type theory for productive coprogramming via guarded recursion

Rasmus Ejlers Møgelberg

doi:10.1145/2603088.2603132

A type theory for productive coprogramming via guarded recursion

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

Original language	Danish
Title of host publication	Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) : CSL-LICS '14
Number of pages	10
Publisher	Association for Computing Machinery
Publication date	2014
Article number	71
ISBN (Print)	978-1-4503-2886-9
DOIs	https://doi.org/10.1145/2603088.2603132
Publication status	Published - 2014
Event	Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) - Vienna, Austria Duration: 14 Jul 2014 → 18 Jul 2014

Conference

Conference	Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Country/Territory	Austria
City	Vienna
Period	14/07/2014 → 18/07/2014

Series	Annual Symposium on Logic in Computer Science
ISSN	1043-6871

Keywords

Guarded recursion
corecursion
dependent types
denotational semantics
categorical semantics

Access to Document

10.1145/2603088.2603132

Cite this

Møgelberg, R. E. (2014). A type theory for productive coprogramming via guarded recursion. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS): CSL-LICS '14 Article 71 Association for Computing Machinery. https://doi.org/10.1145/2603088.2603132

Møgelberg, Rasmus Ejlers. / A type theory for productive coprogramming via guarded recursion. Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS): CSL-LICS '14. Association for Computing Machinery, 2014. (Annual Symposium on Logic in Computer Science).

@inproceedings{0bec11f9a1a344aeb31791978e3f24a9,

title = "A type theory for productive coprogramming via guarded recursion",

keywords = "Guarded recursion, corecursion, dependent types, denotational semantics, categorical semantics, Guarded recursion, corecursion, dependent types, denotational semantics, categorical semantics",

author = "M{\o}gelberg, {Rasmus Ejlers}",

year = "2014",

doi = "10.1145/2603088.2603132",

language = "Dansk",

isbn = "978-1-4503-2886-9",

series = "Annual Symposium on Logic in Computer Science",

publisher = "Association for Computing Machinery",

booktitle = "Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)",

address = "USA",

note = "Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14 ; Conference date: 14-07-2014 Through 18-07-2014",

}

Møgelberg, RE 2014, A type theory for productive coprogramming via guarded recursion. in Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS): CSL-LICS '14., 71, Association for Computing Machinery, Annual Symposium on Logic in Computer Science, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Vienna, Austria, 14/07/2014. https://doi.org/10.1145/2603088.2603132

A type theory for productive coprogramming via guarded recursion. / Møgelberg, Rasmus Ejlers.
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS): CSL-LICS '14. Association for Computing Machinery, 2014. 71 (Annual Symposium on Logic in Computer Science).

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

TY - GEN

T1 - A type theory for productive coprogramming via guarded recursion

AU - Møgelberg, Rasmus Ejlers

PY - 2014

Y1 - 2014

KW - Guarded recursion

KW - corecursion

KW - dependent types

KW - denotational semantics

KW - categorical semantics

KW - Guarded recursion

KW - corecursion

KW - dependent types

KW - denotational semantics

KW - categorical semantics

U2 - 10.1145/2603088.2603132

DO - 10.1145/2603088.2603132

M3 - Konferencebidrag i proceedings

SN - 978-1-4503-2886-9

T3 - Annual Symposium on Logic in Computer Science

BT - Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

PB - Association for Computing Machinery

T2 - Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

Y2 - 14 July 2014 through 18 July 2014

ER -

Møgelberg RE. A type theory for productive coprogramming via guarded recursion. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS): CSL-LICS '14. Association for Computing Machinery. 2014. 71. (Annual Symposium on Logic in Computer Science). doi: 10.1145/2603088.2603132