| Quipper: a scalable quantum programming language AS Green, PLF Lumsdaine, NJ Ross, P Selinger, B Valiron Proceedings of the 34th ACM SIGPLAN conference on Programming language …, 2013 | 536 | 2013 |
| The simplicial model of univalent foundations (after Voevodsky) C Kapulkin, PLF Lumsdaine Journal of the European Mathematical Society, to appear; preprint arXiv:1211 …, 2012 | 336* | 2012 |
| Weak omega-categories from intensional type theory PLF Lumsdaine | 157 | 2008 |
| Semantics of higher inductive types PLF Lumsdaine, M Shulman Mathematical Proceedings of the Cambridge Philosophical Society 169 (1), 159-208, 2020 | 133* | 2020 |
| Homotopy type theory: Univalent foundations of mathematics TUFP (collaboration) Institute for Advanced Study (Princeton), The Univalent Foundations Program …, 2013 | 126* | 2013 |
| The local universes model: an overlooked coherence construction for dependent type theories PLF Lumsdaine, MA Warren ACM Transactions on Computational Logic (TOCL) 16 (3), 1-31, 2015 | 117 | 2015 |
| The HoTT library: a formalization of homotopy type theory in Coq A Bauer, J Gross, PLF Lumsdaine, M Shulman, M Sozeau, B Spitters Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and …, 2017 | 100 | 2017 |
| An introduction to quantum programming in Quipper AS Green, PLF Lumsdaine, NJ Ross, P Selinger, B Valiron Reversible Computation: 5th International Conference, RC 2013, Victoria, BC …, 2013 | 100 | 2013 |
| Displayed categories B Ahrens, PLF Lumsdaine Logical Methods in Computer Science 15, 2019 | 57 | 2019 |
| Homotopy limits in Coq J Avigad, K Kapulkin, PLF Lumsdaine arXiv preprint arXiv:1304.0680 4, 2013 | 55* | 2013 |
| The homotopy theory of type theories K Kapulkin, PLF Lumsdaine Advances in Mathematics 337, 1-38, 2018 | 48 | 2018 |
| A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory KB Hou, E Finster, DR Licata, PLF Lumsdaine Proceedings of the 31st annual ACM/IEEE symposium on logic in computer …, 2016 | 40 | 2016 |
| The simplicial model of univalent foundations C Kapulkin, PLF Lumsdaine, V Voevodsky arXiv preprint arXiv:1211.2851, 3583-3617, 2014 | 29 | 2014 |
| Categorical structures for type theory in univalent foundations B Ahrens, PLF Lumsdaine, V Voevodsky Logical Methods in Computer Science 14, 2018 | 25 | 2018 |
| Higher inductive types: a tour of the menagerie PLF Lumsdaine | 25 | 2011 |
| Univalence in simplicial sets C Kapulkin, PLF Lumsdaine, V Voevodsky arXiv:1203.2553, 2012 | 23 | 2012 |
| Higher Categories from Type Theories (PhD thesis) PLF Lumsdaine Carnegie Mellon University, 2010 | 20 | 2010 |
| The simplicial model of univalent foundations (after voevodsky)(2012) C Kapulkin, PLF Lumsdaine arXiv preprint arXiv:1211.2851, 2012 | 19 | 2012 |
| A general definition of dependent type theories A Bauer, PG Haselwarter, PLF Lumsdaine arXiv preprint arXiv:2009.05539, 2020 | 15 | 2020 |
| Model structures from higher inductive types PLF Lumsdaine url: http://peterlefanulumsdaine.com/research/Lumsdaine-Model-strux-from …, 2011 | 12 | 2011 |
Chris KapulkinAssociate Professor; University of Western Ontario在 uwo.ca 的电子邮件经过验证
