Bas Spitters

According to our database, Bas Spitters authored at least 56 papers between 2002 and 2023.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

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., September, 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

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

Formalising Decentralised Exchanges in Coq.

Eske Hoy Nielsen, Danil Annenkov, Bas Spitters

Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023

2022

Extracting functional programs from Coq, in Coq.

Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters

J. Funct. Program., 2022

Finding Smart Contract Vulnerabilities with ConCert's Property-Based Testing Framework.

Mikkel Milo, Eske Hoy Nielsen, Danil Annenkov, Bas Spitters

Proceedings of the 4th International Workshop on Formal Methods for Blockchains, 2022

2021

Synthetic topology in Homotopy Type Theory for probabilistic programming.

Martin E. Bidlingmaier, Florian Faissole, Bas Spitters

Math. Struct. Comput. Sci., 2021

Formal security analysis of MPC-in-the-head zero-knowledge protocols.

Nikolaj Sidorenco, Sabine Oechsner, 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

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

Extracting smart contracts tested and verified in Coq.

Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters

Proceedings of the CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021

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

Modalities in homotopy type theory.

Egbert Rijke, Michael Shulman, Bas Spitters

Log. Methods Comput. Sci., 2020

Formalizing Nakamoto-Style Proof of Stake.

Søren Eller Thomsen, Bas Spitters

IACR Cryptol. ePrint Arch., 2020

ConCert: a smart contract certification framework in Coq.

Danil Annenkov, Jakob Botsch Nielsen, Bas Spitters

Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

2019

Guarded Cubical Type Theory.

Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi

J. Autom. Reason., 2019

Towards a Smart Contract Verification Framework in Coq.

Danil Annenkov, Bas Spitters

CoRR, 2019

Smart Contract Interactions in Coq.

Jakob Botsch Nielsen, Bas Spitters

Proceedings of the Formal Methods. FM 2019 International Workshops, 2019

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

Normalization by gluing for free λ-theories.

Jonathan Sterling, Bas Spitters

CoRR, 2018

An Application of Computable Distributions to the Semantics of Probabilistic Programs.

Daniel Huang, Greg Morrisett, Bas Spitters

CoRR, 2018

Modal Dependent Type Theory and Dependent Right Adjoints.

Ranald Clouston, Bassel Mannaa, Rasmus Ejlers Møgelberg, Andrew M. Pitts, Bas Spitters

CoRR, 2018

Internal Universes in Models of Homotopy Type Theory.

Daniel R. Licata, Ian Orton, Andrew M. Pitts, Bas Spitters

Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, 2018

2017

The HoTT library: a formalization of homotopy type theory in Coq.

Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

2016

Cubical sets and the topological topos.

Bas Spitters

CoRR, 2016

Guarded Cubical Type Theory: Path Equality for Guarded Recursion.

Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi

Proceedings of the 25th EACSL Annual Conference on Computer Science Logic, 2016

2015

Sets in homotopy type theory.

Egbert Rijke, Bas Spitters

Math. Struct. Comput. Sci., 2015

2013

The Picard Algorithm for Ordinary Differential Equations in Coq.

Evgeny Makarov, Bas Spitters

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012

Bohrification of operator algebras and quantum logic.

Chris Heunen, Nicolaas P. Landsman, Bas Spitters

Synth., 2012

A constructive proof of Simpson's Rule.

Thierry Coquand, Bas Spitters

J. Log. Anal., 2012

Gelfand spectra in Grothendieck toposes using geometric mathematics.

Bas Spitters, Steven Vickers, Sander Wolters

Proceedings of the Proceedings 9th Workshop on Quantum Physics and Logic, 2012

2011

Type classes for mathematics in type theory.

Bas Spitters, Eelis van der Weegen

Math. Struct. Comput. Sci., 2011

Metric complements of overt closed sets.

Thierry Coquand, Erik Palmgren, Bas Spitters

Math. Log. Q., 2011

Type classes for efficient exact real arithmetic in Coq

Robbert Krebbers, Bas Spitters

Log. Methods Comput. Sci., 2011

Computer Certified Efficient Exact Reals in Coq.

Robbert Krebbers, Bas Spitters

Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

2010

A computer-verified monadic functional implementation of the integral.

Russell O'Connor, Bas Spitters

Theor. Comput. Sci., 2010

Constructive Pointfree Topology Eliminates Non-constructive Representation Theorems from Riesz Space Theory.

Bas Spitters

Order, 2010

Constructive theory of Banach algebras.

Thierry Coquand, Bas Spitters

J. Log. Anal., 2010

The space of measurement outcomes as a spectrum for non-commutative algebras

Bas Spitters

Proceedings of the Proceedings Sixth Workshop on Developments in Computational Models: Causality, 2010

Locatedness and overt sublocales.

Bas Spitters

Ann. Pure Appl. Log., 2010

Developing the Algebraic Hierarchy with Type Classes in Coq.

Bas Spitters, Eelis van der Weegen

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

2009

Integrals and valuations.

Thierry Coquand, Bas Spitters

J. Log. Anal., 2009

Computer Verified Exact Analysis (Tutorial).

Bas Spitters, Russell O'Connor

Proceedings of the Sixth International Conference on Computability and Complexity in Analysis, 2009

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

Constructive analysis, types and exact real numbers.

Herman Geuvers, Milad Niqui, Bas Spitters, Freek Wiedijk

Math. Struct. Comput. Sci., 2007

2006

Corrigendum to: 'A constructive view on ergodic theorems'.

Bas Spitters

J. Symb. Log., 2006

A constructive view on ergodic theorems.

Bas Spitters

J. Symb. Log., 2006

Constructive algebraic integration theory.

Bas Spitters

Ann. Pure Appl. Log., 2006

2005

A constructive proof of the Peter-Weyl theorem.

Thierry Coquand, Bas Spitters

Math. Log. Q., 2005

Almost periodic functions, constructively.

Bas Spitters

Log. Methods Comput. Sci., 2005

Constructive Results on Operator Algebras.

Bas Spitters

J. Univers. Comput. Sci., 2005

Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems.

Thierry Coquand, Bas Spitters

J. Univers. Comput. Sci., 2005

Constructive algebraic integration theory without choice.

Bas Spitters

Proceedings of the Mathematics, Algorithms, Proofs, 9.-14. January 2005, 2005

Approximating integrable sets by compacts constructively.

Bas Spitters

Proceedings of the From sets and types to topology and analysis, 2005

2003

Program Extraction from Large Proof Developments.

Luís Cruz-Filipe, Bas Spitters

Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003

2002

Located Operators.

Bas Spitters

Math. Log. Q., 2002