| A topos for algebraic quantum theory C Heunen, NP Landsman, B Spitters Communications in mathematical physics 291 (1), 63-110, 2009 | 178 | 2009 |
| Type classes for mathematics in type theory B Spitters, E Van der Weegen Mathematical Structures in Computer Science 21 (4), 795-825, 2011 | 158* | 2011 |
| Homotopy type theory: Univalent foundations of mathematics TUF Program arXiv:1308.0729, 2013 | 125* | 2013 |
| Modalities in homotopy type theory E Rijke, M Shulman, B Spitters Logical Methods in Computer Science, Volume 16, Issue 1 (January 8, 2020), 2017 | 116 | 2017 |
| 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 | 107 | 2017 |
| Internal universes in models of homotopy type theory DR Licata, I Orton, AM Pitts, B Spitters Formal Structures for Computation and Deduction (FSCD 2018), Leibniz …, 2018 | 98 | 2018 |
| Guarded cubical type theory: Path equality for guarded recursion L Birkedal, A Bizjak, R Clouston, HB Grathwohl, B Spitters, A Vezzosi arXiv preprint arXiv:1606.05223, 2016 | 72* | 2016 |
| Modal dependent type theory and dependent right adjoints L Birkedal, R Clouston, B Mannaa, RE Møgelberg, AM Pitts, B Spitters Mathematical Structures in Computer Science 30 (2), 118-138, 2020 | 69* | 2020 |
| Integrals and valuations T Coquand, B Spitters arXiv preprint arXiv:0808.1522, 2008 | 61 | 2008 |
| Type classes for efficient exact real arithmetic in Coq R Krebbers, B Spitters Logical Methods in Computer Science 9, 2013 | 60 | 2013 |
| ConCert: a smart contract certification framework in Coq D Annenkov, JB Nielsen, B Spitters Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020 | 59* | 2020 |
| The Picard algorithm for ordinary differential equations in Coq E Makarov, B Spitters Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes …, 2013 | 56 | 2013 |
| Bohrification of operator algebras and quantum logic C Heunen, NP Landsman, B Spitters Synthese 186 (3), 719-752, 2012 | 48 | 2012 |
| Intuitionistic quantum logic of an n-level system M Caspers, C Heunen, NP Landsman, B Spitters Foundations of Physics 39 (7), 731-759, 2009 | 48 | 2009 |
| Bohrification. C Heunen, NP Landsman, B Spitters Deep Beauty: Mathematical Innovation and Research for Underlying …, 2011 | 47* | 2011 |
| The Gelfand spectrum of a noncommutative C*-algebra: a topos-theoretic approach C Heunen, NP Landsman, B Spitters, S Wolters Journal of the Australian Mathematical Society 90 (1), 39-52, 2011 | 40 | 2011 |
| Constructive Gelfand duality for C*-algebras T Coquand, B Spitters Mathematical Proceedings of the Cambridge Philosophical Society 147 (2), 339-344, 2009 | 39 | 2009 |
| Sets in homotopy type theory E Rijke, B Spitters Mathematical Structures in Computer Science 25 (5), 1172-1202, 2015 | 38 | 2015 |
| Constructive analysis, types and exact real numbers H Geuvers, M Niqui, B Spitters, F Wiedijk Mathematical Structures in Computer Science 17 (1), 3-36, 2007 | 38 | 2007 |
| Ssprove: A foundational framework for modular cryptographic proofs in coq C Abate, PG Haselwarter, E Rivas, A Van Muylder, T Winterhalter, ... 2021 IEEE 34th Computer Security Foundations Symposium (CSF), 1-15, 2021 | 37 | 2021 |
Chris HeunenUniversity of Edinburgh在 ed.ac.uk 的电子邮件经过验证
