- The HoTT library in Coq at Big Proof
- Synthetic topology in Homotopy Type Theory for probabilistic programming at Big Proof
- Three lectures at POPL related conferences (CPP,PPS,CoqPL).

- Guarded cubical type theory (14 Dec, Nantes)
- Sets in homotopy type theory (18-23 July, FOMUS - Foundations of Mathematics: Univalent foundations and set theory) PDF
- Guarded cubical type theory (8-13 May, Mathematics for computation) PDF
- Cubical sets as a classifying topos (10-14 Feb, Workshop on Homotopy Type Theory) PDF
- Cubical sets as a classifying topos (11-15Jan, Effective Analysis: Foundations, Implementations, Certification) PDF
- Cubical sets as a classifying topos (9-10 Jan, PSSL98 Doorn) PDF

- Cubical sets as a classifying topos (24-25Sept, Homotopy Type Theory and Univalent Foundations - Mini-Symposium at DMV 2015) PDF
- Cubical sets as a classifying topos (8-10 June, 5WFTop) PDF
- Cubical sets as a classifying topos (3- 7 June, AIM)
- Formalizing mathematics in the univalent foundations. (May 24, ITU Copenhagen)
- Cubical sets as a classifying topos (19 May, TYPES) PDF

- Formalizing mathematics in the univalent foundations (Aarhus Nov 25th, slides)
- Domains XI (9 Sept, slides)
- MAP14 (May 30th, slides)
- VALS Seminar, (May 23th, slides)

- Computable Analysis and Rigorous Numerics (invited lecture, Dec 9th, slides)
- Type Theory, Homotopy Theory and Univalent Foundations (slides)
- Coq workshop (Invited lecture, slides.)
- Recent progress in homotopy type theory (General mathematics colloquium Nijmegen, June 19th)
- Cauchy reals in the univalent foundations (Brouwer seminar May 14th)
- Higher inductive types (Brouwer seminar May 7th)
- Quantum theory and topos theory. Institute for Advanced Study Feb 1st.

- Gelfand spectra in Grothendieck toposes, geometrically (Quantum Toposophy/, 14 dec) (slides).
- In homotopy type theory, do hsets form a predicative topos?, with Egbert Rijke (Brouwer seminar, 29 nov)
- The spectrum of the Bohrification is locally compact; an exercise in geometric reasoning. (Extended abstract) (QPL-12)
- Several lectures in the Seminar on simplicial methods
- Fourth Workshop on Formal Topology invited lecture (slides)

- MAP Spring school (slides)

- categorification and foundations of mathematics and quantum theory, 12 December, Stockholm (invited lecture)
- formath review, Brussell, 17-18 October
- Logic Colloquium, special session on Proof Theory and Constructive Mathematics, 11-16 July 2011, invited lecture slidesabs
- MLNL, 19-20 May, invited lecture
- formathBusiness meeting, Paris, 13 April
- Type classes for mathematics with Robbert Krebbers and Eelis van der Weegen (Workshop on reification and generic tactics, March 31th)

- Bohrification: Topos theory and quantum theory (Third Scottish Category Theory Seminar, invited lecture, 2 Dec)
- Topos theory and quantum theory (PSSL91, accepted contribution)
- Numerical integration in Coq (MAP10, 10 Nov)
- Developing the algebraic hierarchy with type classes in Coq (ITP-10, 13 July)
- The Space of Measurement Outcomes as a Non-commutative Spectrum (DCM, 10 July)
- Quantification over streams (Streams seminar, 21 june)
- Developing the algebraic hierarchy with type classes in Coq (ITP-10, 11-14 July)
- The space of measurement outcomes as a spectrum for non-commutative algebras, at DCM (9-10 Jul)
- Developing the algebraic hierarchy with type classes in Coq (Coq workshop, 9 July)
- Bohrification: Constructive Mathematics and Quantum Mechanics (Constructive Mathematics: Proofs and Computation, 7-11 June, invited lecture)
- The space of measurement outcomes as a spectrum for non-commutative algebras, at QPL10 (video) (29-30May)
- ForMath Kick off meeting. Presentation of Workpackage 4: real number computation (7-9 April)
- The algebraic hierarchy using type classes in type theory (Brouwer seminar, 16, 23, 30 March)

- Mathematics: Algorithms and proofs (Monastir) Numerical integration in Coq (14-18 Dec) slides
- AMS Sectional Florida A topos for algebraic quantum theory (Oct 31)
- Workshop on Constructive mathematics Tutorial on Constructive topology, 3hr. (28-30 Oct).
- Numerical integration in Coq (Brouwer semiar, 21 Oct)
- Computer verified implementation of analysis, Seminar on control and systems theory, (22 Sept)
- Computability and Complexity in Analysis Tutorial on computer verified implementation of analysis (3hr). (video) (18-22 Aug)
- A constructive theory of Banach algebras workshop session on constructive topology, Leeds Symposium on Proof Theory and Constructivism, 3-16 July.
- A topos for algebraic quantum theory, TACL09, 7-11 July, featured talk.
- A constructive theory of Banach algebras (jww Thierry Coquand), Darmstadt 25 June.
- A topos for Algebraic Quantum theory, Darmstadt Mathematical Colloquium, 24 June.

Illustration by Prof. Hofmann. - A constructive theory of Banach algebras(jww Thierry Coquand) (Colloquium on Mathematical Logic, 12 June)
- DESDA Symposium `Constructieve en numerieke analyse' and Discussion panel(15 May)
- A constructive theory of Banach algebras (jww Thierry Coquand) (Brouwer Seminar 31 March)
- New Interactions between Analysis, Topology, and Computation. University of Birmingham, (7-9 Jan)

- A topos for Algebraic Quantum theory, Brouwer seminar 2 Dec
- A computer verified, monadic, functional implementation of the integral (jww Russell O'Connor) Algemeen Wiskunde colloquium TU/e (12/11/2008).
- A computer verified, monadic, functional implementation of the integral (jww Russell O'Connor) General Mathematics Colloquium (12/11/2008).
- A computer verified, monadic, functional implementation of the integral (jww Russell O'Connor) Seminar on Algebra and Logic(11/11/2008).
- A topos for algebraic quantum theory (jww Chris Heunen and Klaas Landsman) DIAMANT meets GQT (30/10/2008).
- A topos for algebraic quantum theory (jww Chris Heunen and Klaas Landsman) Mathematisches Kolloquium (24/10/2008)
- A computer verified, monadic, functional implementation of the integral (jww Russell O'Connor)Stafcolloquium Leiden (18/10/2008).
- Constructive pointfree topology eliminates non-constructiverepresentation theorems from Riesz space theory, Analysis seminar Leiden (18/10/2008).
- A topos for algebraic quantum theory (jww Chris Heunen and Klaas Landsman) Advances in Constructive topology (10/10/2008).
- A computer verified, monadic, functional implementation of the integral (jww Russell O'Connor) ICIS Colloquium (8/9/2008).
- Integrals and valuations (jww Thierry Coquand) Sheaves in Geometry and Quantum Theory (5/9/2008).
- A computer verified, monadic, functional implementation of the integral. Conference on Mathematics, Algorithms and Proofs (jww Russell O'Connor) (28 August 2008).
- Modal logics for probability and possibility via pointfree topology (jww Thierry Coquand). Algebra|Coalgebra Seminar (June 11, 2008)
- A computer verified, monadic, functional implementation of the integral. EIDMA seminar(21/5/2008). (jww Russell O'Connor)
- Some points on pointless topology. Wiskunde Colloquium (23/4/2008)
- A topos for algebraic quantum theory (jww Chris Heunen and Klaas Landsman) Oberwolfach(6-12/4/2008)
- Integrals and valuations (part 2)(jww Thierry Coquand). Brouwer seminar, Radboud university. (1/4/2008).
- Integrals and valuations (jww Thierry Coquand). EIDMA seminar, TU/E (27/2/2008).
- Integrals and valuations (jww Thierry Coquand). Brouwer seminar, Radboud university. (26/2/2008).

Lecture at Categorical Quantum Logic, Oxford.

Observational integration theory

TANCL07, Oxford.

**Abstract:**
In this talk I will present a constructive theory of integration. The
theory is constructive in the sense of Bishop or Brouwer, however we
avoid the axiom of countable, or dependent, choice. Thus our results
can be interpreted in any topos. To be more precise 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. This talk
illustrates the general theme of developing mathematics
observationally, connecting ideas by Kolmogorov, von Neumann and Segal
on the one hand and point-free (aka formal) topology on the other. This
provides a nice illustration how ideas from logic (proof theory) can be
used to obtain mathematical results. By generalizing Isham ideas on
quantum theory we find that this integration theory is also applicable
in the non-commutative context.

Observational integration theory

Invited lecture at the
ASL Meeting in Montreal 2006.

**Abstract:**In this talk I will present a constructive theory of
integration. The theory is constructive in the sense of Bishop or
Brouwer, however we avoid the axiom of countable, or dependent, choice.
Thus our results can be interpreted in any topos. To be more precise 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. This talk illustrates the general theme of developing
mathematics observationally, connection ideas by Kolmogorov, von
Neumann and Segal on the one hand and point-free (aka formal) topology
on the other. This provides a nice illustration how ideas from logic
(proof theory) can be used to obtain mathematical results.

Finally, I will show (by constructing a model) that in this context the
reals can not be proved to be uncountable and show how we live wi
th this fact.

A constructive view on compact groups -
constructive algebra applied to analysis

Talk given at the dagstuhl seminar Verification and Constructive Algebra.
Dagstuhl January 2003.

**Abstract:** We claim that, contrary to Weyl's belief, constructive
mathematics suffices for the applications of mathematics. To support
our claim we prove the Peter-Weyl theorem in a constructive and natural
way.

For this proof we need constructive integration theory, Gelfand theory
and spectral theory. These theories will be outlined in the talk.

As proposed by Weyl we stress that mathematics should be build on basic observables or finite approximations.

To my homepage