2025

British Logic Colloquium (contributed talk), Manchester, UK (Sept 11 - 12)
On Uniform Proof Interpretations [slides]
Continuity, Computability, Constructivity - From Logic to Algorithms (contributed talk), Swansea, Wales (Sept 1 - 3)
Uniform Realizability Interpretations [slides]
Computability in Europe (invited speaker), Lisbon, Portugal (Jul 14 - 16)
On Functional Interpretations and Applied Proof Theory [slides]
Ulrich Berger's retirement celebration (invited speaker), Swansea, Wales (Jun 25)
On Uniform Interpretations of Quantifiers [slides]

2024

Workshop on Proof Mining (participant/speaker), Darmstadt, Germany (Sept 4 - 6)
Bounding Interpretations with Abstract Spaces [slides]
MathFound Seminar (invited speaker), Bath, England (Feb 20)
Quantitative Analysis of Stochastic Approximation Methods [slides]

2023

Winter Meeting in Lisbon - Mathematics & Applications (invited speaker), Lisbon, Portugal (Dec 18 - 20)
The Selection Monad Transformer and Higher-Order Games [slides]
Mathematical Logic Oberwolfach meeting , Oberwolfach, Germany (November 12 - 18)
Quantitative Analysis of Stochastic Approximation Methods [slides]

2022

International Conference on Applied Proof Theory (Kohlenbach's 60th birthday) , Pescara, Italy (Sept 2)
My Years under Ulrich's PhD Supervision [slides]
Proof Mining Seminar , Online (July 13)
Proof Mining in Diophantine Approximation Theory [slides]
Fourth Nordic Logic Summer School (course), Bergen, Norway (Jun 13 - 16)
Realizability [lecture 1, lecture 2, lecture 3, lecture 4]
Theory of Computation Seminar , Birmingham, UK (May 13)
Kripke Semantics for Intuitionistic Łukasiewicz Logic [slides]
Seminário de Pesquisa CIn - UFPE , Recife, Brazil (March 30)
Provas e Programas - A influência da Lógica Matemática na Computação [slides]

2021

Encontro Nacional SPM (Parallel Session: Automated Proofs in Mathematics), Lisbon, Portugal (Jul 12 - 16)
Mining Human Proofs from Machine Proofs [slides]
Bath Mathematical Foundations seminar (invited talk), Bath, UK (Mar 30)
The Selection Monad Transformer - Backward Induction with Mixed Strategies [slides]

2020

Days in Logic (invited tutorial), Lisbon, Portugal (Jan 30 - Feb 1)
Tutorial on Proof Theory [lecture 1, lecture 2, lecture 3]

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

Workshop on Proof Theory and its Applications (invited speaker), Ghent, Belgium (September 6-7)
From intuitionistic affine logic to classical logic, and back [slides]
Logic Colloquium (invited speaker), Udine, Italy (July 23-28)
Relational proof interpretations [slides]
Workshop: Proofs and Computation (invited participant), Bonn, Germany (July 2-6)
On a Dialectica-like version of Kleene numerical realizability [slides]

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

Proof, Computation and Complexity 2016 (invited speaker), Munich, Germany (May 5-6)
[talk] Modified bar recursion - 15 years on
Cambridge Logic and Semantic Seminar (seminar speaker), Cambridge, UK (April 22)
[talk] Logical dependence via functional dependence

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

Trip to Brazil (Dec)
BRICS reatreat, Sandbjerg Estate, South of Denmark (Oct 21 - 23)
FLoC'02 . Copenhagen, Denmark (Jul 20 - Aug 1)
BACC'02 (Bounded Arithmetic and Complexity Classes). Lisbon, Portugal (Jun 28 - 29)
[talk] On modified bar recursion
Meeting on "Mathematische Logik" (pic), Oberwolfach, Germany (Apr 07 - 13)
[talk] Modified bar recursion
Spring School 2002, Semantics of Programming Languages. Agay, France (Mar 23 - 30)

2001 and before...

2001
- Nov 11 - Nov 16. Dagstuhl Seminar CCA'2001 (Computational Complexity in Analysis). Wadern, Germany.
  Talk: On the Computational Complexity of L1-approximation (slides)
- Oct 01 - Feb 01. Visiting Ulrich Berger at University of Swansea, Wales.
- Jul - Trip to Brazil.
- Aug 06 - Aug 11. Logic Colloquium 2001. Vienna, Austria.
  Talk: Effective Bounds on Strong Unicity in L1-Approximation (slides)
- Jun 25 - Jul 06. EEF Summer School on Logical Methods. University of Aarhus, Denmark. Organizer: Ulrich Kohlenbach.
- May 20 - May 20. ICC'01, Aarhus, Denmark.
  Talk:
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
- Dec - Trip to Brazil.
- Oct 18 - 19. BRICS reatreat (pic), Sandbjerg Estate, South of Denmark.
- Jul 30 - Moved to Denmark, (pic). Started my PhD.
- Apr 08 - 12. ACM World Programming Contest, (pic). Eindhoven, Netherlands.
1998
- Aug 31 - Sep 04 . IFIP Congress (1st Youth Summit). Austria-Hungary.