2018
- Invited lecture on "Generalised predicativity, tests and the
meaning explanations of intuitionistic type theory" at the
conference
Das
Kontinuum - 100 Years Later", University of Leeds, 11-14.
- Visit at the Centre for Advanced Studies at the Norwegian
Academy of Science and Letters, Oslo, 23 - 31 August. Lecture on
"Internal type theory revisited" at the
kickoff meeting for the programme Programme
Homotopy Type Theory and Univalent Foundations.
- Types 2018 in Braga, 18-21 June. Member of the Programme Committee.
- Visit to Hausdorff Research Institute for the programme Types, 29 May - 15 June.
Sets, Constructions 29 May - 15 June.
- Lectures on Intuitionistic
Type Theory for the Summer School on Types, Sets and Constructions,
Hausdorff Research Institute for Mathematics, Bonn, 3 - 9 May.
- Visit to ENS Lyon, 5 - 9 March.
- AIM XXVI, Budapest, 29 January - 2 February.
2017
- External examiner for PhD thesis of Ernesto Copello, Montevideo,
21-26 August. Workshop.
- Logic Colloquium, Stockholm, 14-19 August.
- Big Proof, Cambridge, 10-14 July.
- MFPS, Ljubljana, 12-15 June.
- AIM XXV, Goteborg, 9-15 May.
- Meeting in Nantes, 25-28 April.
- Meeting on Univalent Foundations, Ljubljana, 31 January - 3
February.
- Visit to Cambridge University, Computer Laboratory, 16 - 20
January. Lecture on "Finitary higher inductive types in the groupoid
model".
2016
- Invited lecture at the Logic and
Computability session of V Congreso Latinoamericano de
Matematicos, Barranquilla, Colombia, 11 - 15 July, 2016.
- Visit and lecture at EAFIT University, Medellin, Colombia, 18 - 20 July, 2016.
- Member of the Program Committee of Mathematical Foundations
of Programming Semantics - MFPSXXXII, Pittsburg, Pennsylvania,
23-26 May.
- Invited visiting researcher at the School of Mathematics, Institute for
Advanced Study, Princeton, New Jersey, 29 March - 12 April.
- Lecture on Game Semantics and Normalization by Evaluation, IT
University of Copenhagen, 27 April.
- External PhD Examiner of Daniel Gustafsson, IT University of
Copenhagen, 26 April.
- Research visit at ENS Lyon, 7 - 13 February.
- External PhD Examiner of Erik Parmann, University of Bergen, 22 January.
- Invited speaker at the Bergen Workshop on Computational Aspects
of Univalence, 20 - 22 January.
2015
- Invited speaker at Categorical
Logic Workshop, Stockholm, 3 -
4 December.
- Visit to Carnegie Mellon University, 22 - 26 November. Lectures
in the Principles
of Programming Seminar and Pure and Applied Logic Colloquium.
- Member of the programme committee of TLCA 2015 - 13th
International Conference on Typed Lambda Calculi and
Applications, Warsaw, Poland, 29 June - 3 July.
- Invited guest lecturer at the
Oregon Programming Languages Summer School, Eugene, Oregon, 15 - 27
June 2015.
- Participant at the Agda
Implementors Meeting XXI, Gothenburg, 3 - 9 June. Lecture on
"Implementing Martin-Lof's Meaning Explanations in Agda".
- Participant at the 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), London, 13 - 16 April.
- Participant at the 10th
Workshop on Games for Logic and Programming Languages (GALOP), London, 11 - 12 April.
2014
- Research visit at ENS Lyon, 30 November - 5 December.
- Research visit at Department of Mathematics at the University of
Stockholm, 2 - 7 November. Lecture on Game Semantics and
Normalization by Evaluation.
- Participant at ICFP
2014, The 19th ACM SIGPLAN International Conference on Functional Programming, Goteborg, 1 - 3 September.
- Participant (as supervisor) at the PhD defence of Andres
Sicard-Ramirez, Montevideo, Uruguay, 25 July.
- Participant Workshop
on dependently typed programming Montevideo, Uruguay, 21 - 24 July. Lectures "A Brief Introduction
to Homotopy Type Theory" and "Tests, Games and Martin-Lof's Meaning Explanations".
- Participant at the Trimester on Semantics of
Proofs and Certified Mathematics, Institut Henri Poincare, Paris, 29 April - 2 May and 19 May - 6 June.
Invited talk at the Workshop on Constructive Mathematics and Models of
Type Theory, 2 - 6 June.
- Lecture at the IT University of Copenhagen, 28 April.
- An episode in the Type Theory Podcast on
Types
and Testing.
2013
- External examiner for Fredrik Forsberg, Swansea University. September 2013.
- AIM XVIII, Goteborg, 12 - 18 September.
- Foundations of Mathematics for Computer-Aided Formalization of Mathematics, Padova, 9-11 January 2013. Invited speaker.
- Institute for Advanced Study, Princeton, NJ, March-April
2013, Invited participant at the Special Year on Univalent Foundations.
- Habilitation seminar of Andreas Abel, Ludwig Maximiians Université–£, Munich, 31 May 2013. Member of the Fachmentorat.
- Symposium on Semantics and Logics of Programs, 5 June 2013. A symposium in connection with my 60th birthday
- PxTP 2013, Third
International Workshop on Proof Exchange for Theorem Proving, Lake Placid 9-10 June 2013. Member of program committee.
2012
- Institute for Advanced Study, Princeton, NJ, November - December
2012, Invited participant at the Special Year on Univalent Foundations.
- 16th Agda Implementors Meeting, 3-9 October 2012, Copenhagen.
- 8th Scandinavian Logic Symposium, Roskilde, 20-21 August 2012. Member of programme
committee
- Interactive Theorem Proving, Princeton, NJ, 13-15 August 2012. Member of programme committee
- CIAO
workshop, Goteborg, 18-19 April 2012. Lecture on Combining
Interactive and Automatic Reasoning in a First Order Theory of
Functional Programs.
- First Workshop on Automation in Proof Assistants (AIPA), Tallinn 31 March - 1
April. Participant.
- 15th International
Conference on Foundations of Software Science and Computation
Structures (FOSSACS), Tallinn, 27 - 30 March 2012. Contributed
paper on Combining Interactive and Automatic Reasoning
in First Order Theories of Functional Programs (with Ana Bove and
Andres Sicard-Ramirez).
- Examintion of PhD thesis of Miguel Pagano, Universidad National Cordoba,
Argentina. 23 March 2012. Lecture on Tests, Games and Martin-Lof's
meaning explanations for Intuitionistic Type Theory.
- 15th Agda Implementors Meeting, Fischbachau, 19-26 February 2012. Participant.
- Logic and Interaction, CIRM, Luminy, Marseille. 5 - 17 February
2012. Invited lecture
on Tests, Games andMartin-Lof's
meaning explanations for Intuitionistic Type Theory.
2011
- Workshop
to Celebrate Peter Hancock's 60th Birthday, Glasgow
19 December 2011. Lecture: Thoughts on Martin-Lof's Meaning Explanations.
- Workshop on Proofs
and Programs, 22 October 2012. Lecture on The Evolution of Inductive
Definitions in Type Theory (a Retrospective)
to Christine Paulin on the occasion of her honorary doctorate at Gothenburg University.
- Workshop on Dependently Typed Programming, Shonan Village,
Japan, 14-17 September 2011. Participant.
- 14th Agda Implementors Meeting, Shonan Village, Japan, 6 - 14
September 2011. Organizer.
- Gunma University, Japan, 5 - 9 September. Lectures on
Constructive Mathematics and Computer Programming - Some Background
and on Program
Testing and Constructive Validity.
- Typed Lambda Calculus and Applications, Novi Sad, 1 - 3 June
2011. Contributed paper on The Biequivalence of Locally Cartesian
Closed Categories and Martin-Lof Type
Theory (with Pierre Clairambault).
- 13th Agda Implementors Meeting, Goteborg 6 - 12
April 2011. Organizer.
- Invited lecture on Program Testing and Constructive Validity at the Oberseminar
Logik und Sprachtheorie at the University of
Tubingen, 8 February 2011.
2010
- Examination of PhD thesis of Dag Hovland, Bergen, 16 December
2010.
- ICFP 2010 : The 15th ACM SIGPLAN International Conference on Functional Programming, Baltimore, Maryland, 27-29 September 2010. Member of programme committee.
- Workshop on Induction-recursion, Edinburgh 15-16 September,
2010. Lecture on the Biequivalence of Locally Cartesian
Closed Categories and Martin-Lof Type
Theory.
- LFCS seminar, Edinburgh, 14 September, 2010. Lecture on Program
Testing and Constructive Validity.
- Uppsala-Stockholm Logic Seminar, 24 August, 2010. Lecture
The Biequivalence
of Locally Cartesian Closed Categories
and Martin-Lof Type Theory with Pi, Sigma and
Extensional Identity Types .
- ICALP 2010, 37th International Colloquium on Automata, Languages and Programming, Bordeaux, 5-12 July 2010. Member of programme committee.
- Examination of PhD thesis of Jacob Thamsborg, IT University of Copenhagen, 15 June, 2010.
- Programming and Constructive Mathematics A symposium in connection with Jan Smith's 60th birthday. 31 May 2010. Organizer.
2009
-
10th Agda Implementors' Meeting, Goteborg, 14-18 September 2009. Organizer.
- 6th Workshop on Fixed Points in Computer Science, FICS 2009,
Coimbra, Portugal, 12-13 September 2009. a satellite workshop to CSL
2009. Member of programme committee.
- Research meeting for EPSRC-project on Induction-Recursion. Swansea, UK, 5 - 6 September 2009.
- British Logic Colloquium
2009. Swansea, UK, 3 - 5 September 2009. Invited lecture on
Program Testing and Constructive Validity.
- 22nd Conference on Theorem Proving in Higher Order Logics (TPHOLs), Munich, 17-20 August 2009. Member of programme committee.
- Workshop on
Normalization by Evaluation, Los Angeles, Ca, 15 August 2009,
co-located with LICS
2009. Keynote lecture: Normalization by Evaluation
and the Foundations of Constructive Mathematics
1972 - 2009
- Philosophy and Foundations of
Mathematics: Ontological and Epistemological Aspects, Uppsala,
5-8 May 2009. Member of organizing and programme committee.
-
Midlands Graduate School in the Foundations of Computer Science, Leicester, UK, 30 March - 3 April, 2009. Invited lecturer.
- Programming, Types, and Languages. A symposium in connection with Bengt Nordstrom's 60th birthday. 19 March 2009. Organizer.
- 14th Estonian Winter School in Computer Science (EWSCS), Palmse, Estonia, 1-6 March, 2009. Invited lecturer.
-
ACM SIGPLAN
Workshop on Types in Language Design and Implementation affiliated
with POPL 2009 21-23 January, 2009, in Savannah, Georgia. Member of the programme committe.
- Public defense of PhD thesis of Johan Granstrom, Reference and Computation in Intuitionistic Type Theory, Uppsala 16 January 2009. Faculty opponent.
- Minisymposium on Type Theory and Foundations, Uppsala, 15 January 2009. Lecture on Program Testing and Constructive Validity.
2008
-
9th Agda Implementors' Meeting, Sendai, Japan, 27 November - 3
December, 2008. Participant.
- 5th IFIP International Conference on Theoretical Computer Science (TCS-2008), Milano, 7-10 September 2008. Member of the programme committee.
- Mathematics of Program Construction (MPC '08), Marseille (Luminy), France, 15-18 July 2008. Member of the programme committee.
- University of Cambridge, Computer Laboratory, 27 June 2008. Seminar on The Interpretation of Intuitionistic Type Theory - an Intuitionistic Perspective.
-
International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'08), 23 June 2008. Workshop
affiliated with LICS-23 at Pittsburgh, Pennsylvania. Member of the programme committee.
- 8th Agda Implementors' Meeting, Goteborg, 29 May - 4 June 2008. Organizer.
- Twenty-fourth Conference on the Mathematical Foundations of
Programming Semantics (MFPS XXIV), Philadelphia, PA, 21-25 May 2008. Invited speaker at the special session honoring Phil Scott on the occasion of his 60th birthday year.
- National Institute of Informatics, Tokyo, 21 April 2008. Lecture on Normalization by Evaluation.
- International Symposium on Functional and Logic Programming (FLOPS 2008), Ise, Japan, 14-16 April 2008. Invited speaker.
- 25 Year Anniversary of the Stockholm-Uppsala Logic Seminar. Symposium on Type Theory, Uppsala, 26 March 2008. Lecture on Category-Theoretic Approach to Type-checking Dependent Types.
- National University of Cordoba, Argentina, 3 March 2008. Lecture on Normalization by Evaluation.
- Summer School on Language Engineering and Rigorous Software Development (LerNet), Piriapolis, Uruguay, 25 February - 1 March 2008. Lectures on Dependent Types at Work.
- University of Warsaw, open lectures for PhD students in computer science, 18-19 January 2008. Lectures on Normalization by evaluation.