Bas Spitters

According to our database1, Bas Spitters authored at least 45 papers between 2002 and 2020.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.



In proceedings 
PhD thesis 





Modal dependent type theory and dependent right adjoints.
Math. Struct. Comput. Sci., 2020

ConCert: a smart contract certification framework in Coq.
Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

Modalities in homotopy type theory.
Logical Methods in Computer Science, 2019

Guarded Cubical Type Theory.
J. Autom. Reasoning, 2019

Synthetic topology in Homotopy Type Theory for probabilistic programming.
CoRR, 2019

Smart Contract Interactions in Coq.
CoRR, 2019

Towards a Smart Contract Verification Framework in Coq.
CoRR, 2019

Computer-aided proofs for multiparty computation with active security.
IACR Cryptol. ePrint Arch., 2018

Normalization by gluing for free λ-theories.
CoRR, 2018

An Application of Computable Distributions to the Semantics of Probabilistic Programs.
CoRR, 2018

Modal Dependent Type Theory and Dependent Right Adjoints.
CoRR, 2018

Internal Universes in Models of Homotopy Type Theory.
Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, 2018

The HoTT library: a formalization of homotopy type theory in Coq.
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

Cubical sets and the topological topos.
CoRR, 2016

Guarded Cubical Type Theory: Path Equality for Guarded Recursion.
Proceedings of the 25th EACSL Annual Conference on Computer Science Logic, 2016

Sets in homotopy type theory.
Math. Struct. Comput. Sci., 2015

The Picard Algorithm for Ordinary Differential Equations in Coq.
Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

Bohrification of operator algebras and quantum logic.
Synthese, 2012

A constructive proof of Simpson's Rule.
J. Log. Anal., 2012

Gelfand spectra in Grothendieck toposes using geometric mathematics.
Proceedings of the Proceedings 9th Workshop on Quantum Physics and Logic, 2012

Type classes for mathematics in type theory.
Math. Struct. Comput. Sci., 2011

Metric complements of overt closed sets.
Math. Log. Q., 2011

Type classes for efficient exact real arithmetic in Coq
Logical Methods in Computer Science, 2011

Computer Certified Efficient Exact Reals in Coq.
Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

A computer-verified monadic functional implementation of the integral.
Theor. Comput. Sci., 2010

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

Constructive theory of Banach algebras.
J. Log. Anal., 2010

The space of measurement outcomes as a spectrum for non-commutative algebras
Proceedings of the Proceedings Sixth Workshop on Developments in Computational Models: Causality, 2010

Locatedness and overt sublocales.
Ann. Pure Appl. Log., 2010

Developing the Algebraic Hierarchy with Type Classes in Coq.
Proceedings of the Interactive Theorem Proving, First International Conference, 2010

Integrals and valuations.
J. Log. Anal., 2009

Computer Verified Exact Analysis (Tutorial).
Proceedings of the Sixth International Conference on Computability and Complexity in Analysis, 2009

Preface to the special issue: Constructive analysis, types and exact real numbers.
Math. Struct. Comput. Sci., 2007

Constructive analysis, types and exact real numbers.
Math. Struct. Comput. Sci., 2007

Corrigendum to: 'A constructive view on ergodic theorems'.
J. Symb. Log., 2006

A constructive view on ergodic theorems.
J. Symb. Log., 2006

Constructive algebraic integration theory.
Ann. Pure Appl. Log., 2006

A constructive proof of the Peter-Weyl theorem.
Math. Log. Q., 2005

Almost periodic functions, constructively.
Logical Methods in Computer Science, 2005

Constructive Results on Operator Algebras.
J. UCS, 2005

Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems.
J. UCS, 2005

Constructive algebraic integration theory without choice.
Proceedings of the Mathematics, Algorithms, Proofs, 9.-14. January 2005, 2005

Approximating integrable sets by compacts constructively.
Proceedings of the From sets and types to topology and analysis, 2005

Program Extraction from Large Proof Developments.
Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003

Located Operators.
Math. Log. Q., 2002