84 citations · 114 across the 3 of their papers we have counts for
3 papers
Agentic Proving for Program Verification
Alessandro Sosso, Akhil Arora, Bas Spitters
Agentic systems have recently emerged as state-of-the-art approaches for automated theorem proving in formal mathematics. To assess how far these capabilities extend to program ver…
ConCert: A Smart Contract Certification Framework in Coq
Danil Annenkov, Jakob Botsch Nielsen, Bas Spitters
We present a new way of embedding functional languages into the Coq proof assistant by using meta-programming. This allows us to develop the meta-theory of the language using the d…
A topos for algebraic quantum theory
Chris Heunen, Nicolaas P. Landsman, Bas Spitters
The aim of this paper is to relate algebraic quantum mechanics to topos theory, so as to construct new foundations for quantum logic and quantum spaces. Motivated by Bohr's idea th…