Slides of some of my talks
This page contains slides of some of my talks.
2020
2018
2017
2016
2015
2014
2013
2012
2011
- 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)
2010
- 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)
2009
- 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)
2008
- 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).
Before 2008
A topos presentation of C*-algebra based physical systems
(jww Chris Heunen)
Lecture at Categorical Quantum Logic, Oxford.
Abstract:
We show how a C*-algebra naturally induces a topos in which the family
of its commutative subalgebras becomes a commutative C*-algebra. Its
internal spectrum is a compact regular locale, and the Kochen-Specker
theorem is equivalent to this spectrum having no points.
(Quasi-)states become integrals, and self-adjoint
elements become functions to the pertinent generalised real numbers
(the interval domain). This provides a probabilistic interpretation of
propositions in quantum theory. The topos-theoretic truth value of such a
proposition is the collection of pure states of commutative
subalgebras that make it true; in a physical interpretation these are
the pure states for a classical observer making the proposition
true. These results were motivated by a topos-theoretic approach of
the Kochen-Specker theorem by Isham and co-workers. Our main tool is
the use of the internal mathematics of a topos, such as the
constructive Gelfand duality of Banaschewski and Mulvey, which
simplifies the computations and provides very natural connections
between internal and external reasoning.
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