Located Operators. - Bas Spitters (Math. Log. Q., 2002)

Program Extraction from Large Proof Developments. - Luís Cruz-Filipe; Bas Spitters (TPHOLs, 2003)

Approximating integrable sets by compacts constructively. - Bas Spitters (From sets and types to topology and analysis, 2005)

Constructive algebraic integration theory without choice. - Bas Spitters (Mathematics, Algorithms, Proofs, 2005)

Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems. - Thierry Coquand; Bas Spitters (J. Univers. Comput. Sci., 2005)

Constructive Results on Operator Algebras. - Bas Spitters (J. Univers. Comput. Sci., 2005)

Almost periodic functions, constructively. - Bas Spitters (Log. Methods Comput. Sci., 2005)

A constructive proof of the Peter-Weyl theorem. - Thierry Coquand; Bas Spitters (Math. Log. Q., 2005)

Constructive algebraic integration theory. - Bas Spitters (Ann. Pure Appl. Log., 2006)

A constructive view on ergodic theorems. - Bas Spitters (J. Symb. Log., 2006)

Corrigendum to: 'A constructive view on ergodic theorems'. - Bas Spitters (J. Symb. Log., 2006)

Constructive analysis, types and exact real numbers. - Herman Geuvers; Milad Niqui; Bas Spitters; Freek Wiedijk (Math. Struct. Comput. Sci., 2007)

Preface to the special issue: Constructive analysis, types and exact real numbers. - Bas Spitters; Herman Geuvers; Milad Niqui; Freek Wiedijk (Math. Struct. Comput. Sci., 2007)

Computer Verified Exact Analysis (Tutorial). - Bas Spitters; Russell O'Connor (CCA, 2009)

Integrals and valuations. - Thierry Coquand; Bas Spitters (J. Log. Anal., 2009)

Developing the Algebraic Hierarchy with Type Classes in Coq. - Bas Spitters; Eelis van der Weegen (ITP, 2010)

Locatedness and overt sublocales. - Bas Spitters (Ann. Pure Appl. Log., 2010)

The space of measurement outcomes as a spectrum for non-commutative algebras - Bas Spitters (DCM, 2010)

Constructive theory of Banach algebras. - Thierry Coquand; Bas Spitters (J. Log. Anal., 2010)

Constructive Pointfree Topology Eliminates Non-constructive Representation Theorems from Riesz Space Theory. - Bas Spitters (Order, 2010)

A computer-verified monadic functional implementation of the integral. - Russell O'Connor; Bas Spitters (Theor. Comput. Sci., 2010)

Computer Certified Efficient Exact Reals in Coq. - Robbert Krebbers; Bas Spitters (Calculemus/MKM, 2011)

Type classes for efficient exact real arithmetic in Coq - Robbert Krebbers; Bas Spitters (Log. Methods Comput. Sci., 2011)

Metric complements of overt closed sets. - Thierry Coquand; Erik Palmgren; Bas Spitters (Math. Log. Q., 2011)

Type classes for mathematics in type theory. - Bas Spitters; Eelis van der Weegen (Math. Struct. Comput. Sci., 2011)

Gelfand spectra in Grothendieck toposes using geometric mathematics. - Bas Spitters; Steven Vickers; Sander Wolters (QPL, 2012)

A constructive proof of Simpson's Rule. - Thierry Coquand; Bas Spitters (J. Log. Anal., 2012)

Bohrification of operator algebras and quantum logic. - Chris Heunen; Nicolaas P. Landsman; Bas Spitters (Synth., 2012)

The Picard Algorithm for Ordinary Differential Equations in Coq. - Evgeny Makarov; Bas Spitters (ITP, 2013)

Sets in homotopy type theory. - Egbert Rijke; Bas Spitters (Math. Struct. Comput. Sci., 2015)

Guarded Cubical Type Theory: Path Equality for Guarded Recursion. - Lars Birkedal; Ales Bizjak; Ranald Clouston; Hans Bugge Grathwohl; Bas Spitters; Andrea Vezzosi (CSL, 2016)

Cubical sets and the topological topos. - Bas Spitters (CoRR, 2016)

The HoTT library: a formalization of homotopy type theory in Coq. - Andrej Bauer; Jason Gross; Peter LeFanu Lumsdaine; Michael Shulman; Matthieu Sozeau; Bas Spitters (CPP, 2017)

Internal Universes in Models of Homotopy Type Theory. - Daniel R. Licata; Ian Orton; Andrew M. Pitts; Bas Spitters (FSCD, 2018)

Modal Dependent Type Theory and Dependent Right Adjoints. - Ranald Clouston; Bassel Mannaa; Rasmus Ejlers Møgelberg; Andrew M. Pitts; Bas Spitters (CoRR, 2018)

An Application of Computable Distributions to the Semantics of Probabilistic Programs. - Daniel Huang 001; Greg Morrisett; Bas Spitters (CoRR, 2018)

Normalization by gluing for free λ-theories. - Jonathan Sterling; Bas Spitters (CoRR, 2018)

Computer-aided proofs for multiparty computation with active security. - Helene Haagh; Aleksandr Karbyshev; Sabine Oechsner; Bas Spitters; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 2018)

Smart Contract Interactions in Coq. - Jakob Botsch Nielsen; Bas Spitters (FM Workshops (1), 2019)

Towards a Smart Contract Verification Framework in Coq. - Danil Annenkov; Bas Spitters (CoRR, 2019)

Guarded Cubical Type Theory. - Lars Birkedal; Ales Bizjak; Ranald Clouston; Hans Bugge Grathwohl; Bas Spitters; Andrea Vezzosi (J. Autom. Reason., 2019)

Application ofComputable Distributions to the Semantics of Probabilistic Programs. - Daniel Huang 001; Greg Morrisett; Bas Spitters (Foundations of Probabilistic Programming, 2020)

ConCert: a smart contract certification framework in Coq. - Danil Annenkov; Jakob Botsch Nielsen; Bas Spitters (CPP, 2020)

Formalizing Nakamoto-Style Proof of Stake. - Søren Eller Thomsen; Bas Spitters (IACR Cryptol. ePrint Arch., 2020)

Modalities in homotopy type theory. - Egbert Rijke; Michael Shulman; Bas Spitters (Log. Methods Comput. Sci., 2020)

Modal dependent type theory and dependent right adjoints. - Lars Birkedal; Ranald Clouston; Bassel Mannaa; Rasmus Ejlers Møgelberg; Andrew M. Pitts; Bas Spitters (Math. Struct. Comput. Sci., 2020)

Extracting smart contracts tested and verified in Coq. - Danil Annenkov; Mikkel Milo; Jakob Botsch Nielsen; Bas Spitters (CPP, 2021)

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. - Carmine Abate; Philipp G. Haselwarter; Exequiel Rivas; Antoine Van Muylder; Théo Winterhalter; Catalin Hritcu; Kenji Maillard; Bas Spitters (IACR Cryptol. ePrint Arch., 2021)

High-assurance field inversion for curve-based cryptography. - Benjamin Salling Hvass; Diego F. Aranha; Bas Spitters (IACR Cryptol. ePrint Arch., 2021)

Formal security analysis of MPC-in-the-head zero-knowledge protocols. - Nikolaj Sidorenco; Sabine Oechsner; Bas Spitters (IACR Cryptol. ePrint Arch., 2021)

Synthetic topology in Homotopy Type Theory for probabilistic programming. - Martin E. Bidlingmaier; Florian Faissole; Bas Spitters (Math. Struct. Comput. Sci., 2021)

Finding Smart Contract Vulnerabilities with ConCert's Property-Based Testing Framework. - Mikkel Milo; Eske Hoy Nielsen; Danil Annenkov; Bas Spitters (FMBC@CAV, 2022)

Extracting functional programs from Coq, in Coq. - Danil Annenkov; Mikkel Milo; Jakob Botsch Nielsen; Bas Spitters (J. Funct. Program., 2022)

Formalising Decentralised Exchanges in Coq. - Eske Hoy Nielsen; Danil Annenkov; Bas Spitters (CPP, 2023)

Faster constant-time evaluation of the Kronecker symbol with application to elliptic curve hashing. - Diego F. Aranha; Benjamin Salling Hvass; Bas Spitters; Mehdi Tibouchi (IACR Cryptol. ePrint Arch., 2023)

The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography. - Philipp G. Haselwarter; Benjamin Salling Hvass; Lasse Letager Hansen; Théo Winterhalter; Catalin Hritcu; Bas Spitters (IACR Cryptol. ePrint Arch., 2023)

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. - Philipp G. Haselwarter; Exequiel Rivas; Antoine Van Muylder; Théo Winterhalter; Carmine Abate; Nikolaj Sidorenco; Catalin Hritcu; Kenji Maillard; Bas Spitters (ACM Trans. Program. Lang. Syst., 2023)

CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoq. - Wolfgang Meier; Martin Jensen; Jean Pichon-Pharabod; Bas Spitters (CPP, 2025)

hax: Verifying Security-Critical Rust Software using Multiple Provers. - Karthikeyan Bhargavan; Maxime Buyse; Lucas Franceschino; Lasse Letager Hansen; Franziskus Kiefer; Jonas Schneider-Bensch; Bas Spitters (IACR Cryptol. ePrint Arch., 2025)

Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust. - Karthikeyan Bhargavan; Lasse Letager Hansen; Franziskus Kiefer; Jonas Schneider-Bensch; Bas Spitters (IACR Cryptol. ePrint Arch., 2025)