When I have been (will be) away...
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