Aarhus University Seal / Aarhus Universitets segl

Bas Spitters

  1. 2018
  2. Published

    Computer-Aided Proofs for Multiparty Computation with Active Security. / Haagh, H.; Karbyshev, A.; Oechsner, S.; Spitters, B.; Strub, P.

    2018 IEEE 31st Computer Security Foundations Symposium (CSF). Vol. 2018 Oxford : IEEE, 2018. p. 119-131.

    Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

  3. Published

    Guarded Cubical Type Theory. / Birkedal, Lars; Bizjak, Aleš; Clouston, Ranald; Grathwohl, Hans Bugge; Spitters, Bas; Vezzosi, Andrea.

    In: Journal of Automated Reasoning, No. Special Issue on Homotopy Type Theory and Univalent Foundations, 26.06.2018, p. 1-43.

    Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

  4. Published

    An Application of Computable Distributions to the Semantics of Probabilistic Programs. / Huang, Daniel; Morrisett, Greg; Spitters, Bas.

    46 p. Cornell University. 2018, .

    Research output: Other contributionNet publication - Internet publicationResearch

  5. Published

    Computer-aided proofs for multiparty computation with active security. / Haagh, Helene; Karbyshev, Aleksandr; Oechsner, Sabine; Spitters, Bas; Strub, Pierre-Yves.

    13 p. arXiv.org. 2018, .

    Research output: Other contributionNet publication - Internet publicationResearchpeer-review

  6. Published

    Internal Universes in Models of Homotopy Type Theory. / Licata, Daniel R.; Orton, Ian; Pitts, Andrew M.; Spitters, Bas.

    17 p. arXiv.org. 2018, .

    Research output: Other contributionNet publication - Internet publicationResearch

  7. Published

    Preuves constructives de programmes probabilistes. / Faissole, Florian; Spitters, Bas.

    Journées Francophones des Langages Applicatifs. 2018.

    Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

  8. 2017
  9. Published

    Modalities in homotopy type theory. / Rijke, Egbert; Shulman, Michael; Spitters, Bas.

    2017, Internetarkiv.

    Research output: Other contributionNet publication - Internet publicationResearch

  10. Published

    The HoTT Library: A Formalization of Homotopy Type Theory in Coq. / Bauer, Andrej; Gross, Jason; Lumsdaine, Peter LeFanu; Shulman, Michael; Sozeau, Matthieu; Spitters, Bas.

    CPP 2017 - Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, co-located with POPL 2017: CPP 2017. ed. / Yves Bertot; Viktor Vafeiadis. New York, NY, USA : Association for Computing Machinery, 2017. p. 164-172.

    Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

  11. 2016
  12. Published

    Cubical sets and the topological topos. / Spitters, Bas.

    2016, Internetarkiv.

    Research output: Other contributionNet publication - Internet publicationResearch

  13. Published

    Guarded Cubical Type Theory. / Birkedal, Lars; Bizjak, Aleš; Clouston, Ranald; Grathwohl, Hans Bugge; Spitters, Bas; Vezzosi, Andrea.

    2016, Internetatikel.

    Research output: Other contributionNet publication - Internet publicationResearchpeer-review

  14. Published

    Guarded Cubical Type Theory : Path Equality for Guarded Recursion. / Birkedal, Lars; Bizjak, Aleš; Clouston, Ranald; Grathwohl, Hans Bugge; Spitters, Bas; Vezzosi, Andrea.

    CSL 2016: 25th EACSL Annual Conference on Computer Science Logic. ed. / Jean-Marc Talbot; Laurent Regnier. 2016. p. 1 - 17.

    Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

  15. Published

    Guarded cubical type theory. / Birkedal, Lars; Bizjak, Aleš; Clouston, Ranald; Grathwohl, Hans Bugge; Spitters, Bas; Vezzosi, Andrea.

    2016. Abstract from 22nd International Conference on Types for Proofs and Programs, Novi Sad, Serbia.

    Research output: Contribution to conferenceConference abstract for conferenceResearch

  16. Published

    Homotopy type theory and the formalization of mathematics. / Rijke, Egbert; Spitters, Bas.

    In: Nieuw Archief voor Wiskunde , Vol. 5/17, No. 3, 2016, p. 159 - 164.

    Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearch

  17. Published

    The HoTT Library : A formalization of homotopy type theory in Coq. / Bauer, Andrej; Gross, Jason; Lumsdaine, Peter LeFanu; Shulman, Michael; Sozeau, Matthieu; Spitters, Bas.

    2016, Internetartikel.

    Research output: Other contributionNet publication - Internet publicationResearch

  18. 2015
  19. Published

    Sets in homotopy type theory. / Rijke, Egbert; Spitters, Bas.

    In: Mathematical Structures in Computer Science, Vol. 25, No. 5, 30.06.2015, p. 1172-1202.

    Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

  20. Published

    Cubical sets as a classifying topos. / Spitters, Bas.

    2015. Abstract from 21st International Conference on Types for Proofs and Programs, , Tallinn, Estonia.

    Research output: Contribution to conferenceConference abstract for conferenceResearch

  21. 2014
  22. Published

    Gelfand spectra in Grothendieck toposes using geometric mathematics. / Spitters, Bas; Vickers, Steven; Wolters, Sander.

    In: Electronic Proceedings in Theoretical Computer Science, EPTCS, Vol. 158, 01.01.2014, p. 77-107.

    Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperConference articleResearchpeer-review

  23. 2013
  24. Published

    The Picard algorithm for ordinary differential equations in Coq. / Makarov, Evgeny; Spitters, Bas.

    Interactive Theorem Proving - 4th International Conference, ITP 2013, Proceedings. 2013. p. 463-468.

    Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

  25. Published

    Type classes for efficient exact real arithmetic in CoQ. / Krebbers, Robbert; Spitters, Bas.

    In: Logical Methods in Computer Science, Vol. 9, No. 1, 25.02.2013.

    Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

  26. 2012
  27. Published

    The Space of Measurement Outcomes as a Spectral Invariant for Non-Commutative Algebras. / Spitters, Bas.

    In: Foundations of Physics, Vol. 42, No. 7, 01.07.2012, p. 896-908.

    Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

  28. Published

    Bohrification of operator algebras and quantum logic. / Heunen, Chris; Landsman, Nicolaas P.; Spitters, Bas.

    In: Synthese, Vol. 186, No. 3, 01.06.2012, p. 719-752.

    Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

  29. 2011
  30. Published

    Computer certified efficient exact reals in Coq. / Krebbers, Robbert; Spitters, Bas.

    Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011 and 10th International Conference, MKM 2011, Proceedings. 2011. p. 90-106.

    Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review