| 2023 | FOSSACS | A Formal Logic for Formal Category Theory. | Max S. New, Daniel R. Licata |
| 2020 | LICS | A Constructive Model of Directed Univalence in Bicubical Sets. | Matthew Z. Weaver, Daniel R. Licata |
| 2016 | LFCS | Adjoint Logic with a 2-Category of Modes. | Daniel R. Licata, Michael Shulman |
| 2016 | LICS | A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory. | Kuen-Bang Hou (Favonia), Eric Finster, Daniel R. Licata, Peter LeFanu Lumsdaine |
| 2015 | ICFP | Denotational cost semantics for functional languages with inductive types. | Norman Danner, Daniel R. Licata, Ramyaa |
| 2015 | LICS | A Cubical Approach to Synthetic Homotopy Theory. | Daniel R. Licata, Guillaume Brunerie |
| 2014 | CSL | Eilenberg-MacLane spaces in homotopy type theory. | Daniel R. Licata, Eric Finster |
| 2014 | ICFP | Homotopical patch theory. | Carlo Angiuli, Edward Morehouse, Daniel R. Licata, Robert Harper |
| 2013 | CPP | π n (S n ) in Homotopy Type Theory. | Daniel R. Licata, Guillaume Brunerie |
| 2013 | LICS | Calculating the Fundamental Group of the Circle in Homotopy Type Theory. | Daniel R. Licata, Michael Shulman |
| 2012 | POPL | Canonicity for 2-dimensional type theory. | Daniel R. Licata, Robert Harper |
| 2010 | ICFP | Security-typed programming within dependently typed programming. | Jamie Morgenstern, Daniel R. Licata |
| 2009 | ICFP | A universe of binding and computation. | Daniel R. Licata, Robert Harper |
| 2008 | LICS | Focusing on Binding and Computation. | Daniel R. Licata, Noam Zeilberger, Robert Harper |