Edit Profile (opens in new tab) Spitters, Bas Co-Author Distance Author ID: spitters.bas Published as: Spitters, Bas; Spitters, B. Homepage: http://users-cs.au.dk/spitters/ External Links: MGP · ORCID · Google Scholar · ResearchGate · dblp Documents Indexed: 45 Publications since 2000 1 Contribution as Editor · 1 Further Contribution Reviewing Activity: 6 Reviews Co-Authors: 38 Co-Authors with 36 Joint Publications 622 Co-Co-Authors all top 5 Co-Authors 11 single-authored 8 Coquand, Thierry 6 Heunen, Chris 6 Landsman, Nicolaas P. 4 Rijke, Egbert 3 Birkedal, Lars 3 Clouston, Ranald A. 2 Bizjak, Aleš 2 Grathwohl, Hans Bugge 2 Krebbers, Robbert 2 Palmgren, Erik 2 Pitts, Andrew M. 2 Shulman, Michael A. 2 van der Weegen, Eelis 2 Vezzosi, Andrea 2 Wolters, Sander A. M. 1 Aczel, Peter 1 Ahrens, Benedikt 1 Altenkirch, Thorsten 1 Angiuli, Carlo 1 Annenkov, Danil 1 Avigad, Jeremy 1 Awodey, Steve 1 Barras, Bruno 1 Bauer, Andrej 1 Bertot, Yves 1 Bezem, Marc 1 Bidlingmaier, Martin E. 1 Bordg, Anthony 1 Bridges, Douglas Suth 1 Brunerie, Guillaume 1 Caspers, Martijn 1 Cohen, Cyril 1 Constable, Robert Lee 1 Cruz-Filipe, Luís 1 Curien, Pierre-Louis 1 Dybjer, Peter 1 Faissole, Florian 1 Finster, Eric 1 Gambino, Nicola 1 Garner, Richard 1 Geuvers, Jan Herman 1 Gonthier, Georges 1 Grayson, Daniel Richard 1 Hales, Thomas Callister 1 Harper, Robert 1 Herbelin, Hugo 1 Hofmann, Martin 1 Hofstra, Pieter J. W. 1 Hötzel Escardó, Martín 1 Hou (Favonia), Kuen-Bang 1 Ishihara, Hajime 1 Jacobs, Bart 1 Joyal, André 1 Kapulkin, Krzysztof 1 Kock, Joachim 1 Kraus, Nicolai 1 Li, Nuo 1 Licata, Dan 1 Licata, Daniel R. 1 Lumsdaine, Peter LeFanu 1 Luo, Zhaohui 1 Mahboubi, Assia 1 Makarov, Evgeniĭ Olegovich 1 Mannaa, Bassel 1 Martin-Löf, Per 1 Melikhov, Sergey Aleksandrovich 1 Milo, Mikkel 1 Møgelberg, Rasmus Ejlers 1 Morrisett, Greg 1 Nahas, Michael 1 Nielsen, Jakob Botsch 1 Niqui, Milad 1 O’Connor, Russell 1 Orton, Ian 1 Pelayo, Alvaro 1 Polonsky, Andrew 1 Riehl, Emily 1 Scott, Dana Stewart 1 Scott, Philip J. 1 Selinger, Peter 1 Sojakova, Kristina 1 Solov’ëv, Sergeĭ Vladimirovich 1 Sozeau, Matthieu 1 1 Van den Berg, Benno 1 Veldman, Wim 1 Vickers, Steven 1 Voevodskiĭ, Vladimir Aleksandrovich 1 Warren, Michael Alton 1 Wiedijk, Freek 1 Zeilberger, Noam all top 5 Serials 5 MSCS. Mathematical Structures in Computer Science 3 Mathematical Logic Quarterly (MLQ) 3 Logical Methods in Computer Science 3 Journal of Logic and Analysis 2 The Journal of Symbolic Logic 2 Annals of Pure and Applied Logic 2 Indagationes Mathematicae. New Series 2 Journal of Universal Computer Science 2 Foundations of Physics 1 Communications in Mathematical Physics 1 Mathematical Proceedings of the Cambridge Philosophical Society 1 Synthese 1 Theoretical Computer Science 1 Order 1 Journal of Automated Reasoning 1 Journal of Functional Programming 1 Nieuw Archief voor Wiskunde. Vijfde Serie 1 Journal of the Australian Mathematical Society 1 Electronic Proceedings in Theoretical Computer Science (EPTCS) all top 5 Fields 31 Mathematical logic and foundations (03-XX) 15 Functional analysis (46-XX) 11 Computer science (68-XX) 10 Category theory; homological algebra (18-XX) 8 Algebraic topology (55-XX) 8 Quantum theory (81-XX) 7 Order, lattices, ordered algebraic structures (06-XX) 7 Measure and integration (28-XX) 3 Operator theory (47-XX) 3 Numerical analysis (65-XX) 2 Real functions (26-XX) 2 Dynamical systems and ergodic theory (37-XX) 1 General and overarching topics; collections (00-XX) 1 Associative rings and algebras (16-XX) 1 Topological groups, Lie groups (22-XX) 1 Ordinary differential equations (34-XX) 1 Abstract harmonic analysis (43-XX) 1 Relativity and gravitational theory (83-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 37 Publications have been cited 248 times in 169 Documents Cited by ▼ Year ▼ Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002The Univalent Foundations Program 128 2013 A topos for algebraic quantum theory. Zbl 1209.81147Heunen, Chris; Landsman, Nicolaas P.; Spitters, Bas 40 2009 Bohrification of operator algebras and quantum logic. Zbl 1275.03166Heunen, Chris; Landsman, Nicolaas P.; Spitters, Bas 16 2012 Modalities in homotopy type theory. Zbl 1489.03005Rijke, Egbert; Shulman, Michael; Spitters, Bas 16 2020 The Picard algorithm for ordinary differential equations in Coq. Zbl 1317.68222Makarov, Evgeny; Spitters, Bas 14 2013 Type classes for mathematics in type theory. Zbl 1223.68105Spitters, Bas; van der Weegen, Eelis 13 2011 Internal universes in models of homotopy type theory. Zbl 1462.03010Licata, Daniel R.; Orton, Ian; Pitts, Andrew M.; Spitters, Bas 13 2018 Integrals and valuations. Zbl 1245.03098Coquand, Thierry; Spitters, Bas 12 2009 The Gelfand spectrum of a noncommutative \(C^*\)-algebra: a topos-theoretic approach. Zbl 1223.46062Heunen, Chris; Landsman, Nicolaas P.; Spitters, Bas; Wolters, Sander 11 2011 Intuitionistic quantum logic of an \(n\)-level system. Zbl 1206.81012Caspers, Martijn; Heunen, Chris; Landsman, Nicolaas P.; Spitters, Bas 11 2009 A computer-verified monadic functional implementation of the integral. Zbl 1209.68108O’Connor, Russell; Spitters, Bas 9 2010 Type classes for efficient exact real arithmetic in Coq. Zbl 1260.68378Krebbers, Robbert; Spitters, Bas 8 2013 Formal topology and constructive mathematics: the Gelfand and Stone-Yosida representation theorems. Zbl 1120.03049Coquand, T.; Spitters, B. 8 2005 Constructive Gelfand duality for C\(^*\)-algebras. Zbl 1183.46052Coquand, Thierry; Spitters, Bas 7 2009 Constructive analysis, types and exact real numbers. Zbl 1157.03036Geuvers, Herman; Niqui, Milad; Spitters, Bas; Wiedijk, Freek 7 2007 Modal dependent type theory and dependent right adjoints. Zbl 1479.03011Birkedal, Lars; Clouston, Ranald; Mannaa, Bassel; Ejlers Møgelberg, Rasmus; Pitts, Andrew M.; Spitters, Bas 7 2020 Sets in homotopy type theory. Zbl 1362.03007Rijke, Egbert; Spitters, Bas 6 2015 Guarded cubical type theory: path equality for guarded recursion. Zbl 1370.68052Birkedal, Lars; Bizjak, Aleš; Clouston, Ranald; Grathwohl, Hans Bugge; Spitters, Bas; Vezzosi, Andrea 5 2016 Program extraction from large proof developments. Zbl 1279.68287Cruz-Filipe, Luís; Spitters, Bas 5 2003 The space of measurement outcomes as a spectral invariant for non-commutative algebras. Zbl 1259.81013Spitters, Bas 4 2012 Bohrification. Zbl 1234.81025Heunen, Chris; Landsman, Nicolaas P.; Spitters, Bas 4 2011 Guarded cubical type theory. Zbl 1477.03034Birkedal, Lars; Bizjak, Aleš; Clouston, Ranald; Grathwohl, Hans Bugge; Spitters, Bas; Vezzosi, Andrea 4 2019 Computer certified efficient exact reals in Coq. Zbl 1260.68377Krebbers, Robbert; Spitters, Bas 4 2011 Developing the algebraic hierarchy with type classes in Coq. Zbl 1291.68370Spitters, Bas; van der Weegen, Eelis 3 2010 A constructive view on ergodic theorems. Zbl 1106.03052Spitters, Bas 3 2006 Constructive algebraic integration theory. Zbl 1099.28009Spitters, Bas 2 2006 Locating the range of an operator with an adjoint. Zbl 1092.47063Bridges, Douglas; Ishihara, Hajime; Spitters, Bas 2 2002 8th international workshop on quantum physics and logic, Nijmegen, Netherlands, October 27–29, 2011. Proceedings. Zbl 1391.81010 2 2012 Located operators. Zbl 1041.03050Spitters, Bas 2 2002 Constructive results on operator algebras. Zbl 1125.46059Spitters, B. 2 2005 Metric complements of overt closed sets. Zbl 1251.03084Coquand, Thierry; Palmgren, Erik; Spitters, Bas 2 2011 The principle of general tovariance. Zbl 1153.83335Heunen, C.; Landsman, N. P.; Spitters, B. 1 2008 Constructive theory of Banach algebras. Zbl 1285.03073Coquand, Thierry; Spitters, Bas 1 2010 Locatedness and overt sublocales. Zbl 1223.03053Spitters, Bas 1 2010 An application of computable distributions to the semantics of probabilistic programs. Zbl 07311043Huang, Daniel; Morrisett, Greg; Spitters, Bas 1 2021 Synthetic topology in homotopy type theory for probabilistic programming. Zbl 1517.68072Bidlingmaier, Martin E.; Faissole, Florian; Spitters, Bas 1 2021 Gelfand spectra in Grothendieck toposes using geometric mathematics. Zbl 1471.81044Spitters, Bas; Vickers, Steven; Wolters, Sander 1 2014 An application of computable distributions to the semantics of probabilistic programs. Zbl 07311043Huang, Daniel; Morrisett, Greg; Spitters, Bas 1 2021 Synthetic topology in homotopy type theory for probabilistic programming. Zbl 1517.68072Bidlingmaier, Martin E.; Faissole, Florian; Spitters, Bas 1 2021 Modalities in homotopy type theory. Zbl 1489.03005Rijke, Egbert; Shulman, Michael; Spitters, Bas 16 2020 Modal dependent type theory and dependent right adjoints. Zbl 1479.03011Birkedal, Lars; Clouston, Ranald; Mannaa, Bassel; Ejlers Møgelberg, Rasmus; Pitts, Andrew M.; Spitters, Bas 7 2020 Guarded cubical type theory. Zbl 1477.03034Birkedal, Lars; Bizjak, Aleš; Clouston, Ranald; Grathwohl, Hans Bugge; Spitters, Bas; Vezzosi, Andrea 4 2019 Internal universes in models of homotopy type theory. Zbl 1462.03010Licata, Daniel R.; Orton, Ian; Pitts, Andrew M.; Spitters, Bas 13 2018 Guarded cubical type theory: path equality for guarded recursion. Zbl 1370.68052Birkedal, Lars; Bizjak, Aleš; Clouston, Ranald; Grathwohl, Hans Bugge; Spitters, Bas; Vezzosi, Andrea 5 2016 Sets in homotopy type theory. Zbl 1362.03007Rijke, Egbert; Spitters, Bas 6 2015 Gelfand spectra in Grothendieck toposes using geometric mathematics. Zbl 1471.81044Spitters, Bas; Vickers, Steven; Wolters, Sander 1 2014 Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002The Univalent Foundations Program 128 2013 The Picard algorithm for ordinary differential equations in Coq. Zbl 1317.68222Makarov, Evgeny; Spitters, Bas 14 2013 Type classes for efficient exact real arithmetic in Coq. Zbl 1260.68378Krebbers, Robbert; Spitters, Bas 8 2013 Bohrification of operator algebras and quantum logic. Zbl 1275.03166Heunen, Chris; Landsman, Nicolaas P.; Spitters, Bas 16 2012 The space of measurement outcomes as a spectral invariant for non-commutative algebras. Zbl 1259.81013Spitters, Bas 4 2012 8th international workshop on quantum physics and logic, Nijmegen, Netherlands, October 27–29, 2011. Proceedings. Zbl 1391.81010 2 2012 Type classes for mathematics in type theory. Zbl 1223.68105Spitters, Bas; van der Weegen, Eelis 13 2011 The Gelfand spectrum of a noncommutative \(C^*\)-algebra: a topos-theoretic approach. Zbl 1223.46062Heunen, Chris; Landsman, Nicolaas P.; Spitters, Bas; Wolters, Sander 11 2011 Bohrification. Zbl 1234.81025Heunen, Chris; Landsman, Nicolaas P.; Spitters, Bas 4 2011 Computer certified efficient exact reals in Coq. Zbl 1260.68377Krebbers, Robbert; Spitters, Bas 4 2011 Metric complements of overt closed sets. Zbl 1251.03084Coquand, Thierry; Palmgren, Erik; Spitters, Bas 2 2011 A computer-verified monadic functional implementation of the integral. Zbl 1209.68108O’Connor, Russell; Spitters, Bas 9 2010 Developing the algebraic hierarchy with type classes in Coq. Zbl 1291.68370Spitters, Bas; van der Weegen, Eelis 3 2010 Constructive theory of Banach algebras. Zbl 1285.03073Coquand, Thierry; Spitters, Bas 1 2010 Locatedness and overt sublocales. Zbl 1223.03053Spitters, Bas 1 2010 A topos for algebraic quantum theory. Zbl 1209.81147Heunen, Chris; Landsman, Nicolaas P.; Spitters, Bas 40 2009 Integrals and valuations. Zbl 1245.03098Coquand, Thierry; Spitters, Bas 12 2009 Intuitionistic quantum logic of an \(n\)-level system. Zbl 1206.81012Caspers, Martijn; Heunen, Chris; Landsman, Nicolaas P.; Spitters, Bas 11 2009 Constructive Gelfand duality for C\(^*\)-algebras. Zbl 1183.46052Coquand, Thierry; Spitters, Bas 7 2009 The principle of general tovariance. Zbl 1153.83335Heunen, C.; Landsman, N. P.; Spitters, B. 1 2008 Constructive analysis, types and exact real numbers. Zbl 1157.03036Geuvers, Herman; Niqui, Milad; Spitters, Bas; Wiedijk, Freek 7 2007 A constructive view on ergodic theorems. Zbl 1106.03052Spitters, Bas 3 2006 Constructive algebraic integration theory. Zbl 1099.28009Spitters, Bas 2 2006 Formal topology and constructive mathematics: the Gelfand and Stone-Yosida representation theorems. Zbl 1120.03049Coquand, T.; Spitters, B. 8 2005 Constructive results on operator algebras. Zbl 1125.46059Spitters, B. 2 2005 Program extraction from large proof developments. Zbl 1279.68287Cruz-Filipe, Luís; Spitters, Bas 5 2003 Locating the range of an operator with an adjoint. Zbl 1092.47063Bridges, Douglas; Ishihara, Hajime; Spitters, Bas 2 2002 Located operators. Zbl 1041.03050Spitters, Bas 2 2002 all cited Publications top 5 cited Publications all top 5 Cited by 235 Authors 18 Spitters, Bas 9 Heunen, Chris 6 Coquand, Thierry 5 Hamhalter, Jan 5 Melquiond, Guillaume 5 Turilova, Ekaterina A. 4 Boldo, Sylvie 4 Döring, Andreas 4 Landsman, Nicolaas P. 4 Rijke, Egbert 3 Birkedal, Lars 3 Bridges, Douglas Suth 3 Heras, Jónathan 3 Kavvos, G. A. 3 Mahboubi, Assia 3 Møgelberg, Rasmus Ejlers 3 Nakayama, Kunji 3 O’Connor, Russell 3 Pitts, Andrew M. 3 Platzer, André 3 Sattler, Christian 3 Théry, Laurent 3 Wolters, Sander A. M. 2 Avigad, Jeremy 2 Berger, Ulrich 2 Bizjak, Aleš 2 Bohrer, Rose 2 Chen, Wei 2 Chhetri, Bishal 2 Christensen, J. Daniel 2 Clément, François 2 Clouston, Ranald A. 2 Cruz-Filipe, Luís 2 de Ronde, Christian 2 Domenech, Graciela 2 Domínguez, César 2 Faissole, Florian 2 Freytes, Hector 2 Gratzer, Daniel 2 Hölzl, Johannes 2 Huber, Simon 2 Immler, Fabian 2 Ishihara, Hajime 2 Jacobs, Bart 2 Karakostas, Vassilios 2 Kawai, Tatsuji 2 Krebbers, Robbert 2 Lelay, Catherine 2 Lin, Bingsheng 2 Mannaa, Bassel 2 Mayero, Micaela 2 Mörtberg, Anders 2 Orton, Ian 2 Pientka, Brigitte 2 Reyes, Manuel L. 2 Rubio García, Julio Jesús 2 Sakaguchi, Kazuhiko 2 Sanjeevi, Carani B. 2 Schneider-Kamp, Peter 2 Schöpp, Ulrich 2 Scoccola, Luis Nerio 2 Shulman, Michael A. 2 Sibut-Pinote, Thomas 2 Steinberg, Florian 2 Thies, Holger 2 Uemura, Taichi 2 Vamsi, Dasu Krishna Kiran 2 Vezzosi, Andrea 2 Zafiris, Elias 1 Abel, Andreas M. 1 Abramsky, Samson 1 Affeldt, Reynald 1 Ahman, Danel 1 Alama, Jesse 1 Anand, Abhishek 1 Ananth, V. S. 1 Anel, Mathieu 1 Angiuli, Carlo 1 Annenkov, Danil 1 Audebaud, Philippe 1 Bahr, Patrick 1 Bain, Jonathan 1 Barnum, Howard 1 Basold, Henning 1 Ben-Zvi, Michael 1 Bertot, Yves 1 Bertozzini, Paolo 1 Bhagat, Vijay M. 1 Bickford, Mark 1 Bidlingmaier, Martin E. 1 Biedermann, Georg 1 Bielas, Krzysztof 1 Blechschmidt, Ingo 1 Bohrer, Brandon 1 Boulier, Simon 1 Boulmé, Sylvain 1 Brandenburger, Adam 1 Brink, Kasper 1 Brogi, Cosimo Perini 1 Brunerie, Guillaume ...and 135 more Authors all top 5 Cited in 50 Serials 17 MSCS. Mathematical Structures in Computer Science 12 Journal of Automated Reasoning 10 Logical Methods in Computer Science 7 Journal of Mathematical Physics 7 Foundations of Physics 5 Communications in Mathematical Physics 5 International Journal of Theoretical Physics 4 Synthese 4 Theoretical Computer Science 4 Annals of Pure and Applied Logic 3 Mathematical Logic Quarterly (MLQ) 3 Journal of Functional Programming 2 Advances in Mathematics 2 Studia Logica 2 Transactions of the American Mathematical Society 2 Order 2 The Bulletin of Symbolic Logic 2 ACM Transactions on Computational Logic 2 Mathematics in Computer Science 2 Studies in History and Philosophy of Science. Part B. Studies in History and Philosophy of Modern Physics 2 Computational and Mathematical Biophysics 2 Higher Structures 1 Israel Journal of Mathematics 1 Journal of Mathematical Analysis and Applications 1 Mathematical Proceedings of the Cambridge Philosophical Society 1 Journal of Algebra 1 Journal of Pure and Applied Algebra 1 The Journal of Symbolic Logic 1 Science of Computer Programming 1 Formal Aspects of Computing 1 International Journal of Mathematics 1 Expositiones Mathematicae 1 Archive for Mathematical Logic 1 Indagationes Mathematicae. New Series 1 Applicable Algebra in Engineering, Communication and Computing 1 Applied Categorical Structures 1 Journal of Mathematical Sciences (New York) 1 Theory and Applications of Categories 1 Annals of Mathematics and Artificial Intelligence 1 Theory of Computing Systems 1 Soft Computing 1 New Journal of Physics 1 Lobachevskii Journal of Mathematics 1 Journal of the Australian Mathematical Society 1 Journal of Applied Logic 1 Oberwolfach Reports 1 Journal of Physics A: Mathematical and Theoretical 1 Journal of Logic and Analysis 1 Mathematics 1 Philosophical Transactions A. Royal Society of London all top 5 Cited in 35 Fields 87 Mathematical logic and foundations (03-XX) 61 Computer science (68-XX) 47 Category theory; homological algebra (18-XX) 44 Quantum theory (81-XX) 32 Functional analysis (46-XX) 19 Order, lattices, ordered algebraic structures (06-XX) 16 Algebraic topology (55-XX) 9 General topology (54-XX) 7 Measure and integration (28-XX) 7 Numerical analysis (65-XX) 5 General and overarching topics; collections (00-XX) 5 Operator theory (47-XX) 4 Associative rings and algebras (16-XX) 4 Nonassociative rings and algebras (17-XX) 4 Real functions (26-XX) 4 Dynamical systems and ergodic theory (37-XX) 3 Ordinary differential equations (34-XX) 3 Partial differential equations (35-XX) 3 Biology and other natural sciences (92-XX) 2 Commutative algebra (13-XX) 2 Algebraic geometry (14-XX) 2 Calculus of variations and optimal control; optimization (49-XX) 2 Convex and discrete geometry (52-XX) 2 Probability theory and stochastic processes (60-XX) 2 Systems theory; control (93-XX) 1 Number theory (11-XX) 1 Field theory and polynomials (12-XX) 1 Linear and multilinear algebra; matrix theory (15-XX) 1 Group theory and generalizations (20-XX) 1 Topological groups, Lie groups (22-XX) 1 Statistics (62-XX) 1 Mechanics of particles and systems (70-XX) 1 Relativity and gravitational theory (83-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year