arXiv.itsnick.co

an independent field guide to 23 million papers from arXiv & OpenAlex — not affiliated with arXiv.org

Author

Bas Spitters

80 papers · 2002–2026

2002: 22003: 02004: 02005: 62006: 22007: 42008: 62009: 52010: 32011: 72012: 22013: 52014: 22015: 02016: 92017: 12018: 52019: 32020: 42021: 32022: 22023: 32024: 22025: 22026: 2
2002peak 9 in 20162026

Frequent co-authors

Papers

showing 1–25 of 80 RSS

Type Classes for Mathematics in Type Theory

Bas Spitters, Eelis van der Weegen

cs.LO · · cited 110× · arXiv ↗ · more like this ·

The introduction of first-class type classes in the Coq system calls for re-examination of the basic interfaces used for mathematical formalization in type theory. We present a new set of type classes for mathematics and take full advantage of their unique features to make practical a particularly flexible approach formerly thought infeasible. Thus, we address both traditional proof engineering challenges as well as new ones resulting from our ambition to build upon this development a library of constructive analysis in which abstraction penalties inhibiting efficient computation are reduced to a minimum. The base of our development consists of type classes representing a standard algebraic hierarchy, as well as portions of category theory and universal algebra. On this foundation we build a set of mathematically sound abstract interfaces for different kinds of numbers, succinctly…

Modalities in homotopy type theory

Egbert Rijke, Michael Shulman, Bas Spitters

math.CT · · cited 109× · arXiv ↗ · more like this ·

Univalent homotopy type theory (HoTT) may be seen as a language for the category of $\infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal language for (elementary) higher toposes. We develop the theory of factorization systems, reflective subuniverses, and modalities in homotopy type theory, including their construction using a "localization" higher inductive type. This produces in particular the ($n$-connected, $n$-truncated) factorization system as well as internal presentations of subtoposes, through lex modalities. We also develop the semantics of these constructions.

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

Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine +3 more

cs.LO · · cited 87× · arXiv ↗ · more like this ·

We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, higher inductive types, and significant amounts of synthetic homotopy theory, as well as category theory and modalities. The library has been used as a basis for several independent developments. We discuss the decisions that led to the design of the library, and we comment on the interaction of homotopy type theory with recently introduced features of Coq, such as universe polymorphism and private inductive types.

Internal Universes in Models of Homotopy Type Theory

Daniel R. Licata, Ian Orton, Andrew M. Pitts +1 more

cs.LO · · cited 73× · arXiv ↗ · more like this ·

We begin by recalling the essentially global character of universes in various models of homotopy type theory, which prevents a straightforward axiomatization of their properties using the internal language of the presheaf toposes from which these model are constructed. We get around this problem by extending the internal language with a modal operator for expressing properties of global elements. In this setting we show how to construct a universe that classifies the Cohen-Coquand-Huber-Mörtberg (CCHM) notion of fibration from their cubical sets model, starting from the assumption that the interval is tiny - a property that the interval in cubical sets does indeed have. This leads to an elementary axiomatization of that and related models of homotopy type theory within what we call crisp type theory.

Modal Dependent Type Theory and Dependent Right Adjoints

Lars Birkedal, Ranald Clouston, Bassel Mannaa +3 more

cs.LO · · cited 63× · arXiv ↗ · more like this ·

In recent years we have seen several new models of dependent type theory extended with some form of modal necessity operator, including nominal type theory, guarded and clocked type theory, and spatial and cohesive type theory. In this paper we study modal dependent type theory: dependent type theory with an operator satisfying (a dependent version of) the K-axiom of modal logic. We investigate both semantics and syntax. For the semantics, we introduce categories with families with a dependent right adjoint (CwDRA) and show that the examples above can be presented as such. Indeed, we show that any finite limit category with an adjunction of endofunctors gives rise to a CwDRA via the local universe construction. For the syntax, we introduce a dependently typed extension of Fitch-style modal lambda-calculus, show that it can be interpreted in any CwDRA, and build a term model. We extend…

Bohrification of operator algebras and quantum logic

Chris Heunen, Nicolaas P. Landsman, Bas Spitters

quant-ph · · cited 57× · arXiv ↗ · more like this ·

Following Birkhoff and von Neumann, quantum logic has traditionally been based on the lattice of closed linear subspaces of some Hilbert space, or, more generally, on the lattice of projections in a von Neumann algebra A. Unfortunately, the logical interpretation of these lattices is impaired by their nondistributivity and by various other problems. We show that a possible resolution of these difficulties, suggested by the ideas of Bohr, emerges if instead of single projections one considers elementary propositions to be families of projections indexed by a partially ordered set C(A) of appropriate commutative subalgebras of A. In fact, to achieve both maximal generality and ease of use within topos theory, we assume that A is a so-called Rickart C*-algebra and that C(A) consists of all unital commutative Rickart C*-subalgebras of A. Such families of projections form a Heyting algebra…

Integrals and Valuations

Thierry Coquand, Bas Spitters

math.LO · · cited 53× · arXiv ↗ · more like this ·

We construct a homeomorphism between the compact regular locale of integrals on a Riesz space and the locale of (valuations) on its spectrum. In fact, we construct two geometric theories and show that they are biinterpretable. The constructions are elementary and tightly connected to the Riesz space structure.

Type classes for efficient exact real arithmetic in Coq

Robbert Krebbers, Bas Spitters

cs.LO · · cited 46× · arXiv ↗ · more like this ·

Floating point operations are fast, but require continuous effort on the part of the user in order to ensure that the results are correct. This burden can be shifted away from the user by providing a library of exact analysis in which the computer handles the error estimates. Previously, we [Krebbers/Spitters 2011] provided a fast implementation of the exact real numbers in the Coq proof assistant. Our implementation improved on an earlier implementation by O'Connor by using type classes to describe an abstract specification of the underlying dense set from which the real numbers are built. In particular, we used dyadic rationals built from Coq's machine integers to obtain a 100 times speed up of the basic operations already. This article is a substantially expanded version of [Krebbers/Spitters 2011] in which the implementation is extended in the various ways. First, we implement and…

Guarded Cubical Type Theory: Path Equality for Guarded Recursion

Lars Birkedal, Aleš Bizjak, Ranald Clouston +3 more

cs.LO · · cited 39× · arXiv ↗ · more like this ·

This paper improves the treatment of equality in guarded dependent type theory (GDTT), by combining it with cubical type theory (CTT). GDTT is an extensional type theory with guarded recursive types, which are useful for building models of program logics, and for programming and reasoning with coinductive types. We wish to implement GDTT with decidable type-checking, while still supporting non-trivial equality proofs that reason about the extensions of guarded recursive constructions. CTT is a variation of Martin-Löf type theory in which the identity type is replaced by abstract paths between terms. CTT provides a computational interpretation of functional extensionality, is conjectured to have decidable type checking, and has an implemented type-checker. Our new type theory, called guarded cubical type theory, provides a computational interpretation of extensionality for guarded…

Formal topology and constructive mathematics: the Gelfand and Stone-Yosida representation theorems

Thierry Coquand, Bas Spitters

math.FA · · cited 32× · arXiv ↗ · more like this ·

We present a constructive proof of the Stone-Yosida representation theorem for Riesz spaces motivated by considerations from formal topology. This theorem is used to derive a representation theorem for f-algebras. In turn, this theorem implies the Gelfand representation theorem for C*-algebras of operators on Hilbert spaces as formulated by Bishop and Bridges. Our proof is shorter, clearer, and we avoid the use of approximate eigenvalues.

Computer-aided proofs for multiparty computation with active security

Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner +2 more

cs.LO · · cited 31× · arXiv ↗ · more like this ·

Secure multi-party computation (MPC) is a general cryptographic technique that allows distrusting parties to compute a function of their individual inputs, while only revealing the output of the function. It has found applications in areas such as auctioning, email filtering, and secure teleconference. Given its importance, it is crucial that the protocols are specified and implemented correctly. In the programming language community it has become good practice to use computer proof assistants to verify correctness proofs. In the field of cryptography, EasyCrypt is the state of the art proof assistant. It provides an embedded language for probabilistic programming, together with a specialized logic, embedded into an ambient general purpose higher-order logic. It allows us to conveniently express cryptographic properties. EasyCrypt has been used successfully on many applications…

Constructive analysis, types and exact real numbers

Herman Geuvers, Milad Niqui, Bas Spitters +1 more

Artificial Intelligence · Mathematical Structures in Computer Science · · cited 28× · DOI ↗ · more like this ·

In this paper we will discuss various aspects of computable/constructive analysis, namely semantics, proofs and computations. We will present some of the problems and solutions of exact real arithmetic varying from concrete implementations, representation and algorithms to various models for real computation. We then put these models in a uniform framework using realisability, which opens the door to the use of type theoretic and coalgebraic constructions both in computing and reasoning about these computations. We will indicate that it is often natural to use constructive logic to reason about these computations.

Sets in homotopy type theory

Egbert Rijke, Bas Spitters

math.CT · · cited 27× · arXiv ↗ · more like this ·

Homotopy Type Theory may be seen as an internal language for the $\infty$-category of weak $\infty$-groupoids which in particular models the univalence axiom. Voevodsky proposes this language for weak $\infty$-groupoids as a new foundation for mathematics called the Univalent Foundations of Mathematics. It includes the sets as weak $\infty$-groupoids with contractible connected components, and thereby it includes (much of) the traditional set theoretical foundations as a special case. We thus wonder whether those `discrete' groupoids do in fact form a (predicative) topos. More generally, homotopy type theory is conjectured to be the internal language of `elementary' $\infty$-toposes. We prove that sets in homotopy type theory form a $ΠW$-pretopos. This is similar to the fact that the $0$-truncation of an $\infty$-topos is a topos. We show that both a subobject classifier and a…

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq

Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas +5 more

Artificial Intelligence · VUBIR (Vrije Universiteit Brussel) · · cited 22× · DOI ↗ · more like this ·

State-separating proofs (SSP) is a recent methodology for structuring game-based cryptographic proofs in a modular way. While very promising, this methodology was previously not fully formalized and came with little tool support. We address this by introducing SSProve, the first general verification framework for machine-checked state-separating proofs. SSProve combines high-level modular proofs about composed protocols, as proposed in SSP, with a probabilistic relational program logic for formalizing the lower-level details, which together enable constructing fully machine-checked crypto proofs in the Coq proof assistant. Moreover, SSProve is itself formalized in Coq, including the algebraic laws of SSP, the soundness of the program logic, and the connection between these two verification styles.

ConCert: A Smart Contract Certification Framework in Coq

Danil Annenkov, Jakob Botsch Nielsen, Bas Spitters

cs.PL · · cited 20× · arXiv ↗ · more like this ·

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 deep embedding and provides a convenient way for reasoning about concrete programs using the shallow embedding. We connect the deep and the shallow embeddings by a soundness theorem. As an instance of our approach, we develop an embedding of a core smart contract language into Coq and verify several important properties of a crowdfunding contract based on a previous formalisation of smart contract execution in blockchains.

Bohrification

Chris Heunen, Nicolaas P. Landsman, Bas Spitters

quant-ph · · cited 20× · arXiv ↗ · more like this ·

New foundations for quantum logic and quantum spaces are constructed by merging algebraic quantum theory and topos theory. Interpreting Bohr's "doctrine of classical concepts" mathematically, given a quantum theory described by a noncommutative C*-algebra A, we construct a topos T(A), which contains the "Bohrification" B of A as an internal commutative C*-algebra. Then B has a spectrum, a locale internal to T(A), the external description S(A) of which we interpret as the "Bohrified" phase space of the physical system. As in classical physics, the open subsets of S(A) correspond to (atomic) propositions, so that the "Bohrified" quantum logic of A is given by the Heyting algebra structure of S(A). The key difference between this logic and its classical counterpart is that the former does not satisfy the law of the excluded middle, and hence is intuitionistic. When A contains sufficiently…

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq

Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder +6 more

Artificial Intelligence · ACM Transactions on Programming Languages and Systems · · cited 14× · DOI ↗ · more like this ·

State-separating proofs (SSP) is a recent methodology for structuring game-based cryptographic proofs in a modular way, by using algebraic laws to exploit the modular structure of composed protocols. While promising, this methodology was previously not fully formalized and came with little tool support. We address this by introducing SSProve, the first general verification framework for machine-checked state-separating proofs. SSProve combines high-level modular proofs about composed protocols, as proposed in SSP, with a probabilistic relational program logic for formalizing the lower-level details, which together enable constructing machine-checked cryptographic proofs in the Coq proof assistant. Moreover, SSProve is itself fully formalized in Coq, including the algebraic laws of SSP, the soundness of the program logic, and the connection between these two verification styles. To…

A topos for algebraic quantum theory

Chris Heunen, Nicolaas P. Landsman, Bas Spitters

quant-ph · · cited 13× · arXiv ↗ · more like this ·

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 that the empirical content of quantum physics is accessible only through classical physics, we show how a C*-algebra of observables A induces a topos T(A) in which the amalgamation of all of its commutative subalgebras comprises a single commutative C*-algebra. According to the constructive Gelfand duality theorem of Banaschewski and Mulvey, the latter has an internal spectrum S(A) in T(A), which in our approach plays the role of a quantum phase space of the system. Thus we associate a locale (which is the topos-theoretical notion of a space and which intrinsically carries the intuitionistic logical structure of a Heyting algebra) to a C*-algebra (which is the noncommutative notion of a space). In this setting…

Constructive Results on Operator Algebras

Bas Spitters

Mathematical Physics · TU/e Research Portal · · cited 11× · DOI ↗ · more like this ·

Abstract: We present a to following results in the constructive theory of operator algebras. A representation theorem for finite dimensional von Neumann-algebras. A representation theorem for normal functionals. The spectral measure is independent of the choice of the basis of the underlying Hilbert space. Finally, the double commutant theorem for finite von Neumann algebras and for Abelian von Neumann algebras.

Extracting Smart Contracts Tested and Verified in Coq

Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen +1 more

cs.PL · · cited 9× · arXiv ↗ · more like this ·

We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. As part of this, we implement an optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value operational semantics of functional languages. We apply this to two functional smart contract languages, Liquidity and Midlang, and to the functional language Elm. Our development is done in the context of the ConCert framework that enables smart contract verification. We contribute a verified boardroom voting smart contract featuring maximum voter privacy such that each vote is kept private except under collusion of all other parties. We also integrate property-based testing into ConCert using QuickChick and our development is the first to support testing properties of interacting smart contracts. We test several complex contracts such as a DAO-like…

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

Bas Spitters

Mathematical Physics · Foundations of Physics · · cited 9× · DOI ↗ · more like this ·

The recently developed technique of Bohrification associates to a (unital) C*-algebra A We propose this locale, the ‘state space’, as a (n intuitionistic) logic of the physical system whose observable algebra is A. We compute a site which externally captures this locale and find that externally its points may be identified with partial measurement outcomes. This prompts us to compare Scott-continuity on the poset of contexts and continuity with respect to the C*-algebra as two ways to mathematically identify measurement outcomes with the same physical interpretation. Finally, we consider the not-not-sheafification of the Kripke model on classical contexts and obtain a space of measurement outcomes which for commutative C*-algebras coincides with the spectrum. The construction is functorial on the category of C*-algebras with commutativity reflecting maps.

Faster Constant-time Evaluation of the Kronecker Symbol with Application to Elliptic Curve Hashing

Diego F. Aranha, Benjamin Salling Hvass, Bas Spitters +1 more

Information Systems · · cited 8× · DOI ↗ · more like this ·

We generalize the Bernstein-Yang (BY) algorithm [11] for constant-time modular inversion to compute the Kronecker symbol, of which the Jacobi and Legendre symbols are special cases. We first develop a basic and easy-to-implement algorithm, defined with full-precision division steps. We then describe an optimized version due to Hamburg [21] over word-sized inputs, and formally verify its correctness. Along the way, we introduce a number of optimizations for implementing both versions in constant time. The resulting algorithms are particularly suitable for computing the Legendre symbol with dense prime p, where no efficient addition chain is known for exponentiating to p-1 over 2, as it is often the case in pairing-friendly elliptic curves. Our high-speed implementation for a range of parameters shows that the new algorithm is up to 40 times faster than exponentiation, and up to 25.7%…

Formalising Decentralised Exchanges in Coq

Eske Hoy Nielsen, Danil Annenkov, Bas Spitters

cs.LO · · cited 8× · arXiv ↗ · more like this ·

The number of attacks and accidents leading to significant losses of crypto-assets is growing. According to Chainalysis, in 2021, approx. $14 billion has been lost due to various incidents, and this number is dominated by Decentralized Finance (DeFi) applications. In order to address these issues, one can use a collection of tools ranging from auditing to formal methods. We use formal verification and provide the first formalisation of a DeFi contract in a foundational proof assistant capturing contract interactions. We focus on Dexter2, a decentralized, non-custodial exchange for the Tezos network similar to Uniswap on Ethereum. The Dexter implementation consists of several smart contracts. This poses unique challenges for formalisation due to the complex contract interactions. Our formalisation includes proofs of functional correctness with respect to an informal specification for the…

Constructive algebraic integration theory without choice

Bas Spitters

Mathematical Physics · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · · cited 8× · DOI ↗ · more like this ·

We present a constructive algebraic integration theory. The theory is constructive in the sense of Bishop, however we avoid the axiom of countable, or dependent, choice. Thus our results can be interpreted in any topos. Since we avoid impredicative methods the results may also be interpreted in Martin-Löf type theory or in a predicative topos in the sense of Moerdijk and Palmgren. We outline how to develop most of Bishop's theorems on integration theory that do not mention points explicitly. Coquand's constructive version of the Stone representation theorem is an important tool in this process. It is also used to give a new proof of Bishop's spectral theorem.