Daniel R. Licata

According to our database, Daniel R. Licata authored at least 35 papers between 2003 and 2023.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2023

Gradual Typing for Effect Handlers.

Max S. New, Eric Giovannini, Daniel R. Licata

Proc. ACM Program. Lang., October, 2023

Special issue on homotopy type theory 2019 vol. 2.

Dan Licata, Peter LeFanu Lumsdaine

Math. Struct. Comput. Sci., 2023

A Formal Logic for Formal Category Theory.

Max S. New, Daniel R. Licata

Proceedings of the Foundations of Software Science and Computation Structures, 2023

2022

Denotational semantics as a foundation for cost recurrence extraction for functional languages.

Norman Danner, Daniel R. Licata

J. Funct. Program., 2022

2021

Special issue on homotopy type theory 2019.

Dan Licata, Peter LeFanu Lumsdaine

Math. Struct. Comput. Sci., 2021

Syntax and models of Cartesian cubical type theory.

Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), Daniel R. Licata

Math. Struct. Comput. Sci., 2021

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

Denotational recurrence extraction for amortized analysis.

Joseph W. Cutler, Daniel R. Licata, Norman Danner

Proc. ACM Program. Lang., 2020

Call-by-name Gradual Type Theory.

Max S. New, Daniel R. Licata

Log. Methods Comput. Sci., 2020

A Constructive Model of Directed Univalence in Bicubical Sets.

Matthew Z. Weaver, Daniel R. Licata

Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

2019

Gradual type theory.

Max S. New, Daniel R. Licata, Amal Ahmed

Proc. ACM Program. Lang., 2019

Recurrence Extraction for Functional Programs through Call-by-Push-Value (Extended Version).

G. A. Kavvos, Edward Morehouse, Daniel R. Licata, Norman Danner

CoRR, 2019

2018

Gradual Type Theory (Extended Version).

Max S. New, Daniel R. Licata, Amal Ahmed

CoRR, 2018

Internal Universes in Models of Homotopy Type Theory.

Daniel R. Licata, Ian Orton, Andrew M. Pitts, Bas Spitters

Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, 2018

2017

A Fibrational Framework for Substructural and Modal Logics.

Daniel R. Licata, Michael Shulman, Mitchell Riley

Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction, 2017

2016

Homotopical patch theory.

Carlo Angiuli, Edward Morehouse, Daniel R. Licata, Robert Harper

J. Funct. Program., 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

Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

Adjoint Logic with a 2-Category of Modes.

Daniel R. Licata, Michael Shulman

Proceedings of the Logical Foundations of Computer Science - International Symposium, 2016

A functional programmer's guide to homotopy type theory.

Dan Licata

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

2015

A Cubical Approach to Synthetic Homotopy Theory.

Daniel R. Licata, Guillaume Brunerie

Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 2015

Denotational cost semantics for functional languages with inductive types.

Norman Danner, Daniel R. Licata, Ramyaa

Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 2015

2014

Eilenberg-MacLane spaces in homotopy type theory.

Daniel R. Licata, Eric Finster

Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014

2013

Calculating the Fundamental Group of the Circle in Homotopy Type Theory.

Daniel R. Licata, Michael Shulman

Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013

π n (S n ) in Homotopy Type Theory.

Daniel R. Licata, Guillaume Brunerie

Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

2012

Canonicity for 2-dimensional type theory.

Daniel R. Licata, Robert Harper

Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

2011

2-Dimensional Directed Type Theory.

Daniel R. Licata, Robert Harper

Proceedings of the Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, 2011

2010

A Monadic Formalization of ML5

Daniel R. Licata, Robert Harper

Proceedings of the Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, 2010

Security-typed programming within dependently typed programming.

Jamie Morgenstern, Daniel R. Licata

Proceedings of the Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, 2010

2009

A Pronominal Approach to Binding and Computation.

Robert Harper, Daniel R. Licata, Noam Zeilberger

Proceedings of the Typed Lambda Calculi and Applications, 9th International Conference, 2009

Positively dependent types.

Daniel R. Licata, Robert Harper

Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, 2009

A universe of binding and computation.

Daniel R. Licata, Robert Harper

Proceedings of the Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, 2009

2008

Focusing on Binding and Computation.

Daniel R. Licata, Noam Zeilberger, Robert Harper

Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, 2008

2007

Mechanizing metatheory in a logical framework.

Robert Harper, Daniel R. Licata

J. Funct. Program., 2007

2004

Verifying Interactive Web Programs.

Daniel R. Licata, Shriram Krishnamurthi

Proceedings of the 19th IEEE International Conference on Automated Software Engineering (ASE 2004), 2004

2003

The Feature Signatures of Evolving Programs.

Daniel R. Licata, Christopher D. Harris, Shriram Krishnamurthi

Proceedings of the 18th IEEE International Conference on Automated Software Engineering (ASE 2003), 2003