Mechanizing metatheory in a logical framework R Harper, DR Licata Journal of functional programming 17 (4-5), 613-673, 2007 | 156 | 2007 |
Calculating the fundamental group of the circle in homotopy type theory DR Licata, M Shulman 2013 28th annual acm/ieee symposium on logic in computer science, 223-232, 2013 | 114 | 2013 |
Internal universes in models of homotopy type theory DR Licata, I Orton, AM Pitts, B Spitters arXiv preprint arXiv:1801.07664, 2018 | 99 | 2018 |
Gradual type theory MS New, DR Licata, A Ahmed Proceedings of the ACM on Programming Languages 3 (POPL), 1-31, 2019 | 94 | 2019 |
Eilenberg-MacLane spaces in homotopy type theory DR Licata, E Finster Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference …, 2014 | 85 | 2014 |
Denotational cost semantics for functional languages with inductive types N Danner, DR Licata, R Ramyaa Proceedings of the 20th ACM SIGPLAN International Conference on Functional …, 2015 | 80 | 2015 |
A fibrational framework for substructural and modal logics DR Licata, M Shulman, M Riley 2nd International Conference on Formal Structures for Computation and …, 2017 | 75 | 2017 |
Canonicity for 2-dimensional type theory DR Licata, R Harper ACM SIGPLAN Notices 47 (1), 337-348, 2012 | 65 | 2012 |
2-dimensional directed type theory DR Licata, R Harper Electronic Notes in Theoretical Computer Science 276, 263-289, 2011 | 64 | 2011 |
A cubical approach to synthetic homotopy theory DR Licata, G Brunerie 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 92-103, 2015 | 57 | 2015 |
Verifying interactive web programs DR Licata, S Krishnamurthi Proceedings. 19th International Conference on Automated Software Engineering …, 2004 | 57 | 2004 |
A universe of binding and computation DR Licata, R Harper Proceedings of the 14th ACM SIGPLAN international conference on Functional …, 2009 | 53 | 2009 |
Focusing on binding and computation DR Licata, N Zeilberger, R Harper 2008 23rd Annual IEEE Symposium on Logic in Computer Science, 241-252, 2008 | 51 | 2008 |
Adjoint logic with a 2-category of modes DR Licata, M Shulman Logical Foundations of Computer Science: International Symposium, LFCS 2016 …, 2016 | 46 | 2016 |
Security-typed programming within dependently typed programming J Morgenstern, DR Licata Proceedings of the 15th ACM SIGPLAN international conference on Functional …, 2010 | 46 | 2010 |
Syntax and models of Cartesian cubical type theory C Angiuli, G Brunerie, T Coquand, R Harper, KB Hou, DR Licata Mathematical Structures in Computer Science 31 (4), 424-468, 2021 | 45 | 2021 |
A constructive model of directed univalence in bicubical sets MZ Weaver, DR Licata Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer …, 2020 | 44 | 2020 |
Homotopical patch theory C Angiuli, E Morehouse, DR Licata, R Harper ACM SIGPLAN Notices 49 (9), 243-256, 2014 | 42 | 2014 |
π n (S n ) in Homotopy Type Theory DR Licata, G Brunerie Certified Programs and Proofs: Third International Conference, CPP 2013 …, 2013 | 36 | 2013 |
Recurrence extraction for functional programs through call-by-push-value GA Kavvos, E Morehouse, DR Licata, N Danner Proceedings of the ACM on Programming Languages 4 (POPL), 1-31, 2019 | 32 | 2019 |