Bas Spitters

Research output

Research output per year 2006 2016 2018 2020 2021 2024

• 17 Article in proceedings
• 10 Journal article
• 7 Net publication - Internet publication
• 4 Conference abstract for conference
• 13 More
  • 4 Working paper
  • 3 Preprint
  • 2 Book chapter
  • 2 Paper
  • 2 Conference article

Research output per year

Research output per year

Search results

• 2024

  Modernizing FIPS for safe languages and verified libraries

  Protzenko, J. & Spitters, B., 2024.

  Research output: Contribution to conference › Paper › Research

  File
  5 Downloads (Pure)

• The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography

  Haselwarter, P. G., Hvass, B. S., Hansen, L. L., Winterhalter, T., Hriţcu, C. & Spitters, B., Jan 2024, CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs. Timany, A., Traytel, D., Pientka, B. & Blazy, S. (eds.). Association for Computing Machinery, p. 30-44 15 p.

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  Open Access

  • Specification Language 100%
  • Encryption Scheme 100%
  • Operational Semantics 100%
  • Formal Verification 100%
  • hardware acceleration 100%
• 2023

  Faster constant-time evaluation of the Kronecker symbol with application to elliptic curve hashing

  Aranha, D. F., Hvass, B. S., Spitters, B. & Tibouchi, M., Nov 2023, CCS'23: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security. New York: Association for Computing Machinery, p. 3228-3238 11 p.

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  • Constant Time 100%
  • Kronecker Symbol 100%
  • Hashing 100%
  • Elliptic Curves 100%
  • Elliptic Curve 100%
  2 Citations (Scopus)

• Formalising Decentralised Exchanges in Coq

  Nielsen, E. H., Annenkov, D. & Spitters, B., Jan 2023, CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs. Krebbers, R., Traytel, D., Pientka, B. & Zdancewic, S. (eds.). New York: Association for Computing Machinery, p. 290-302 13 p.

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  Open Access

  • Formalization 100%
  • Smart Contract 50%
  • Formal Verification 25%
  • Interaction Pattern 25%
  • Blockchain 25%
  5 Citations (Scopus)

• High-assurance field inversion for curve-based cryptography

  Hvass, B. S., Aranha, D. F. & Spitters, B., 2023, 2023 IEEE 36th Computer Security Foundations Symposium (CSF) . IEEE, p. 552-567 16 p. (Proceedings of the IEEE Computer Security Foundations Symposium).

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  • Little's Theorem 100%
  • side-channel 66%
  • Performance Penalty 50%
  • Cryptographic Operation 33%
  • Sensitive Informations 33%
  1 Citation (Scopus)

• SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq

  Haselwarter, P. G., Rivas, E., Van Muylder, A., Winterhalter, T., Abate, C., Sidorenco, N., Hriţcu, C., Maillard, K. & Spitters, B., Jul 2023, In: ACM Transactions on Programming Languages and Systems. 45, 3, p. 61 15.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  • Logic Programming 100%
  • Soundness 50%
  • public-key encryption scheme 50%
  • Data Encryption 50%
  • Case Study 50%
  4 Citations (Scopus)
• 2022

  Extracting functional programs from Coq, in Coq

  Annenkov, D., Milo, M., Nielsen, J. B. & Spitters, B. A. S., Aug 2022, In: Journal of Functional Programming. 32, 5, 60 p., e11.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  File

  • Functional Program 100%
  • Smart Contract 100%
  • Functional Languages 60%
  • Call by Value 20%
  • Target Language 20%
  2 Citations (Scopus)

  23 Downloads (Pure)

• Finding smart contract vulnerabilities with ConCert's property-based testing framework

  Milo, M., Nielsen, E. H., Annenkov, D. & Spitters, B., Aug 2022, 13 p. (FMBC: Formal Methods for Blockchains).

  Research output: Working paper/Preprint › Working paper › Research

  Open Access

  File

  • Vulnerabilities In Smart Contracts 100%
  43 Downloads (Pure)

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

  Milo, M., Nielsen, E. H., Annenkov, D. & Spitters, B., Oct 2022, 4th International Workshop on Formal Methods for Blockchains (FMBC 2022). Dargaye, Z. & Schneidewind, C. (eds.). Dagstuhl Publishing, 13 p. (OpenAccess Series in Informatics, Vol. 105).

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  Open Access

  • Smart Contract 100%
  • Formal Verification 25%
  • Executable Model 25%
  • Case Study 25%
  • Model Specification 25%
  1 Citation (Scopus)
• 2021

  Extracting functional programs from Coq, in Coq

  Annenkov, D., Milo, M., Nielsen, J. B. & Spitters, B., 6 Aug 2021.

  Research output: Working paper/Preprint › Preprint

  File

  • Functional Program 100%
  • Smart Contract 100%
  • Functional Languages 60%
  • Call by Value 20%
  • Target Language 20%
  241 Downloads (Pure)

• Extracting smart contracts tested and verified in Coq

  Annenkov, D., Milo, M., Nielsen, J. B. & Spitters, B., Jan 2021, CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021. Hritcu, C. & Popescu, A. (eds.). Association for Computing Machinery, p. 105-121 17 p.

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  Open Access

  • Smart Contract 100%
  • Decentralized Finance 100%
  • Functional Languages 50%
  • Call by Value 16%
  • Operational Semantics 16%
  10 Citations (Scopus)

• Formalizing Nakamoto-Style Proof of Stake

  Thomsen, S. E. & Spitters, B., 2021, Proceedings - 2021 IEEE 34th Computer Security Foundations Symposium, CSF 2021. IEEE, 15 p.

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  • Blockchain 100%
  • Distributed Systems 66%
  • Liveness 66%
  • Fault Tolerant 33%
  • Consensus Algorithm 33%
  13 Citations (Scopus)

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

  Sidorenco, N., Oechsner, S. & Spitters, B., 2021, Proceedings - 2021 IEEE 34th Computer Security Foundations Symposium, CSF 2021. IEEE, p. 607-620 14 p.

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  • Security Analysis 100%
  • Knowledge Protocol 100%
  • Building-Blocks 20%
  • Knowledge Proof 20%
  • secure multiparty computation 20%
  11 Citations (Scopus)

• SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq

  Abate, C., Haselwarter, P. G., Rivas, E., Muylder, A. V., Winterhalter, T., Hritcu, C., Maillard, K. & Spitters, B., 2021, Cryptology ePrint Archive, p. 397, 1 p.

  Research output: Working paper/Preprint › Preprint

• SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq

  Abate, C., Haselwarter, P. G., Rivas, E., Muylder, A. V., Winterhalter, T., Hriţcu, C., Maillard, K. & Spitters, B., 2021, Proceedings - 2021 IEEE 34th Computer Security Foundations Symposium, CSF 2021. IEEE, 15 p.

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  • Logic Programming 100%
  • Soundness 50%
  14 Citations (Scopus)
• 2020

  Application ofComputable Distributions to the Semantics of Probabilistic Programs

  Huang, D., Morrisett, G. & Spitters, B., 1 Jan 2020, Foundations of Probabilistic Programming. Cambridge University Press, p. 75-120 46 p.

  Research output: Contribution to book/anthology/report/proceeding › Book chapter › Research › peer-review

  Open Access

  • Probabilistic Programs 100%
  • Computability 100%
  • Continuous Distribution 100%
  • Computational Semantics 50%
  • Constructive Mathematics 50%
  5 Citations (Scopus)

• Application of Computable Distributions to the Semantics of Probabilistic Programs

  Huang, D., Morrisett, G. & Spitters, B., 2020, Foundations of Probabilistic Programming. Barthe, G., Katoen, J.-P. & Silva, A. (eds.). Cambridge University Press, p. 75-120 46 p.

  Research output: Contribution to book/anthology/report/proceeding › Book chapter › Research › peer-review

  Open Access
  25 Citations (Scopus)

• ConCert: A smart contract certification framework in Coq

  Annenkov, D., Botsch Nielsen, J. & Spitters, B., 2020, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’20), January 20-21, 2020, New Orleans, LA, USA. New York: Association for Computing Machinery, p. 215-228 14 p.

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  Open Access

  • Smart Contract 100%
  • Metatheory 33%
  • Functional Languages 33%
  • Soundness 33%
  • meta programming 33%
  28 Citations (Scopus)

• Formalizing Nakamoto-Style Proof of Stake

  Thomsen, S. E. & Spitters, B., 23 Jul 2020.

  Research output: Working paper/Preprint › Preprint

  File

  • Blockchain 100%
  • Distributed Systems 66%
  • Liveness 66%
  • Fault Tolerant 33%
  • Consensus Algorithm 33%
  71 Downloads (Pure)

• High-assurance field inversion for pairing-friendly primes

  Hvass, B. S., Aranha, D. F. & Spitters, B., 20 Jul 2020.

  Research output: Contribution to conference › Conference abstract for conference › Research › peer-review

  Open Access

• High-assurance field inversion for pairing-friendly primes

  Hvass, B. S., Aranha, D. F. & Spitters, B., 6 Jul 2020.

  Research output: Contribution to conference › Conference abstract for conference › Research › peer-review

  Open Access

• Modal dependent type theory and dependent right adjoints

  Birkedal, L., Clouston, R., Mannaa, B., Ejlers Møgelberg, R., Pitts, A. M. & Spitters, B., Feb 2020, In: Mathematical Structures in Computer Science. 30, 2, p. 118-138 21 p.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  • Type Theory 100%
  • Dependent Type 100%
  • Adjoints 100%
  • Calculus 14%
  23 Citations (Scopus)

• Modalities in homotopy type theory

  Rijke, E., Shulman, M. & Spitters, B., 1 Jan 2020, In: Logical Methods in Computer Science. 16, 1, p. 2:1-2:79 79 p.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  • Type Theory 100%
  • Homotopy Type 100%
  • Factorization 66%
  • Mathematics 33%
  • Groupoid 33%
  26 Citations (Scopus)

• Smart contract interactions in coq

  Nielsen, J. B. & Spitters, B., Jan 2020, Formal Methods- FM 2019 International Workshops - Revised Selected Papers. Sekerinski, E., Moreira, N., Oliveira, J. N., Ratiu, D., Guidotti, R., Farrell, M., Luckcuck, M., Marmsoler, D., Campos, J., Astarte, T., Gonnord, L., Cerone, A., Couto, L., Dongol, B., Kutrib, M., Monteiro, P. & Delmas, D. (eds.). Cham: Springer, p. 380-391 12 p. (Lecture Notes in Computer Science, Vol. 12232).

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  Open Access

  • Smart Contract 100%
  • Blockchain 50%
  • Functional Languages 25%
  • Partial Specification 25%
  • Executable Model 25%
  7 Citations (Scopus)
• 2019

  ConCert: A Smart Contract Certification Framework in Coq

  Annenkov, D., Nielsen, J. B. & Spitters, B., 2019, arxiv.org, p. 215-228, 14 p.

  Research output: Working paper/Preprint › Working paper › Research › peer-review

  Open Access

  • Smart Contract 100%
  • Metatheory 33%
  • Functional Languages 33%
  • Soundness 33%
  • meta programming 33%

• Guarded Cubical Type Theory

  Birkedal, L., Bizjak, A., Clouston, R., Grathwohl, H. B., Spitters, B. & Vezzosi, A., 2019, In: Journal of Automated Reasoning. 63, 2, p. 211-253 43 p.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  • Type Checking 100%
  • Extensionality 100%
  • Type Theory 100%
  • Small Category 50%
  • Computer Science 50%
  13 Citations (Scopus)

• Smart Contract Interactions in Coq

  Nielsen, J. B. & Spitters, B., Nov 2019, 0 ed., ArXiv.

  Research output: Working paper/Preprint › Working paper › Research › peer-review

  File

  • Smart Contract 100%
  • Blockchain 50%
  • Functional Languages 25%
  • Partial Specification 25%
  • Executable Model 25%
  63 Downloads (Pure)

• Synthetic topology in Homotopy Type Theory for probabilistic programming

  Bidlingmaier, M. E., Faissole, F. & Spitters, B., Dec 2019, ArXiv.

  Research output: Working paper/Preprint › Working paper › Research › peer-review

  File

  • Riesz Theorem 100%
  155 Downloads (Pure)
• 2018

  An Application of Computable Distributions to the Semantics of Probabilistic Programs

  Huang, D., Morrisett, G. & Spitters, B., 20 Jun 2018, 46 p. Cornell University.

  Research output: Other contribution › Net publication - Internet publication › Research

  File

  • Continuous Distribution 100%
  76 Downloads (Pure)

• Computer-aided proofs for multiparty computation with active security

  Haagh, H., Karbyshev, A., Oechsner, S., Spitters, B. & Strub, P.-Y., 19 Jun 2018, 13 p. arxiv.org.

  Research output: Other contribution › Net publication - Internet publication › Research › peer-review

  Open Access

  File

  • Cryptographic Property 100%
  178 Downloads (Pure)

• Computer-Aided Proofs for Multiparty Computation with Active Security

  Haagh, H., Karbyshev, A., Oechsner, S., Spitters, B. & Strub, P., 1 Jul 2018, Proceedings - IEEE 31st Computer Security Foundations Symposium, CSF 2018. Oxford: IEEE, Vol. 2018. p. 119-131 13 p. 8429300. (Proceedings of the IEEE Computer Security Foundations Symposium; No. 31).

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  • Correctness Proofs 100%
  • secure multiparty computation 100%
  • secret sharing scheme 100%
  • public-key encryption 100%
  • high-order logic 100%
  22 Citations (Scopus)

• Internal Universes in Models of Homotopy Type Theory

  Licata, D. R., Orton, I., Pitts, A. M. & Spitters, B., 23 Jan 2018, 17 p. arxiv.org.

  Research output: Other contribution › Net publication - Internet publication › Research › peer-review

  Open Access

  File

  • Homotopy Type Theory 100%
  • Type Theory 100%
  • Homotopy Type 100%
  • Internal Language 66%
  • Axiomatization 66%
  33 Citations (Scopus)

  149 Downloads (Pure)

• Preuves constructives de programmes probabilistes

  Translated title of the contribution: Constructive proofs of probabilistic programsFaissole, F. & Spitters, B., Jan 2018, Journées Francophones des Langages Applicatifs. (Journées Francophones des Langages Applicatifs (JFLA); No. 2018).

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

• Un cadre pour la preuve de programmes probabilistes

  Faissole, F. & Spitters, B., 1 Jan 2018, p. 137-150. 14 p.

  Research output: Contribution to conference › Paper › Research › peer-review
• 2017

  Modalities in homotopy type theory

  Rijke, E., Shulman, M. & Spitters, B., 27 Jun 2017

  Research output: Other contribution › Net publication - Internet publication › Research › peer-review

  Open Access

• The HoTT Library: A Formalization of Homotopy Type Theory in Coq

  Bauer, A., Gross, J., Lumsdaine, P. L., Shulman, M., Sozeau, M. & Spitters, B., 16 Jan 2017, CPP 2017 - Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, co-located with POPL 2017: CPP 2017. Bertot, Y. & Vafeiadis, V. (eds.). New York, NY, USA: Association for Computing Machinery, p. 164-172 9 p.

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  • Type Theory 100%
  • Homotopy Type 100%
  • Formalization 100%
  • Inductive Type 50%
  • Category Theory 25%
  37 Citations (Scopus)
• 2016

  Cubical sets and the topological topos

  Spitters, B., 17 Oct 2016

  Research output: Other contribution › Net publication - Internet publication › Research

  Open Access

  • Topos 100%
  • Type Theory 66%
  • Simplicial Set 66%
  • Morphism 33%
  • Model Set 33%

• Guarded cubical type theory

  Birkedal, L., Bizjak, A., Clouston, R., Grathwohl, H. B., Spitters, B. & Vezzosi, A., 2016. 2 p.

  Research output: Contribution to conference › Conference abstract for conference › Research

  Open Access

• Guarded Cubical Type Theory

  Birkedal, L., Bizjak, A., Clouston, R., Grathwohl, H. B., Spitters, B. & Vezzosi, A., 2016

  Research output: Other contribution › Net publication - Internet publication › Research › peer-review

  Open Access

  • Type Checking 100%
  • Extensionality 100%
  • Small Category 50%
  • Computer Science 50%
  • Logic Programming 50%
  16 Citations (Scopus)

• Guarded Cubical Type Theory: Path Equality for Guarded Recursion

  Birkedal, L., Bizjak, A., Clouston, R., Grathwohl, H. B., Spitters, B. & Vezzosi, A., 2016, CSL 2016: 25th EACSL Annual Conference on Computer Science Logic. Talbot, J.-M. & Regnier, L. (eds.). p. 1 - 17 17 p. (Leibniz International Proceedings in Informatics, Vol. 62).

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  Open Access

  File

  • Extensionality 100%
  168 Downloads (Pure)

• Homotopy type theory and the formalization of mathematics

  Rijke, E. & Spitters, B., 2016, In: Nieuw Archief voor Wiskunde . 5/17, 3, p. 159 - 164 6 p.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research

  Open Access

• The HoTT Library: A formalization of homotopy type theory in Coq

  Bauer, A., Gross, J., Lumsdaine, P. L., Shulman, M., Sozeau, M. & Spitters, B., 2016

  Research output: Other contribution › Net publication - Internet publication › Research

  Open Access
• 2015

  Cubical sets as a classifying topos

  Spitters, B., 2015. 2 p.

  Research output: Contribution to conference › Conference abstract for conference › Research

  Open Access

  File

  • Topos 100%
  • Type Theory 66%
  • Cube 33%
  • Model Set 33%
  • Inductive Type 33%
  203 Downloads (Pure)

• Sets in homotopy type theory

  Rijke, E. & Spitters, B., 30 Jun 2015, In: Mathematical Structures in Computer Science. 25, 5, p. 1172-1202 31 p.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  • Groupoid 100%
  • Type Theory 100%
  • Homotopy Type 100%
  • Topos 66%
  • Subobject 33%
  12 Citations (Scopus)
• 2014

  Gelfand spectra in Grothendieck toposes using geometric mathematics

  Spitters, B., Vickers, S. & Wolters, S., 1 Jan 2014, In: Electronic Proceedings in Theoretical Computer Science, EPTCS. 158, p. 77-107 31 p.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Conference article › Research › peer-review

  • Mathematics 100%
  • Grothendieck 100%
  • Topos 100%
  • C-Algebras 28%
  • Functor 14%
  3 Citations (Scopus)
• 2013

  The Picard algorithm for ordinary differential equations in Coq

  Makarov, E. & Spitters, B., 28 Aug 2013, Interactive Theorem Proving - 4th International Conference, ITP 2013, Proceedings. p. 463-468 6 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 7998 LNCS).

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  • Ordinary Differential Equation 100%
  • Mathematics 33%
  • Sufficient Condition 33%
  • Differential Equation 33%
  • Fundamental Theorem 33%
  24 Citations (Scopus)

• Type classes for efficient exact real arithmetic in CoQ

  Krebbers, R. & Spitters, B., 25 Feb 2013, In: Logical Methods in Computer Science. 9, 1

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  • Dyadic Rational 100%
  • Cosine Function 100%
  • Error Estimate 100%
  22 Citations (Scopus)
• 2012

  Bohrification of operator algebras and quantum logic

  Heunen, C., Landsman, N. P. & Spitters, B., 1 Jun 2012, In: Synthese. 186, 3, p. 719-752 34 p.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  • Lattices 100%
  • Operator Algebra 100%
  • Quantum Logic 100%
  • C-Algebras 50%
  • Subalgebra 50%
  21 Citations (Scopus)

• The Space of Measurement Outcomes as a Spectral Invariant for Non-Commutative Algebras

  Spitters, B., 1 Jul 2012, In: Foundations of Physics. 42, 7, p. 896-908 13 p.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  • C-Algebras 100%
  • Noncommutative Algebra 100%
  • Spectral Invariant 100%
  • Coincides 20%
  • Commutativity 20%
  6 Citations (Scopus)
• 2011

  Computer certified efficient exact reals in Coq

  Krebbers, R. & Spitters, B., 11 Aug 2011, Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011 and 10th International Conference, MKM 2011, Proceedings. p. 90-106 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 6824 LNAI).

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  • Approximates 100%
  • Integer 100%
  • Power Series 100%
  • Basic Operation 100%
  • Error Estimate 100%
  10 Citations (Scopus)