27 citations · 100 across the 13 of their papers we have counts for
13 papers
Gradual Typing for Effect Handlers
Max S. New, Eric Giovannini, Daniel R. Licata
We present a gradually typed language, GrEff, with effects and handlers that supports migration from unchecked to checked effect typing. This serves as a simple model of the integr…
A Formal Logic for Formal Category Theory (Extended Version)
Max S. New, Daniel R. Licata
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 for…
Synthetic Spectra via a Monadic and Comonadic Modality
Mitchell Riley, Eric Finster, Daniel R. Licata
We extend Homotopy Type Theory with a novel modality that is simultaneously a monad and a comonad. Because this modality induces a non-trivial endomap on every type, it requires a…
Denotational recurrence extraction for amortized analysis
Joseph W. Cutler, Daniel R. Licata, Norman Danner
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 t…
Denotational semantics as a foundation for cost recurrence extraction for functional languages
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 co…
Recurrence Extraction for Functional Programs through Call-by-Push-Value (Extended Version)
G. A. Kavvos, Edward Morehouse, Daniel R. Licata +1
The main way of analyzing the complexity of a program is that of extracting and solving a recurrence that expresses its running time in terms of the size of its input. We develop a…
Gradual Type Theory (Extended Version)
Max S. New, Daniel R. Licata, Amal Ahmed
Gradually typed languages are designed to support both dynamically typed and statically typed programming styles while preserving the benefits of each. While existing gradual type…
Call-by-name Gradual Type Theory
Max S. New, Daniel R. Licata
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 typ…
Internal Universes in Models of Homotopy Type Theory
Daniel R. Licata, Ian Orton, Andrew M. Pitts +1
We begin by recalling the essentially global character of universes in various models of homotopy type theory, which prevents a straightforward axiomatization of their properties u…
A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory
Kuen-Bang Hou, Eric Finster, Dan Licata +1
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…
Denotational cost semantics for functional languages with inductive types
Norman Danner, Daniel R. Licata, Ramyaa Ramyaa
A central method for analyzing the asymptotic complexity of a functional program is to extract and then solve a recurrence that expresses evaluation cost in terms of input size. Th…
Calculating the Fundamental Group of the Circle in Homotopy Type Theory
Daniel R. Licata, Michael Shulman
Recent work on homotopy type theory exploits an exciting new correspondence between Martin-Lof's dependent type theory and the mathematical disciplines of category theory and homot…
A Monadic Formalization of ML5
Daniel R. Licata, Robert Harper
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 S…