Zobrazeno 1 - 10
of 30
pro vyhledávání: '"Daniel R. Licata"'
Autor:
Max S. New, Daniel R. Licata
Publikováno v:
Logical Methods in Computer Science, Vol Volume 16, Issue 1 (2020)
We present gradual type theory, a logic and type theory for call-by-name gradual typing. We define the central constructions of gradual typing (the dynamic type, type casts and type error) in a novel way, by universal properties relative to new judgm
Externí odkaz:
https://doaj.org/article/82b30a81a31746389f603b9c17035e18
Autor:
Daniel R. Licata, Robert Harper
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 34, Iss Proc. LFMTP 2010, Pp 69-83 (2010)
ML5 is a programming language for spatially distributed computing, based on a Curry-Howard correspondence with the modal logic S5. Despite being designed by a correspondence with S5 modal logic, the ML5 programming language differs from the logic in
Externí odkaz:
https://doaj.org/article/88f32bf45e614bcaae5d194ca67f1314
Autor:
Max S. New, Daniel R. Licata
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783031308284
We present a domain-specific type theory for constructions and proofs in category theory. The type theory axiomatizes notions of category, functor, profunctor and a generalized form of natural transformations. The type theory imposes an ordered linea
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::022bc94074fe800c5bbedc4dc4420dda
https://doi.org/10.1007/978-3-031-30829-1_6
https://doi.org/10.1007/978-3-031-30829-1_6
Autor:
Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), Daniel R. Licata
Publikováno v:
Mathematical Structures in Computer Science. 31:424-468
We present a cubical type theory based on the Cartesian cube category (faces, degeneracies, symmetries, diagonals, but no connections or reversal) with univalent universes, each containing Π, Σ, path, identity, natural number, boolean, suspension,
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::5ed2b2c96ba07fa76e844ad793228f2e
https://doi.org/10.1017/s0960129521000347
https://doi.org/10.1017/s0960129521000347
Publikováno v:
Journal of Functional Programming. 31
Gradually typed languages are designed to support both dynamically typed and statically typed programming styles while preserving the benefits of each. Sound gradually typed languages dynamically check types at runtime at the boundary between statica
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::903da5feb2b77aea00ca591754e0103c
https://doi.org/10.1017/s0956796821000125
https://doi.org/10.1017/s0956796821000125
Autor:
Daniel R. Licata, Matthew Z. Weaver
Publikováno v:
LICS
Directed type theory is an analogue of homotopy type theory where types represent categories, generalizing groupoids. A bisimplicial approach to directed type theory, developed by Riehl and Shulman, is based on equipping each type with both a notion
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::aa9ec7ee3cf1bb80507b4f1662c0b531
https://doi.org/10.1145/3373718.3394794
https://doi.org/10.1145/3373718.3394794
Autor:
NORMAN DANNER, DANIEL R. LICATA
A standard informal method for analyzing the asymptotic complexity of a program is to extract a recurrence that describes its cost in terms of the size of its input, and then to compute a closed-form upper bound on that recurrence. We give a formal a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f0ba7cd680b6029c083cd762384603e0
A typical way of analyzing the time complexity of functional programs is to extract a recurrence expressing the running time of the program in terms of the size of its input, and then to solve the recurrence to obtain a big-O bound. For recurrence ex
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6bbe986003bfed48d4498829e49379c3
Autor:
Daniel R. Licata
Publikováno v:
ICFP
Dependent type theories are functional programming languages with types rich enough to do computer-checked mathematics and software verification. Homotopy type theory is a recent area of work that connects dependent type theory to the mathematical di
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d5531fe011852bf4e7f3bf2ee9324011
https://doi.org/10.1145/2951913.2976748
https://doi.org/10.1145/2951913.2976748
Publikováno v:
LICS
This paper continues investigations in "synthetic homotopy theory": the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory We present a mechanized proof of the Blakers-Massey connectivity theorem, a resul
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ed6e851a5b2c045304a28072020b0328
https://doi.org/10.1145/2933575.2934545
https://doi.org/10.1145/2933575.2934545