The Feature Signatures of Evolving Programs. - Daniel R. Licata; Christopher D. Harris; Shriram Krishnamurthi (ASE, 2003)

Verifying Interactive Web Programs. - Daniel R. Licata; Shriram Krishnamurthi (ASE, 2004)

Mechanizing metatheory in a logical framework. - Robert Harper 001; Daniel R. Licata (J. Funct. Program., 2007)

Focusing on Binding and Computation. - Daniel R. Licata; Noam Zeilberger; Robert Harper 001 (LICS, 2008)

A universe of binding and computation. - Daniel R. Licata; Robert Harper 001 (ICFP, 2009)

Positively dependent types. - Daniel R. Licata; Robert Harper 001 (PLPV, 2009)

A Pronominal Approach to Binding and Computation. - Robert Harper 001; Daniel R. Licata; Noam Zeilberger (TLCA, 2009)

Security-typed programming within dependently typed programming. - Jamie Morgenstern; Daniel R. Licata (ICFP, 2010)

A Monadic Formalization of ML5 - Daniel R. Licata; Robert Harper 001 (LFMTP, 2010)

2-Dimensional Directed Type Theory. - Daniel R. Licata; Robert Harper 001 (MFPS, 2011)

Canonicity for 2-dimensional type theory. - Daniel R. Licata; Robert Harper 001 (POPL, 2012)

π n (S n ) in Homotopy Type Theory. - Daniel R. Licata; Guillaume Brunerie (CPP, 2013)

Calculating the Fundamental Group of the Circle in Homotopy Type Theory. - Daniel R. Licata; Michael Shulman (LICS, 2013)

Eilenberg-MacLane spaces in homotopy type theory. - Daniel R. Licata; Eric Finster (CSL-LICS, 2014)

Denotational cost semantics for functional languages with inductive types. - Norman Danner; Daniel R. Licata; Ramyaa (ICFP, 2015)

A Cubical Approach to Synthetic Homotopy Theory. - Daniel R. Licata; Guillaume Brunerie (LICS, 2015)

A functional programmer's guide to homotopy type theory. - Dan Licata (ICFP, 2016)

Adjoint Logic with a 2-Category of Modes. - Daniel R. Licata; Michael Shulman (LFCS, 2016)

A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory. - Kuen-Bang Hou (Favonia); Eric Finster; Daniel R. Licata; Peter LeFanu Lumsdaine (LICS, 2016)

Homotopical patch theory. - Carlo Angiuli; Edward Morehouse; Daniel R. Licata; Robert Harper 001 (J. Funct. Program., 2016)

A Fibrational Framework for Substructural and Modal Logics. - Daniel R. Licata; Michael Shulman; Mitchell Riley (FSCD, 2017)

Internal Universes in Models of Homotopy Type Theory. - Daniel R. Licata; Ian Orton; Andrew M. Pitts; Bas Spitters (FSCD, 2018)

Gradual Type Theory (Extended Version). - Max S. New; Daniel R. Licata; Amal Ahmed 001 (CoRR, 2018)

Recurrence Extraction for Functional Programs through Call-by-Push-Value (Extended Version). - G. A. Kavvos; Edward Morehouse; Daniel R. Licata; Norman Danner (CoRR, 2019)

Gradual type theory. - Max S. New; Daniel R. Licata; Amal Ahmed 001 (Proc. ACM Program. Lang., 2019)

A Constructive Model of Directed Univalence in Bicubical Sets. - Matthew Z. Weaver; Daniel R. Licata (LICS, 2020)

Call-by-name Gradual Type Theory. - Max S. New; Daniel R. Licata (Log. Methods Comput. Sci., 2020)

Denotational recurrence extraction for amortized analysis. - Joseph W. Cutler; Daniel R. Licata; Norman Danner (Proc. ACM Program. Lang., 2020)

Recurrence extraction for functional programs through call-by-push-value. - G. A. Kavvos; Edward Morehouse; Daniel R. Licata; Norman Danner (Proc. ACM Program. Lang., 2020)

Syntax and models of Cartesian cubical type theory. - Carlo Angiuli; Guillaume Brunerie; Thierry Coquand; Robert Harper 001; Kuen-Bang Hou (Favonia); Daniel R. Licata (Math. Struct. Comput. Sci., 2021)

Special issue on homotopy type theory 2019. - Dan Licata; Peter LeFanu Lumsdaine (Math. Struct. Comput. Sci., 2021)

Denotational semantics as a foundation for cost recurrence extraction for functional languages. - Norman Danner; Daniel R. Licata (J. Funct. Program., 2022)

A Formal Logic for Formal Category Theory. - Max S. New; Daniel R. Licata (FoSSaCS, 2023)

Special issue on homotopy type theory 2019 vol. 2. - Dan Licata; Peter LeFanu Lumsdaine (Math. Struct. Comput. Sci., 2023)

Gradual Typing for Effect Handlers. - Max S. New; Eric Giovannini; Daniel R. Licata (Proc. ACM Program. Lang., 2023)

Complexity of Cubical Cofibration Logics I: coNP-Complete Examples. - Robert Rose; Daniel R. Licata (TYPES, 2024)