arXiv subjects
Publications and source records attributed to Thierry Coquand.
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.
We present a constructive proof of Gelfand duality for C*-algebras by reducing the problem to Gelfand duality for real C*-algebras.
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.
Ulrich Berger presented a powerful proof of strong normalisation using domains, in particular it simplifies significantly Tait's proof of strong normalisation of Spector's bar recursion. The main contribution of this paper is to show that, using ideas from intersection types and Martin-Lof's domain interpretation of type theory one can in turn simplify further U. Berger's argument. We build a domain model for an untyped programming language where U. Berger has an interpretation only for typed terms or alternatively has an interpretation for untyped terms but need an extra condition to deduce strong normalisation. As a main application, we show that Martin-Löf dependent type theory extended with a program for Spector double negation shift.