Daniel R. Licata

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