Bas Spitters
According to our database^{1},
Bas Spitters
authored at least 45 papers
between 2002 and 2020.
Collaborative distances:
Collaborative distances:
Timeline
Legend:
Book In proceedings Article PhD thesis OtherLinks
Homepages:

at zbmath.org

at orcid.org

at github.com

at cs.au.dk

at andrej.com
On csauthors.net:
Bibliography
2020
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
2019
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
2018
Computeraided 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
2017
The HoTT library: a formalization of homotopy type theory in Coq.
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017
2016
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
2015
Sets in homotopy type theory.
Math. Struct. Comput. Sci., 2015
2013
The Picard Algorithm for Ordinary Differential Equations in Coq.
Proceedings of the Interactive Theorem Proving  4th International Conference, 2013
2012
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
2011
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
2010
A computerverified monadic functional implementation of the integral.
Theor. Comput. Sci., 2010
Constructive Pointfree Topology Eliminates Nonconstructive 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 noncommutative 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
2009
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
2007
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
2006
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
2005
A constructive proof of the PeterWeyl 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 StoneYosida 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
2003
Program Extraction from Large Proof Developments.
Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003
2002
Located Operators.
Math. Log. Q., 2002