Bas Spitters

Cited by

	All	Since 2020
Citations	2216	1057
h-index	26	19
i10-index	45	26

240

120

180

200320042005200620072008200920102011201220132014201520162017201820192020202120222023202420256 9 16 14 10 26 55 70 51 102 108 78 82 89 127 142 151 157 200 191 207 236 65

Public access

View all

15 articles

0 articles

available

not available

Based on funding mandates

Co-authors

Chris HeunenUniversity of EdinburghVerified email at ed.ac.uk
Danil AnnenkovAarhus UniversityVerified email at di.ku.dk
Andrew M PittsEmeritus Professor of Theoretical Computer Science, University of CambridgeVerified email at cl.cam.ac.uk
Jakob Botsch NielsenVerified email at cs.au.dk
Ranald CloustonLecturer, Australian National UniversityVerified email at anu.edu.au
Egbert RijkePostdoc in Mathematics, University of LjubljanaVerified email at fmf.uni-lj.si
Michael ShulmanAssociate Professor of Mathematics, University of San DiegoVerified email at sandiego.edu
Lars BirkedalDept. of Computer Science, Aarhus UniversityVerified email at cs.au.dk
Andrej BauerUniversity of LjubljanaVerified email at andrej.com
Ian OrtonUniversity of CambridgeVerified email at cam.ac.uk
Dan LicataWesleyan UniversityVerified email at wesleyan.edu
Bassel MannaaPostdoc, IT University of CopenhagenVerified email at itu.dk
Rasmus MøgelbergIT University of CopenhagenVerified email at itu.dk
Peter LeFanu LumsdaineAssistant professor, Dept. of Mathematics, Stockholm UniversityVerified email at math.su.se
Jason GrossGraduate, Massachusetts Institute of TechnologyVerified email at mit.edu
Cătălin HrițcuTenured Faculty at MPI-SPVerified email at mpi-sp.org
Théo WinterhalterInria SaclayVerified email at inria.fr
Philipp G. HaselwarterAssistant Professor, Aarhus UniversityVerified email at cs.au.dk
Sabine OechsnerAssistant Professor at Vrije Universiteit AmsterdamVerified email at vu.nl
Robbert KrebbersAssociate Professor, Radboud University NijmegenVerified email at cs.ru.nl

Bas Spitters

Associate Professor, Aarhus University

Verified email at cs.au.dk - Homepage

Categorical type theory semantics program verification blockchain


Title Sort by citations Sort by year Sort by title	Cited by Cited by	Year
A topos for algebraic quantum theory C Heunen, NP Landsman, B Spitters Communications in mathematical physics 291 (1), 63-110, 2009	184	2009
Type classes for mathematics in type theory B Spitters, E Van der Weegen Mathematical Structures in Computer Science 21 (4), 795-825, 2011	165*	2011
Homotopy type theory: Univalent foundations of mathematics TUF Program arXiv:1308.0729, 2013	144*	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	126	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	115	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	100	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	76*	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	75	2020
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	67*	2020
Type classes for efficient exact real arithmetic in Coq R Krebbers, B Spitters Logical Methods in Computer Science 9, 2013	65	2013
The Picard algorithm for ordinary differential equations in Coq E Makarov, B Spitters Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes …, 2013	63	2013
Integrals and valuations T Coquand, B Spitters arXiv preprint arXiv:0808.1522, 2008	62	2008
Bohrification of operator algebras and quantum logic C Heunen, NP Landsman, B Spitters Synthese 186 (3), 719-752, 2012	52	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	50	2009
Bohrification. C Heunen, NP Landsman, B Spitters Deep Beauty: Mathematical Innovation and Research for Underlying …, 2011	49*	2011
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	44	2021
Sets in homotopy type theory E Rijke, B Spitters Mathematical Structures in Computer Science 25 (5), 1172-1202, 2015	43	2015
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	42	2011
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	41	2007
Computer-aided proofs for multiparty computation with active security H Haagh, A Karbyshev, S Oechsner, B Spitters, PY Strub 2018 IEEE 31st Computer Security Foundations Symposium (CSF), 119-131, 2018	39	2018

The system can't perform the operation now. Try again later.

Articles 1–20

Citations per year

Duplicate citations

Merged citations

Add co-authorsCo-authors

Follow

Cited by

Co-authors