Daniel R. Licata

Publication Activity (10 Years)

Years Active: 2003-2023
Publications (10 Years): 28

Top Topics

Functional Language

Denotational Semantics

Top Venues

Proc. ACM Program. Lang.

J. Funct. Program.

Publications

Max S. New, Daniel R. Licata
A Formal Logic for Formal Category Theory. FoSSaCS (2023)
Max S. New, Eric Giovannini, Daniel R. Licata
Gradual Typing for Effect Handlers. CoRR (2023)
Max S. New, Eric Giovannini, Daniel R. Licata
Gradual Typing for Effect Handlers. Proc. ACM Program. Lang. 7 (OOPSLA2) (2023)
Norman Danner, Daniel R. Licata
Denotational semantics as a foundation for cost recurrence extraction for functional languages. J. Funct. Program. 32 (2022)
Max S. New, Daniel R. Licata
A Formal Logic for Formal Category Theory. CoRR (2022)
Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), Daniel R. Licata
Syntax and models of Cartesian cubical type theory. Math. Struct. Comput. Sci. 31 (4) (2021)
Max S. New, Daniel R. Licata, Amal Ahmed
Gradual type theory. J. Funct. Program. 31 (2021)
Joseph W. Cutler, Daniel R. Licata, Norman Danner
Denotational recurrence extraction for amortized analysis. Proc. ACM Program. Lang. 4 (ICFP) (2020)
Max S. New, Daniel R. Licata
Call-by-name Gradual Type Theory. Log. Methods Comput. Sci. 16 (1) (2020)
Norman Danner, Daniel R. Licata
Denotational semantics as a foundation for cost recurrence extraction for functional languages. CoRR (2020)
G. A. Kavvos, Edward Morehouse, Daniel R. Licata, Norman Danner
Recurrence extraction for functional programs through call-by-push-value. Proc. ACM Program. Lang. 4 (POPL) (2020)
Matthew Z. Weaver, Daniel R. Licata
A Constructive Model of Directed Univalence in Bicubical Sets. LICS (2020)
Joseph W. Cutler, Daniel R. Licata, Norman Danner
Denotational recurrence extraction for amortized analysis. CoRR (2020)
Max S. New, Daniel R. Licata, Amal Ahmed
Gradual type theory. Proc. ACM Program. Lang. 3 (POPL) (2019)
G. A. Kavvos, Edward Morehouse, Daniel R. Licata, Norman Danner
Recurrence Extraction for Functional Programs through Call-by-Push-Value (Extended Version). CoRR (2019)
Daniel R. Licata, Ian Orton, Andrew M. Pitts, Bas Spitters
Internal Universes in Models of Homotopy Type Theory. CoRR (2018)
Max S. New, Daniel R. Licata
Call-by-Name Gradual Type Theory. FSCD (2018)
Max S. New, Daniel R. Licata, Amal Ahmed
Gradual Type Theory (Extended Version). CoRR (2018)
Max S. New, Daniel R. Licata
Call-by-name Gradual Type Theory. CoRR (2018)
Daniel R. Licata, Ian Orton, Andrew M. Pitts, Bas Spitters
Internal Universes in Models of Homotopy Type Theory. FSCD (2018)
Daniel R. Licata, Michael Shulman, Mitchell Riley
A Fibrational Framework for Substructural and Modal Logics. FSCD (2017)
Kuen-Bang Hou, Eric Finster, Daniel R. Licata, Peter LeFanu Lumsdaine
A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory. CoRR (2016)
Daniel R. Licata, Michael Shulman
Adjoint Logic with a 2-Category of Modes. LFCS (2016)
Carlo Angiuli, Edward Morehouse, Daniel R. Licata, Robert Harper
Homotopical patch theory. J. Funct. Program. 26 (2016)
Kuen-Bang Hou (Favonia), Eric Finster, Daniel R. Licata, Peter LeFanu Lumsdaine
A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory. LICS (2016)
Daniel R. Licata, Guillaume Brunerie
A Cubical Approach to Synthetic Homotopy Theory. LICS (2015)
Norman Danner, Daniel R. Licata, Ramyaa
Denotational cost semantics for functional languages with inductive types. ICFP (2015)
Norman Danner, Daniel R. Licata, Ramyaa Ramyaa
Denotational cost semantics for functional languages with inductive types. CoRR (2015)
Carlo Angiuli, Edward Morehouse, Daniel R. Licata, Robert Harper
Homotopical patch theory. ICFP (2014)
Daniel R. Licata, Eric Finster
Eilenberg-MacLane spaces in homotopy type theory. CSL-LICS (2014)
Daniel R. Licata, Guillaume Brunerie
π n (S n ) in Homotopy Type Theory. CPP (2013)
Daniel R. Licata, Michael Shulman
Calculating the Fundamental Group of the Circle in Homotopy Type Theory CoRR (2013)
Daniel R. Licata, Michael Shulman
Calculating the Fundamental Group of the Circle in Homotopy Type Theory. LICS (2013)
Daniel R. Licata, Robert Harper
Canonicity for 2-dimensional type theory. POPL (2012)
Daniel R. Licata, Robert Harper
2-Dimensional Directed Type Theory. MFPS (2011)
Daniel R. Licata, Robert Harper
A Monadic Formalization of ML5 LFMTP (2010)
Jamie Morgenstern, Daniel R. Licata
Security-typed programming within dependently typed programming. ICFP (2010)
Daniel R. Licata, Robert Harper
A universe of binding and computation. ICFP (2009)
Robert Harper, Daniel R. Licata, Noam Zeilberger
A Pronominal Approach to Binding and Computation. TLCA (2009)
Daniel R. Licata, Robert Harper
Positively dependent types. PLPV (2009)
Daniel R. Licata, Noam Zeilberger, Robert Harper
Focusing on Binding and Computation. LICS (2008)
Robert Harper, Daniel R. Licata
Mechanizing metatheory in a logical framework. J. Funct. Program. 17 (4-5) (2007)
Daniel R. Licata, Shriram Krishnamurthi
Verifying Interactive Web Programs. ASE (2004)
Daniel R. Licata, Christopher D. Harris, Shriram Krishnamurthi
The Feature Signatures of Evolving Programs. ASE (2003)