Bas Spitters

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