2022
2020
2019
-
Visiting Fernando Ferreira (PhD defence of Pedro Pinto), Lisbon, Portugal
(Sept 23 - 24)
On the functional interpretation of functional types
[slides]
-
2nd International Summer School on Proof Theory (invited speaker), Swansea, Wales
(Sept 8-11)
Introduction to proof mining and functional interpretations
[lecture 1,
lecture 2,
lecture 3]
- Visiting Chuangjie Xu
@
Mathematical Institute, University of Munich,
Germany (August 5 - 9)
Unifying functional interpretation 2.0
[slides]
-
Proof, Computation, Complexity (invited participant), Djursholm, Sweden
(July 15-19)
On "Approximate" variants of functional interpretations
[slides]
-
Facets of Realizability (invited speaker), Cachan, France
(July 1-3)
On approximate variants of realizability and functional interpretations
[slides]
2018
2017
-
Mathematical Logic Oberwolfach meeting, Oberwolfach, Germany
(November 5 - 11)
Ineffective theorems and higher-order games
[slides]
-
Leeds Logic Seminar, Leeds,
UK
(November 1)
Closure of system T under the bar recursion rule
[slides]
-
British Logic Colloquium, University of Sussex, UK
(September 8-9)
Modular searching with higher-order functions
[slides and Haskell code]
- Visiting Chuangjie Xu
@
Mathematical Institute, University of Munich,
Germany (August 14 - 18)
Closure of system T under the bar recursion rule
[slides]
Symmetric bar recursion
[slides]
- Big Proof,
Newton Institute, Cambridge, UK (June 26 - August 4)
Mining human proofs from machine proofs
[slides]
- Birmingham
Theory Seminar (seminar speaker), Cambridge, UK
(February 24)
Closure of system T under the bar
recursion rule [slides]
2016
2015
- Dagstuhl
meeting: Measuring the Complexity of Computational Content
(invited participant), Dagstuhl, Germany (September 20 - 25)
[talk] Substructural logics, algebras and Weirhrauch
degrees
- British
Colloquium of Theoretical Computer Science, London, UK
(June 29 - July 3)
[talk] A monad for backtracking
- Computability
in Europe, Special session (automata, logic and
infinite games) invited speaker, Bucharest, Romania
(June 29 - July 3)
[talk] Nash equilibrium and unbounded games
- Conference of
Topology, Algebra, and Categories in Logic (invited
speaker), Ischia Island, Italy
(June 21 - 26)
[talk, haskell] Higher-order game theory
- Heyting Day
2015 (invited speaker), Utrecht, Netherlands (February 27)
[talk] On proof interpretations and linear logic
- Dagstuhl
meeting: Coalgebraic Semantics of Reflexive Economics
(invited participant), Dagstuhl, Germany (January 18 - 21)
2014
- Mathematical
Logic Oberwolfach meeting, Oberwolfach, Germany (November 16 - 22)
[talk] Recent applications of
bar recursion and selection functions
- Southampton ESS
Research Seminar, Southampton, UK (November
12)
[talk] Calculating games with higher-order functions
- British
Logic Colloquium (invited speaker), Preston, UK
(September 3-5)
[talk] Bar recursion: A survey
- Logic
Colloquium (PC member), Vienna, Austria (July 14 - 19)
- Logic, Algebra and
Truth Degrees (LATD), Vienna, Austria (16 -
19 July)
[talk] On pocrims and hoops
- Classical Logic and
Computation (Chair), Vienna, Austria (July
13)
- Constructive
Mathematics and Models of Type Theory workshop, Paris,
France (June 2 - 6)
- Algebra
and Coalgebra meet Proof Theory (organiser), Queen
Mary University of London, UK (May 15 - 16)
- Visiting FAU (Bob
Lubarsky), USA
(April 16)
[talk] The logic of the unit interval [0,1]
2013
- 20th Workshop on
Logic, Language, Information and Computation (WoLLIC 2013),
Darmstadt, Germany
(August 20 - 23)
- Logic Colloquium,
Evora, Portugal (July 22 - 27)
- 8th Workshop on
Games for Logic and Programming Languages (GaLoP 2013),
Queen Mary UoL, London, UK (July 18 - 19)
- Combinatorics,
Algebra,
and More, Queen Mary UoL, London, UK (July 8 - 10)
- Visiting Fernando
Ferreira, Lisbon, Portugal
(May 15 - 17)
[talk] Conservation results for the axiom of
choice over constructive theories
2012
- Collegium
Logicum
2012:
Structural
Proof
Theory (invited speaker), Paris, France (November 15-16)
[talk] Algorithms
from proofs in classical arithmetic and analysis
- Florida
Atlantic
University, Algebra and Logic seminar series (seminar
speaker), Boca Raton, USA
(August 31)
[talk] Goedel's
dialectica interpretation: Classical logic, arithtmetic
and analysis
- Classical
Logic
and Computation CL&C 2012 workshop (invited
speaker), Warwick, UK
(July 8)
[talk] Some
connections between proof theory and game theory
- Turing
100 conference (presentation at poster session),
Manchester, UK (June 22 - 25)
[talk] Computing Nash equilibria of unbounded games
- QMUL
EECS Theory Seminar, London, UK (May 31)
[talk] Games and logic
- Montly CHoCoLa
(Curry-Howard: Logic and Computation) meeting (invited
speaker), Lyon, France
(May 10)
[talk] Some connections between proof theory and game
theory
2011
- Visiting Jaime Gaspar and Ulrich Kohlenbach, Darmstadt, Germany (Dec 5 - 6)
[talk] On the restricted form of Spector's bar
recursion
- Invited talk, Logic and
Semantics seminar, Cambridge, UK (Nov 25)
[talk] Nash equilibrium, Bekic's lemma and bar
recursion
- Mathematical
Logic: Proof Theory, Constructive Mathematics, (pic),
Oberwolfach, Germany (Nov 6 - 12)
[talk] Nash equilibrium, Bekic's lemma and bar
recursion
- Visit to LIAMF
group, USP, Brazil (Oct
22)
[talk] Sequential games and optimal strategies
- Computing
with Infinite Data, Dagstuhl, Germany (Oct 9 - 14)
[talk] A finitisation of the infinite Ramsey theorem
- 14th CLMPS
(invited speaker), special session on "Mathematical Logic",
Nancy, France (Jul 19 - 26)
[talk] Goedel's dialectica interpretation: Classical
logic, arithtmetic and analysis
- 27th Conference
on Mathematical Foundations of Programming Semantics (MFPS
XXVII) (invited speaker), Pittsburgh, USA (May 25 - 28)
[talk] Programs from classical proofs via Goedel's
dialectica interpretation
- Federico
Aschieri, PhD defence, Turin, Italy (April 11)
- 10th Wessex
Theory Seminar (speaker), Swansea, UK (April 7)
[talk] The dialectica interpretation of classical logic
2010
- Leeds
Logic Seminar, Leeds, UK (Dec 8)
[talk] The theory of selection functions
- Swansea
University - Proof, Complexity, Verification Seminar,
Swansea, UK (Nov 23)
[talk] The theory of selection functions
- Loughborough
University - CS Departmental Seminar, Loughborough, UK (Nov 17)
[talk] Sequential games and optimal strategies
- Program
Extraction and Constructive Proofs (PECP), Brno, Czech Republic (Aug 23 - 27)
[talk] Theorems, games, proofs and optimal strategies
- Logic Colloquium 2010
(invited speaker), Paris, France
(Jul 25 - 31)
[talk] Sequential games and optimal strategies
- Computability in
Europe (CiE 2010) (invited speaker), special session
"Proof theory and computation", Azores, Portugal (Jun 30 - Jul 4)
[talk] Bar recursion and the product of selection
functions
- ASL 2010 North
American Annual Meeting (contributed talk),
Washington, USA (Mar 17 - 20)
[talk] Instances of bar recursion as products of
selection functions
- Wessex
Theory Seminar, Southampton, UK (Feb 19)
[talk] Selection functions in proof theory
2009
- Imperial
College LogIC Seminar, London, UK (Nov 26)
[talk] Selection functions and attainable quantifiers
- Gentzen
Centenary workshop (invited speaker), Coimbra, Portugal (Sep 12)
[talk] Spector's bar recursion as an infinite product
selection functions
- Computer Science
Logic (plenary speaker), Coimbra, Portugal (Sep 7 - 11)
[talk] Functional interpretations
- British Logic
Colloquium (invited speaker) (pic),
Swansea,
UK (Sep 3 - 5)
[talk] Selection functions, bar recursion and Nash
equilibrium
- Logic and
Mathematics Conference, York, UK (Aug 3 - 7)
- Leeds
Symposium on Proof Theory and Constructivism, Leeds, UK (Jul 3 - 16)
- Realizability
workshop (invited tutorial), Chambery, France
(Jun 2 - 5)
[talk] Realizability interpretations of linear logic
- Pure
Maths Seminar, Maths dept, QMUL, London (May 18)
[talk] Brief introduction to proof mining
2008
- Domains
IX (contributed talk) Brighton, UK (Sep 22 - 24)
[talk] On variants of modified bar recursion
- Colloquium
Logicum, Darmstadt, Germany (Sep 10 - 12)
- Meeting on "Mathematische
Logik" (invited tutorial) (pic),
Oberwolfach, Germany (Apr 7 - 11)
[talk] Dialectica interpretation in the light of linear
logic
- Visiting GKLI,
Munich, Germany (Jan 21 - 25)
[talk] On variants of modified bar recursion
2007
- Visiting Martin
Escardo, Birmingham, UK (Ago 24 - 27)
[talk] Recent developments in Proof Mining
- European
Logic Colloquium'2007, Wroclaw, Poland (Jul 14
- 19)
- TMCNAA
workshop (invited speaker), Wroclaw, Poland (Jul 15)
[talk] Hoare logic in the abstract
- LICS
- Logic in Computer Science (contributed talk), Wroclaw, Poland (Jul 10 - 14)
[talk] Modified realizability interpretation of classical
linear logic
- WoLLIC - Workshop on
Logic, Language, Information and Computation (invited
speaker), Rio de Janeiro, Brazil
(Jul 2 - 5)
[talk] Computational interpretations of classical linear logic
- Trimestre
on methods of proof theory, Max-Planck Institute for
Mathematics, Bonn, Germany
(Jun 2 - 6)
[talk] Functional interpretations and games
- BMC - British Mathematical
Colloquium (invited speaker), special session "Splinter
group in logic", Swansea, UK
(Apr 16 - 19)
[talk]
Theorems and symmetric games
- Trimestre
on methods of proof theory, Max-Planck Institute for
Mathematics, Bonn, Germany
(Mar 1 - 30)
[talk]
A game called Mathematics
- MAP
- Mathematics, Algorithms and Proofs, Lorentz Center,
Leiden, Holland (Jan 8 - 12)
[talk]
Modified realizability of linear logic
2006
- Invited talk, Logic and
Semantics seminar, Cambridge, UK (Oct 6)
- British Logic Colloquium, Oxford, UK (Sept 7 - 9)
- CiE (invited
speaker) (pic),
special
session
on
"Computability
in
analysis"
Swansea,
Wales (Jun 30 - Jul 5)
[talk]
Understanding and using Spector's bar recursive
interpretation of classical analysis
- ASL Annual meeting (invited
speaker), special session on "Effective aspects of measure
theory and analysis" Montreal, Canada
(May 17 - 21)
[talk]
Effective WKL conservation in feasible analysis
- London Theory Day,
Imperial College (Apr 24)
[talk]
Abstract Hoare logic
- Visiting GKLI
(invited tutorial) Munich, Germany
(Mar 28 - 31)
[talk
1, talk
2, talk
3] Functional interpretations
2005
- ACM ICPC Northwestern
regional. Stockholm, Sweden
(Nov 12 - Nov 14)
Coaching a team of students from QM
- Visiting Professor Fernando
Ferreira, Lisbon, Portugal (Oct 18 - Oct 26)
- PCC
workshop (invited speaker), Lisbon, Portugal (Jul 16 - Jul 17)
[talk]
Computational interpretations of the contraction
axiom
- Workshop
on
applications of proof assistants (invited talk), Venice, Italy
( Mar 29 - Apr 1)
[talk]
Functional interpretations
- Mathematical
Logic: Proof Theory, Type Theory and Constructive Mathematics
(pic),
Oberwolfach,
Germany (Mar 20 - Mar
26)
[talk]
Unifying functional interpretations
- MAP - Mathematics,
Algorithms and Proofs (pic),
Schloss
Dagstuhl,
Germany (Jan 9 - Jan 15)
[talk]
Unifying functional interpretations
2004
- Visiting Professor Fernando
Ferreira, Lisbon, Portugal (Nov 20 - 27)
[talk]
Unifying functional interpretations
- The Nature
of Mathematical Proof, Royal Society, London, UK (Oct 18 - 19)
- 2nd Workshop on
the Logic for Pragmatics, Paris, France (Jul 23 - 24)
[talk] On different interpretaions of classical countable
choice
- 25 Years of CSP,
London, UK (Jul 7 - 8)
- 4th
Conference on Integreted Formal Methods (pic),
Canterbury,
UK (Apr 4 - 7)
- MAP
- Mathematics, Algorithms and Proofs (pic),
Marseille,
France (Jan 11 - 20)
[talk]
Bounded functional interpretation
2003
- LICS'2003
(contributed talk), Ottawa, Canada (Jun 22 - 25)
[talk]
Polynomial-time programs from ineffective proofs in
feasbile analysis
- ASL Annual
meeting 2003 (contributed talk), Chicago, USA (May 29 - Jun 5)
[talk]
Polynomial-time programs from
ineffective proofs in feasbile analysis
- Workshop
on Proof Theory and Algorithms, Edinburgh, Scotland
(Mar 23 - 29)
[talk] Polynomial-time programs from
ineffective proofs in feasbile analysis
2002
2001 and before...
- 2001
- 2000
- Dec - Trip to Brazil.
- Oct 18 - Oct 20. BRICS
reatreat (pic),
Sandbjerg
Estate,
South
of
Denmark.
- Aug 06 - Aug 18. ESSLLI 2000
(pic).
University
of
Birmingham,
UK. Organizers: Achim Jung (chair) and Eike Ritter.
- Jul 16 - Aug 05. 2000 Summer
Session -- Computational Complexity Theory. Institute
for Advanced Study, Princeton, NJ, USA.
- 1999
- 1998