Zobrazeno 1 - 6
of 6
pro vyhledávání: '"Evan Cavallo"'
Autor:
Evan Cavallo, Robert Harper
Publikováno v:
Logical Methods in Computer Science, Vol Volume 17, Issue 4 (2021)
We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, which we call relat
Externí odkaz:
https://doaj.org/article/81bd290feab7404392fb742bb9d43091
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 274, Iss Proc. LFMTP 2018, Pp 1-10 (2018)
RedPRL is an experimental proof assistant based on Cartesian cubical computational type theory, a new type theory for higher-dimensional constructions inspired by homotopy type theory. In the style of Nuprl, RedPRL users employ tactics to establish b
Externí odkaz:
https://doaj.org/article/86dcd954605c4cb2ac77f3daa3801932
Publikováno v:
Gratzer, D, Cavallo, E, Kavvos, G A, Guatto, A & Birkedal, L 2022, ' Modalities and Parametric Adjoints ', ACM Transactions on Computational Logic, vol. 23, no. 3, 18, pp. 1-29 . https://doi.org/10.1145/3514241
Gratzer, D, Cavallo, E, Kavvos, G A, Guatto, A & Birkedal, L 2022, ' Modalities and Parametric Adjoints ', ACM Transactions on Computational Logic, vol. 23, no. 3, 18 . https://doi.org/10.1145/3514241
Gratzer, D, Cavallo, E, Kavvos, G A, Guatto, A & Birkedal, L 2022, ' Modalities and Parametric Adjoints ', ACM Transactions on Computational Logic, vol. 23, no. 3, 18 . https://doi.org/10.1145/3514241
Birkedal et al. recently introduced dependent right adjoints as an important class of (non-fibered) modalities in type theory. We observe that several aspects of their calculus are left underdeveloped and that it cannot serve as an internal language.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5b12671944a27f4c722076962104067f
https://hdl.handle.net/1983/ea431b5e-5842-4714-ae0c-801d55ad2aa9
https://hdl.handle.net/1983/ea431b5e-5842-4714-ae0c-801d55ad2aa9
Publikováno v:
Proceedings of the ACM on Programming Languages. 5:1-30
In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our programming lang
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::91aa38b238a81e8316a339671ed1fa30
https://doi.org/10.1145/3434293
https://doi.org/10.1145/3434293
Autor:
Evan Cavallo, Robert Harper
Publikováno v:
Proceedings of the ACM on Programming Languages. 3:1-27
Homotopy type theory proposes higher inductive types (HITs) as a means of defining and reasoning about inductively-generated objects with higher-dimensional structure. As with the univalence axiom, however, homotopy type theory does not specify the c
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::69ed7798eca32dcc3ba55cf1efab7da8
https://doi.org/10.1145/3290314
https://doi.org/10.1145/3290314
Publikováno v:
LFMTP@FSCD
Electronic Proceedings in Theoretical Computer Science, Vol 274, Iss Proc. LFMTP 2018, Pp 1-10 (2018)
Electronic Proceedings in Theoretical Computer Science, Vol 274, Iss Proc. LFMTP 2018, Pp 1-10 (2018)
RedPRL is an experimental proof assistant based on Cartesian cubical computational type theory, a new type theory for higher-dimensional constructions inspired by homotopy type theory. In the style of Nuprl, RedPRL users employ tactics to establish b
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::433f85b65a7fe7172432ef8069e29560