BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Bas Spitters

Bas Spitters appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
Logic in Computer Sciencemath.LOmath.CTProgramming Languagesquant-phmath.FAmath-phmath.MPmath.OACryptography and Securitymath.NANumerical Analysis

Catalog footprint

What is connected

22works
12topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

22 published item(s)

preprint2022arXiv

Formalising Decentralised Exchanges in Coq

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 contracts involved in Dexter's implementation. Moreover, our formalisation is the first to feature proofs of safety properties of the interacting smart contracts of a decentralized exchange. We have extracted our contract from Coq into CameLIGO code, so it can be deployed on the Tezos blockchain. Uniswap and Dexter are paradigmatic for a collection of similar contracts. Our methodology thus allows us to implement and verify DeFi applications featuring similar interaction patterns.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

Synthetic topology in Homotopy Type Theory for probabilistic programming

The ALEA Coq library formalizes measure theory based on a variant of the Giry monad on the category of sets. This enables the interpretation of a probabilistic programming language with primitives for sampling from discrete distributions. However, continuous distributions have to be discretized because the corresponding measures cannot be defined on all subsets of their carriers. This paper proposes the use of synthetic topology to model continuous distributions for probabilistic computations in type theory. We study the initial $σ$-frame and the corresponding induced topology on arbitrary sets. Based on these intrinsic topologies we define valuations and lower integrals on sets, and prove versions of the Riesz and Fubini theorems. We then show how the Lebesgue valuation, and hence continuous distributions, can be constructed.

0 citations0 reviewsNo code linkedOpen access
preprint2019arXiv

An Application of Computable Distributions to the Semantics of Probabilistic Programs

In this chapter, we explore how (Type-2) computable distributions can be used to give both (algorithmic) sampling and distributional semantics to probabilistic programs with continuous distributions. Towards this end, we sketch an encoding of computable distributions in a fragment of Haskell and show how topological domains can be used to model the resulting PCF-like language. We also examine the implications that a (Type-2) computable semantics has for implementing conditioning. We hope to draw out the connection between an approach based on (Type-2) computability and ordinary programming throughout the chapter as well as highlight the relation with constructive mathematics (via realizability).

0 citations0 reviewsNo code linkedOpen access
preprint2019arXiv

ConCert: A Smart Contract Certification Framework in Coq

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.

0 citations0 reviewsNo code linkedOpen access
preprint2019arXiv

Modal Dependent Type Theory and Dependent Right Adjoints

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 the syntax and semantics with universes.

0 citations0 reviewsNo code linkedOpen access
preprint2019arXiv

Smart Contract Interactions in Coq

We present a model/executable specification of smart contract execution in Coq. Our formalization allows for inter-contract communication and generalizes existing work by allowing modelling of both depth-first execution blockchains (like Ethereum) and breadth-first execution blockchains (like Tezos). We represent smart contracts programs in Coq's functional language Gallina, enabling easier reasoning about functional correctness of concrete contracts than other approaches. In particular we develop a Congress contract in this style. This contract -- a simplified version of the infamous DAO -- is interesting because of its very dynamic communication pattern with other contracts. We give a high-level partial specification of the Congress's behavior, related to reentrancy, and prove that the Congress satisfies it for all possible smart contract execution orders.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Cubical sets and the topological topos

Coquand's cubical set model for homotopy type theory provides the basis for a computational interpretation of the univalence axiom and some higher inductive types, as implemented in the cubical proof assistant. This paper contributes to the understanding of this model. We make three contributions: 1. Johnstone's topological topos was created to present the geometric realization of simplicial sets as a geometric morphism between toposes. Johnstone shows that simplicial sets classify strict linear orders with disjoint endpoints and that (classically) the unit interval is such an order. Here we show that it can also be a target for cubical realization by showing that Coquand's cubical sets classify the geometric theory of flat distributive lattices. As a side result, we obtain a simplicial realization of a cubical set. 2. Using the internal `interval' in the topos of cubical sets, we construct a Moore path model of identity types. 3. We construct a premodel structure internally in the cubical type theory and hence on the fibrant objects in cubical sets.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Guarded Cubical Type Theory: Path Equality for Guarded Recursion

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 recursive types. This further expands the foundations of CTT as a basis for formalisation in mathematics and computer science. We present examples to demonstrate the expressivity of our type theory, all of which have been checked using a prototype type-checker implementation, and present semantics in a presheaf category.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Gelfand spectra in Grothendieck toposes using geometric mathematics

In the (covariant) topos approach to quantum theory by Heunen, Landsman and Spitters, one associates to each unital C*-algebra, A, a topos T(A) of sheaves on a locale and a commutative C*-algebra, a, within that topos. The Gelfand spectrum of a is a locale S in this topos, which is equivalent to a bundle over the base locale. We further develop this external presentation of the locale S, by noting that the construction of the Gelfand spectrum in a general topos can be described using geometric logic. As a consequence, the spectrum, seen as a bundle, is computed fibrewise. As a by-product of the geometricity of Gelfand spectra, we find an explicit external description of the spectrum whenever the topos is a functor category. As an intermediate result we show that locally perfect maps compose, so that the externalization of a locally compact locale in a topos of sheaves over a locally compact locale is locally compact, too.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

A constructive proof of Simpson's Rule

For most purposes, one can replace the use of Rolle's theorem and the mean value theorem, which are not constructively valid, by the law of bounded change. The proof of two basic results in numerical analysis, the error term for Lagrange interpolation and Simpson's rule, however seem to require the full strength of the classical Rolle's Theorem. The goal of this note is to justify these two results constructively, using ideas going back to Ampère and Genocchi.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Proceedings 8th International Workshop on Quantum Physics and Logic

This volume contains the proceedings of the 8th International Workshop on Quantum Physics and Logic (QPL 2011), which was held October 27-29, 2011 at Radboud University Nijmegen. The goal of this workshop series is to bring together researchers working on mathematical foundations of quantum physics, quantum computing and spatio-temporal causal structures, and in particular those that use logical tools, ordered algebraic and category-theoretic structures, formal languages, semantic methods and other computer science methods for the study of physical behavior in general. Over the past few years, there has been growing activity in these foundational approaches, together with a renewed interest in the foundations of quantum theory, which complement the more mainstream research in quantum computation.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Computer certified efficient exact reals in Coq

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. We provide an implementation of the exact real numbers in the Coq proof assistant. This improves on the earlier Coq-implementation by O'Connor in two ways: we use dyadic rationals built from the machine integers and we optimize computation of power series by using approximate division. Moreover, we use type classes for clean mathematical interfaces. This appears to be the first time that type classes are used in heavy computation. We obtain over a 100 times speed up of the basic operations and indications for improving the Coq system.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Type Classes for Mathematics in Type Theory

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 expressed using categorical language and universal algebra constructions. Strategic use of type classes lets us support these high-level theory-friendly definitions while still enabling efficient implementations unhindered by gratuitous indirection, conversion or projection. Algebra thrives on the interplay between syntax and semantics. The Prolog-like abilities of type class instance resolution allow us to conveniently define a quote function, thus facilitating the use of reflective techniques.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

Bohrification

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 many projections (e.g. when A is a von Neumann algebra, or, more generally, a Rickart C*-algebra), the intuitionistic quantum logic S(A) of A may also be compared with the traditional quantum logic, i.e. the orthomodular lattice of projections in A. This time, the main difference is that the former is distributive (even when A is noncommutative), while the latter is not. This chapter is a streamlined synthesis of 0709.4364, 0902.3201, 0905.2275.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

Bohrification of operator algebras and quantum logic

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 in a natural way, so that the associated propositional logic is intuitionistic: distributivity is recovered at the expense of the law of the excluded middle. Subsequently, generalizing an earlier computation for n-by-n matrices, we prove that the Heyting algebra thus associated to A arises as a basis for the internal Gelfand spectrum (in the sense of Banaschewski-Mulvey) of the "Bohrification" of A, which is a commutative Rickart C*-algebra in the topos of functors from C(A) to the category of sets. We explain the relationship of this construction to partial Boolean algebras and Bruns-Lakser completions. Finally, we establish a connection between probability measure on the lattice of projections on a Hilbert space H and probability valuations on the internal Gelfand spectrum of A for A = B(H).

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

Constructive Theory of Banach algebras

We present a way to organize a constructive development of the theory of Banach algebras, inspired by works of Cohen, de Bruijn and Bishop. We illustrate this by giving elementary proofs of Wiener's result on the inverse of Fourier series and Wiener's Tauberian Theorem, in a sequel to this paper we show how this can be used in a localic, or point-free, description of the spectrum of a Banach algebra.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

The Gelfand spectrum of a noncommutative C*-algebra: a topos-theoretic approach

We compare two influential ways of defining a generalized notion of space. The first, inspired by Gelfand duality, states that the category of 'noncommutative spaces' is the opposite of the category of C*-algebras. The second, loosely generalizing Stone duality, maintains that the category of 'pointfree spaces' is the opposite of the category of frames (i.e., complete lattices in which the meet distributes over arbitrary joins). One possible relationship between these two notions of space was unearthed by Banaschewski and Mulvey, who proved a constructive version of Gelfand duality in which the Gelfand spectrum of a commutative C*-algebra comes out as a pointfree space. Being constructive, this result applies in arbitrary toposes (with natural numbers objects, so that internal C*-algebras can be defined). Earlier work by the first three authors, shows how a noncommutative C*-algebra gives rise to a commutative one internal to a certain sheaf topos. The latter, then, has a constructive Gelfand spectrum, also internal to the topos in question. After a brief review of this work, we compute the so-called external description of this internal spectrum, which in principle is a fibered pointfree space in the familiar topos Sets of sets and functions. However, we obtain the external spectrum as a fibered topological space in the usual sense. This leads to an explicit Gelfand transform, as well as to a topological reinterpretation of the Kochen-Specker Theorem of quantum mechanics, which supplements the remarkable topos-theoretic version of this theorem due to Butterfield and Isham.

0 citations0 reviewsNo code linkedOpen access
preprint2008arXiv

Constructive pointfree topology eliminates non-constructive representation theorems from Riesz space theory

In Riesz space theory it is good practice to avoid representation theorems which depend on the axiom of choice. Here we present a general methodology to do this using pointfree topology. To illustrate the technique we show that almost f-algebras are commutative. The proof is obtained relatively straightforward from the proof by Buskes and van Rooij by using the pointfree Stone-Yosida representation theorem by Coquand and Spitters.

0 citations0 reviewsNo code linkedOpen access