Greatest HITs: Higher Inductive Types in Coinductive Definitions via Induction under Clocks

Magnus Baunsgaard Kristensen; Rasmus Ejlers Møgelberg; Andrea Vezzosi

doi:10.1145/3531130.3533359

Greatest HITs: Higher Inductive Types in Coinductive Definitions via Induction under Clocks

Magnus Baunsgaard Kristensen
, Rasmus Ejlers Møgelberg
, Andrea Vezzosi

Programming Logic and Semantics

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 37th Annual ACM/IEEE Symposium on Logic in Computer Science
Number of pages	13
Publisher	Association for Computing Machinery
Publication date	2022
Article number	42
ISBN (Print)	9781450393515
DOIs	https://doi.org/10.1145/3531130.3533359
Publication status	Published - 2022
Event	Annual ACM/IEEE Symposium on Logic in Computer Science - Haifa, Israel Duration: 2 Aug 2022 → 5 Aug 2022 Conference number: 37 https://dl.acm.org/doi/proceedings/10.1145/3531130

Symposium

Symposium	Annual ACM/IEEE Symposium on Logic in Computer Science
Number	37
Country/Territory	Israel
City	Haifa
Period	02/08/2022 → 05/08/2022
Internet address	https://dl.acm.org/doi/proceedings/10.1145/3531130

Access to Document

10.1145/3531130.3533359

CubicalCloTTAccepted author manuscript, 799 KB

https://arxiv.org/abs/2102.01969

Type theories for reactive programming
Møgelberg, R. E. (PI), Vezzosi, A. (CoI), Graulund, C. U. (CoI), Kristensen, M. B. (CoI) & Veltri, N. (CoI)
Villum Foundation
22/01/2016 → 21/01/2022
Project: Research

Cite this

@inproceedings{5a4e8bf3158b420f9edb163d8f9a1f70,

title = "Greatest HITs: Higher Inductive Types in Coinductive Definitions via Induction under Clocks",

author = "Kristensen, \{Magnus Baunsgaard\} and M{\o}gelberg, \{Rasmus Ejlers\} and Andrea Vezzosi",

year = "2022",

doi = "10.1145/3531130.3533359",

language = "Dansk",

isbn = "9781450393515",

booktitle = "Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science",

publisher = "Association for Computing Machinery",

address = "USA",

note = "Symposium on Logic in Computer Science, LICS ; Conference date: 02-08-2022 Through 05-08-2022",

url = "https://dl.acm.org/doi/proceedings/10.1145/3531130",

}

Kristensen, MB, Møgelberg, RE & Vezzosi, A 2022, Greatest HITs: Higher Inductive Types in Coinductive Definitions via Induction under Clocks. in Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science., 42, Association for Computing Machinery, Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, 02/08/2022. https://doi.org/10.1145/3531130.3533359

Greatest HITs: Higher Inductive Types in Coinductive Definitions via Induction under Clocks. / Kristensen, Magnus Baunsgaard; Møgelberg, Rasmus Ejlers; Vezzosi, Andrea.
Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science. Association for Computing Machinery, 2022. 42.

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

TY - GEN

T1 - Greatest HITs: Higher Inductive Types in Coinductive Definitions via Induction under Clocks

AU - Kristensen, Magnus Baunsgaard

AU - Møgelberg, Rasmus Ejlers

AU - Vezzosi, Andrea

N1 - Conference code: 37

PY - 2022

Y1 - 2022

U2 - 10.1145/3531130.3533359

DO - 10.1145/3531130.3533359

M3 - Konferencebidrag i proceedings

SN - 9781450393515

BT - Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science

PB - Association for Computing Machinery

T2 - Symposium on Logic in Computer Science

Y2 - 2 August 2022 through 5 August 2022

ER -

Greatest HITs: Higher Inductive Types in Coinductive Definitions via Induction under Clocks

Symposium

Access to Document

Projects

Type theories for reactive programming

Cite this