Bas Spitters

Publication Activity (10 Years)

Years Active: 2002-2024
Publications (10 Years): 47

Top Topics

Stochastic Grammar

Theoretical Framework

Functional Programs

Top Venues

IACR Cryptol. ePrint Arch.

Publications

Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Catalin Hritcu, Bas Spitters
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography. CPP (2024)
Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Catalin Hritcu, Kenji Maillard, Bas Spitters
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. ACM Trans. Program. Lang. Syst. 45 (3) (2023)
Eske Hoy Nielsen, Danil Annenkov, Bas Spitters
Formalising Decentralised Exchanges in Coq. CPP (2023)
Benjamin Salling Hvass, Diego F. Aranha, Bas Spitters
High-Assurance Field Inversion for Curve-Based Cryptography. CSF (2023)
Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Catalin Hritcu, Bas Spitters
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography. IACR Cryptol. ePrint Arch. 2023 (2023)
Diego F. Aranha, Benjamin Salling Hvass, Bas Spitters, Mehdi Tibouchi
Faster constant-time evaluation of the Kronecker symbol with application to elliptic curve hashing. IACR Cryptol. ePrint Arch. 2023 (2023)
Diego F. Aranha, Benjamin Salling Hvass, Bas Spitters, Mehdi Tibouchi
Faster Constant-time Evaluation of the Kronecker Symbol with Application to Elliptic Curve Hashing. CCS (2023)
Eske Hoy Nielsen, Danil Annenkov, Bas Spitters
Formalising Decentralised Exchanges in Coq. CoRR (2022)
Mikkel Milo, Eske Hoy Nielsen, Danil Annenkov, Bas Spitters
Finding smart contract vulnerabilities with ConCert's property-based testing framework. CoRR (2022)
Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters
Extracting functional programs from Coq, in Coq. J. Funct. Program. 32 (2022)
Mikkel Milo, Eske Hoy Nielsen, Danil Annenkov, Bas Spitters
Finding Smart Contract Vulnerabilities with ConCert's Property-Based Testing Framework. FMBC@CAV (2022)
Benjamin Salling Hvass, Diego F. Aranha, Bas Spitters
High-assurance field inversion for curve-based cryptography. IACR Cryptol. ePrint Arch. 2021 (2021)
Søren Eller Thomsen, Bas Spitters
Formalizing Nakamoto-Style Proof of Stake. CSF (2021)
Nikolaj Sidorenco, Sabine Oechsner, Bas Spitters
Formal security analysis of MPC-in-the-head zero-knowledge protocols. IACR Cryptol. ePrint Arch. 2021 (2021)
Nikolaj Sidorenco, Sabine Oechsner, Bas Spitters
Formal security analysis of MPC-in-the-head zero-knowledge protocols. CSF (2021)
Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard, Bas Spitters
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. IACR Cryptol. ePrint Arch. 2021 (2021)
Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard, Bas Spitters
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. CSF (2021)
Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters
Extracting smart contracts tested and verified in Coq. CPP (2021)
Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters
Extracting functional programs from Coq, in Coq. CoRR (2021)
Martin E. Bidlingmaier, Florian Faissole, Bas Spitters
Synthetic topology in Homotopy Type Theory for probabilistic programming. Math. Struct. Comput. Sci. 31 (10) (2021)
Danil Annenkov, Jakob Botsch Nielsen, Bas Spitters
ConCert: a smart contract certification framework in Coq. CPP (2020)
Lars Birkedal, Ranald Clouston, Bassel Mannaa, Rasmus Ejlers Møgelberg, Andrew M. Pitts, Bas Spitters
Modal dependent type theory and dependent right adjoints. Math. Struct. Comput. Sci. 30 (2) (2020)
Søren Eller Thomsen, Bas Spitters
Formalizing Nakamoto-Style Proof of Stake. IACR Cryptol. ePrint Arch. 2020 (2020)
Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters
Extracting Smart Contracts Tested and Verified in Coq. CoRR (2020)
Søren Eller Thomsen, Bas Spitters
Formalizing Nakamoto-Style Proof of Stake. CoRR (2020)
Egbert Rijke, Michael Shulman, Bas Spitters
Modalities in homotopy type theory. Log. Methods Comput. Sci. 16 (1) (2020)
Jakob Botsch Nielsen, Bas Spitters
Smart Contract Interactions in Coq. FM Workshops (1) (2019)
Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi
Guarded Cubical Type Theory. J. Autom. Reason. 63 (2) (2019)
Danil Annenkov, Bas Spitters
Towards a Smart Contract Verification Framework in Coq. CoRR (2019)
Martin E. Bidlingmaier, Florian Faissole, Bas Spitters
Synthetic topology in Homotopy Type Theory for probabilistic programming. CoRR (2019)
Jakob Botsch Nielsen, Bas Spitters
Smart Contract Interactions in Coq. CoRR (2019)
Daniel R. Licata, Ian Orton, Andrew M. Pitts, Bas Spitters
Internal Universes in Models of Homotopy Type Theory. CoRR (2018)
Jonathan Sterling, Bas Spitters
Normalization by gluing for free λ-theories. CoRR (2018)
Ranald Clouston, Bassel Mannaa, Rasmus Ejlers Møgelberg, Andrew M. Pitts, Bas Spitters
Modal Dependent Type Theory and Dependent Right Adjoints. CoRR (2018)
Daniel R. Licata, Ian Orton, Andrew M. Pitts, Bas Spitters
Internal Universes in Models of Homotopy Type Theory. FSCD (2018)
Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner, Bas Spitters, Pierre-Yves Strub
Computer-aided proofs for multiparty computation with active security. IACR Cryptol. ePrint Arch. 2018 (2018)
Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner, Bas Spitters, Pierre-Yves Strub
Computer-Aided Proofs for Multiparty Computation with Active Security. CSF (2018)
Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner, Bas Spitters, Pierre-Yves Strub
Computer-aided proofs for multiparty computation with active security. CoRR (2018)
Daniel Huang, Greg Morrisett, Bas Spitters
An Application of Computable Distributions to the Semantics of Probabilistic Programs. CoRR (2018)
Egbert Rijke, Michael Shulman, Bas Spitters
Modalities in homotopy type theory. CoRR (2017)
Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters
The HoTT library: a formalization of homotopy type theory in Coq. CPP (2017)
Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi
Guarded Cubical Type Theory: Path Equality for Guarded Recursion. CSL (2016)
Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi
Guarded Cubical Type Theory: Path Equality for Guarded Recursion. CoRR (2016)
Bas Spitters
Cubical sets and the topological topos. CoRR (2016)
Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters
The HoTT Library: A formalization of homotopy type theory in Coq. CoRR (2016)
Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi
Guarded Cubical Type Theory. CoRR (2016)
Egbert Rijke, Bas Spitters
Sets in homotopy type theory. Math. Struct. Comput. Sci. 25 (5) (2015)
Evgeny Makarov, Bas Spitters
The Picard Algorithm for Ordinary Differential Equations in Coq. ITP (2013)
Egbert Rijke, Bas Spitters
Sets in homotopy type theory CoRR (2013)
Thierry Coquand, Bas Spitters
A constructive proof of Simpson's Rule. J. Log. Anal. 4 (2012)
Bas Spitters, Steven Vickers, Sander Wolters
Gelfand spectra in Grothendieck toposes using geometric mathematics. QPL (2012)
Chris Heunen, Nicolaas P. Landsman, Bas Spitters
Bohrification of operator algebras and quantum logic. Synth. 186 (3) (2012)
Robbert Krebbers, Bas Spitters
Computer certified efficient exact reals in Coq CoRR (2011)
Robbert Krebbers, Bas Spitters
Type classes for efficient exact real arithmetic in Coq Log. Methods Comput. Sci. 9 (1) (2011)
Robbert Krebbers, Bas Spitters
Computer Certified Efficient Exact Reals in Coq. Calculemus/MKM (2011)
Bas Spitters, Eelis van der Weegen
Type Classes for Mathematics in Type Theory CoRR (2011)
Bas Spitters, Eelis van der Weegen
Type classes for mathematics in type theory. Math. Struct. Comput. Sci. 21 (4) (2011)
Thierry Coquand, Erik Palmgren, Bas Spitters
Metric complements of overt closed sets. Math. Log. Q. 57 (4) (2011)
Bas Spitters
The space of measurement outcomes as a spectrum for non-commutative algebras DCM (2010)
Bas Spitters
Locatedness and overt sublocales. Ann. Pure Appl. Log. 162 (1) (2010)
Russell O'Connor, Bas Spitters
A computer-verified monadic functional implementation of the integral. Theor. Comput. Sci. 411 (37) (2010)
Bas Spitters, Eelis van der Weegen
Developing the Algebraic Hierarchy with Type Classes in Coq. ITP (2010)
Thierry Coquand, Bas Spitters
Constructive theory of Banach algebras. J. Log. Anal. 2 (2010)
Bas Spitters
Constructive Pointfree Topology Eliminates Non-constructive Representation Theorems from Riesz Space Theory. Order 27 (2) (2010)
Thierry Coquand, Bas Spitters
Integrals and valuations. J. Log. Anal. 1 (2009)
Bas Spitters, Russell O'Connor
Computer Verified Exact Analysis (Tutorial). CCA (2009)
Russell O'Connor, Bas Spitters
A computer verified, monadic, functional implementation of the integral CoRR (2008)
Bas Spitters, Herman Geuvers, Milad Niqui, Freek Wiedijk
Preface to the special issue: Constructive analysis, types and exact real numbers. Math. Struct. Comput. Sci. 17 (1) (2007)
Herman Geuvers, Milad Niqui, Bas Spitters, Freek Wiedijk
Constructive analysis, types and exact real numbers. Math. Struct. Comput. Sci. 17 (1) (2007)
Bas Spitters
Constructive algebraic integration theory. Ann. Pure Appl. Log. 137 (1-3) (2006)
Bas Spitters
Corrigendum to: 'A constructive view on ergodic theorems'. J. Symb. Log. 71 (4) (2006)
Bas Spitters
A constructive view on ergodic theorems. J. Symb. Log. 71 (2) (2006)
Bas Spitters
Constructive Results on Operator Algebras. J. Univers. Comput. Sci. 11 (12) (2005)
Bas Spitters
Almost periodic functions, constructively. Log. Methods Comput. Sci. 1 (3) (2005)
Thierry Coquand, Bas Spitters
A constructive proof of the Peter-Weyl theorem. Math. Log. Q. 51 (4) (2005)
Bas Spitters
Almost periodic functions, constructively CoRR (2005)
Thierry Coquand, Bas Spitters
Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems. J. Univers. Comput. Sci. 11 (12) (2005)
Bas Spitters
Constructive algebraic integration theory without choice. Mathematics, Algorithms, Proofs (2005)
Luís Cruz-Filipe, Bas Spitters
Program Extraction from Large Proof Developments. TPHOLs (2003)
Bas Spitters
Located Operators. Math. Log. Q. 48 (S1) (2002)