Talks

Last update: 21 June 2022.

Modalities and Erasure in a Dependently Typed Language: 21 June 2022, 28th International Conference on Types for Proofs and Programs, Nantes, France.

2021

On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction: 7 June 2021, 27th International Conference on Types for Proofs and Programs, online.

2020

Type-preserving compilation via dependently typed syntax in Agda: 16 January 2020, IFIP 1.3 Meeting, Massa Marittima, Italy.
Similar talk planned for TYPES 2020, Torino, Italy, 2-5 March 2020. (Cancelled due to COVID-19.)

2019

Resolving the circularity of infinite processes via sized coinductive types: 22 November 2019, Circularity in Syntax and Semantics, Gothenburg University, Sweden.
Normalization by Evaluation for Call-By-Push-Value: 13 June 2019, 25th International Conference on Types for Proofs and Programs, TYPES 2019, Oslo, Norway.
Similar talk given 28 June 2019 in the TCS Oberseminar, LMU München, DE.
Informal talk given 22 May 2019 in the Programming Logic seminar, Chalmers.
How to Represent It in Agda: 13 March 2019, 29th Agda Implementors' Meeting, AIM XXIX, Ochanomizu University, Tokyo, Japan
slides Agda code (stub)
Agda Tutorial in Advanced Functional Programming course: 4 March 2019, Chalmers, Gothenburg
Agda installation essentials: see ESSLLI 2016
Agda sources after live coding: .zip html
Correct-By-Construction Programming in Agda: 14 January 2019, Tutorial at the 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019), Hotel Cascais Miragem, Lisbon, Portugal
On Proof-Relevant Relations and Evidence-Aware Programming: 11 January 2019, TCS Oberseminar, LMU München, DE

2018

Lifting linear laws: On the preservation of linear equational laws under the pointwise lifting to sets: 21 November 2018, Programming Logic seminar, Chalmers, Gothenburg, Sweden
Handout: .pdf
Normalization by Evaluation for Intuitionistic Propositional Logic: 19 July 2018, Initial Types Club, Chalmers, Gothenburg, Sweden
PDF Handout: local github Agda code: html github
On Typed Lambda Definability and Normalization By Evaluation: 6 July 2018, IFIP 1.3 Meeting, Royal Holloway University, London, UK
Agda code: listing github
Resourceful Dependent Types: 20 June 2018, 24th International Conference on Types for Proofs and Programs, TYPES 2018, Braga, Portugal
On Typed Lambda Definability and Normalization By Evaluation: 7 June 2018, 27th Agda Implementors' Meeting (AIM XXVII), Chalmers Teknikparken, Gothenburg, Sweden
Agda code: listing github
Introduction to Dependent Types and Agda: 2 lectures during the 8th Summer School on Formal Techniques, Menlo College, Atherton, California, USA, 21-25 May 2018.
On the Syntax and Semantics of Quantitative Type Theory: 19 April 2018, Workshop on Mixed Inductive-Coinductive Reasoning, Institute for Computing and Information Sciences, Radboud University, Nijmegen, The Netherlands
On the Syntax and Semantics of Quantitative Type Theory: 11 April 2018, Informal talk in the Programming Logic Seminar, Department of Computer Science and Engineering, Chalmers
Compositional Coinduction with Sized Types: 16 February 2018, Functional Programming Seminar, School of Computer Science, University of St Andrews, Scotland, UK
What is a monotone dependently typed function?: 9 January 2018, Winter Meeting 2018 of the Division of Functional Programming, Salt & Sill, Tjörn, Sweden
Talk given again on 10 January 2018 in the Programming Logic Seminar, Department of Computer Science and Engineering, Chalmers

2017

Normalization by Evaluation for Sized Dependent Types: 6 September 2017, 22nd ACM SIGPLAN International Conference on Functional Programming, ICFP 2017, Oxford, UK
Formal Languages, Coinductively Formalized: Invited talk, 19 July 2017, Workshop on Termination and Circular Proofs, Department of Mathematics (LAMA), Université Savoie Mont Blanc, Chambery, France
Agda Tutorial at Big Proof 2017: 30 June 2017, Issac Newton Institute, Cambridge, UK

Tutorial material for live coding: Tutorial.zip Individual files: Tutorial.agda Prelude.agda TreeSortOrd.agda Copatterns.agda Rewriting.agda Cubical.agda
Normalization by Evaluation for Sized Dependent Types: 30 May 2017, 23nd International Conference on Types for Proofs and Programs TYPES 2017, Budapest, Hungary
Formal Languages, Coinductively Formalized: Seminar on the occasion of Jesper Cockx' non-public defense, Department of Computer Science, KU Leuven, Belgium, 17 May 2017
Programming Language Technology: Putting Formal Languages to Work: 11 May 2017, guest lecture in class Finite Automata Theory and Formal Languages TMV027/DIT321, Chalmers and Gothenburg University, Sweden.
Slides: .pdf Code: .zip
Eating Your Own Dog Food: 9 May 2017, 25th Agda Implementor's Meeting (AIM XXV), Chalmers, Gothenburg, Sweden.
Normalization by Evaluation: 9 March 2017, Mathematical Engineering PhD Seminar, EAFIT University, Medellin, Colombia.
Slides
Agda Tutorial in Advanced Functional Programming course: 23 February 2017, Chalmers, Gothenburg
Agda installation essentials: see ESSLLI 2016
Agda sources for live coding: .zip
Formal languages, coinductively formalized in Agda: 31 January 2017, COST Action CA15123 EUTYPES MC & WG Meeting, Ljubljana, Slovenia
Compositional Coinduction in Agda: 10 January 2017, IFIP 1.3 Meeting 26, Ostseebad Binz, Germany
Code: .agda

2016

Translating between Agda and Dedukti: Universality of Proofs (Dagstuhl seminar 16421)
18 October 2016, Schloss Dagstuhl, Wadern, Germany
Seminar report: http://dx.doi.org/10.4230/DagRep.6.10.75
Agda Tutorial at Proof and Computation 2016: Autumn School Proof and Computation
3-8 October 2016, Aurachhof, Fischbachau, Bayern, Germany

Tutorial material for live coding: Prelude.agda TreeSortBool.agda TreeSortOrd.agda Copatterns.agda
Solutions: TreeSortOrdSolution.agda CopatternsSolution.agda
Solutions pretty: TreeSortOrdSolution.html CopatternsSolution.html
Type Theory. A Constructive Foundation for Logics and Computer Science: Introductory course (5 × 90 min)
28th European Summer School in Logic, Language and Information (ESSLLI 2016)
Bolzano-Bozen, South Tyrol, Italy, 15-26 August 2016
How to Keep Your Neighbors in Order: An Agda tutorial using Conor McBride's beautiful representation of binary search trees
30 June 2016, guest lecture in Computer Aided Formal Reasoning, class by Gordon Cichon and Martin Hofmann, Institut für Informatik, Ludwig-Maximilians-Universität München
Agda code: .html .zip
Normalization by Evaluation in the Delay Monad: 24 May 2016, 22nd International Conference on Types for Proofs and Programs TYPES 2016, Novi Sad, Serbia
Programming Language Technology: Putting Formal Languages to Work: 16 May 2016, guest lecture in class Finite Automata Theory and Formal Languages TMV027/DIT321, Chalmers and Gothenburg University, Sweden.
Slides: .pdf Code: .zip
Formal Languages, Coinductively Formalized: 19 April 2016, Departmental Seminar CISeminar, Computer and Information Sciences, Strathclyde University, Glasgow, Scotland, UK
Compositional Coinduction with Sized Types: 13th IFIP WG 1.3 International Workshop on Coalgebraic Methods in Computer Science (CMCS 2016)
Part of ETAPS 2016
3 April 2016, Eindhoven, the Netherlands
Slides: .pdf Agda code: .zip Agda code pretty: unsized sized
Similar talk given 13 April 2016 in the ProgLog Seminar, Department of Computer Science and Engineering, Chalmers and Gothenburg University, Gothenburg, Sweden.
Coinduction in Agda via Copatterns and Sized Types: Language Based Verification Tools for Functional Programs (Dagstuhl seminar 16131)
30 March 2016, Schloss Dagstuhl, Wadern, Germany
Slides: .pdf Agda code: .zip Agda code pretty: unsized sized
Agda Tutorial at FLOPS 2016: 13th International Symposium of Functional and Logic Programming (FLOPS 2016)
6 March 2016, Kochi, Japan
Slides: .pdf Start: .agda Solution: .agda Solution pretty: .html
Interactive Programs and Objects, Functionally -- Via Coinduction with Copatterns and Sized Types in Agda: 2 March 2016, Dept. of Communications and Computer Engineering, Graduate School of Informatics, Kyoto University, Japan
Agda code: .zip Agda code pretty: .html
Agda Tutorial in Advanced Functional Programming course: 24 February 2016, Chalmers, Gothenburg
Agda sources: .zip

2015

Coinduction in Agda Using Copatterns and Sized Types: 15 December 2015, Workshop on Advances in Programming Languages and Systems (APLS 2015), Frankfurt a.M., Germany.
Agda code
Implementierung und Verifikation von Prozessen mittels Komusterabgleich: Herbst 2015, in einem Institut für Informatik einer deutschen Universität
Coinduction: Formalizing infinite computations in Type Theory: 25 June 2015, FireEye Research & Development Dresden, Germany

On an abstract level, servers and operating systems can be seen as infinite processes that continuously accept a request and send a response. While such a process should not terminate, but run potentially infinitely, each request should terminate with a response. Mathematically, such behavior can be modeled by coinduction.
In this talk, I introduce coinduction via some examples and show how to program and reason coinductively in the Agda proof assistant. This includes a presentation of my research on copatterns and sized types.
10 Years of Agda2: 3 June 2015, 21st Agda Implementor's Meeting (AIM XXI), Chalmers, Gothenburg, Sweden.
Logic and Language, Proposition and Types, Proofs and Computation: 21 April 2015, Introduction to Programming Logic research for 1st year students, Seminarier i Data och IT Chalmers, Gothenburg, Sweden.
Code: .agda

2014

Strong Normalization for Guarded Recursive Types: 18 December 2014, Theory Seminar, Institute of Cybernetics, Tallinn Technical University, Tallinn, Estonia.
Strong Normalization for Guarded Types: 20 August 2014, Programming Logics and Semantics Group, ITU, Copenhagen, Denmark.
Coinduction in Agda Using Copatterns and Sized Types: 7 July 2014, Workshop on Certification of High-Level and Low-Level Programs, part of the Institut Henri Poincaré thematic trimester Semantics of proofs and certified mathematics, Paris, France.
Coinduction in Agda Using Copatterns and Sized Types: 15 May 2014, Types for Proofs and Programs ( TYPES 2014), part of the Institut Henri Poincaré thematic trimester Semantics of proofs and certified mathematics, Paris, France.
The Present and Future of Agda: 7 March 2014, ProgLog Day, Ågrenska villa, Gothenburg, Sweden.
Programming and Reasoning with Infinite Structures Using Copatterns and Sized Types: 26 February 2014, 7. Arbeitstagung Programmiersprachen ( ATPS 2014), part of the GI-conference Software Engineering 2014, Christian-Albrechts-Universität Kiel, Germany.
Abstract published in CEUR SE-WS 2014.
Productive Infinite Objects via Copatterns and Sized Types in Agda: 30 January 2014, Representing Streams II, Lorentz-Center, Leiden, Netherlands.

2013

Productive Infinite Objects via Copatterns: 21 November 2013, 25th Nordic Workshop on Programming Theory (NWPT'13), Brotherhood of the Black Heads, Tallinn, Estonia.
On Lenses and Traversals: 19 November 2013, Informal talk in the Theory Seminar, Institute of Cybernetics, Tallinn, Estonia.
Pattern Inductive Families Need Not Store Their Indices, Ever: 13 November 2013, Informal talk in the Programming Logics Seminar, Department of Computer Science and Engineering, Chalmers, Gothenburg, Sweden. Unfinished slides.
Wellfounded Recursion with Copatterns: 7 October 2013, (NII Shonan Meeting 026:), Coinduction for computation structures and programming languages, Shonan Village Center, Kanagawa prefecture, Japan.
Agda as a Library?! Modularization of the Implementation and Stuff: Informal talk at the 18th Agda Implementor's Meeting, AIM XVIII, Teknikparkens Konferenscenter, Chalmers, Gothenburg, Sweden.
Wellfounded Recursion with Copatterns: 26 September 2013, The 18th ACM SIGPLAN International Conference on Functional Programming (ICFP 2013), Hilton Logan Airport, Boston, MA, USA.
Copatterns: Programming Infinite Structures by Observations: 4 July 2013, Institute of Cybernetics, Theory Seminar, Tallinn, Estonia.
Normalization by Evaluation: Dependent Types and Impredicativity: 31 May 2013, Department of Computer Science, Ludwig-Maximilians-University Munich. Habilitation talk.
Copatterns: Programming Infinite Structures by Observations: 23 Jan 2013, 40th ACM Symp. on Principles of Programming Languages, POPL 2013, Rome, Italy.
Similar talk given 18 Jan 2013 in the TCS Oberseminar, LMU Munich.

2012

Strong Normalization for Lambda-Calculus II: Semantic Methods: 6 Dec 2012, Lecture given for the Logic and Computation Group, McGill University, Montreal, Canada.
Strong Normalization for Lambda-Calculus I: Syntactic Methods: 4 Dec 2012, Lecture given for the Logic and Computation Group, McGill University, Montreal, Canada.
Copatterns: Programmig Infinite Structures by Observation: 7 Nov 2012, Oberseminar Mathematische Logik, LMU Munich.
Copatterns: A new syntax for the definition of infinite things, like functions and objects defined by coinduction: 4 October 2013, Informal talk at the 16th Agda Implementor's Meeting, AIM XVI, ITU Copenhagen, Denmark.
Programming and Program Verification with Dependent Types in Agda: 8 May 2012, Seminar Lehrstuhl Theoretische Informatik, Friedrich-Alexander-Universität Erlangen.
Agda code
Similar talk given at the PUMA/RISE Workshop, Goldegg, Austria, 27 September 2012.
Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types: 24 March 2012, Invited talk at the Workshop on Fixed Points in Computer Science, FICS 2012, part of ETAPS 2012, Tallinn, Estonia.
A Semantics for Agda's Mixed Inductive-Coinductive Types: 22 February 2012, 15th Agda Implementor's Meeting, AIM XV, Fischbachau, near Munich, Germany.

2011

Higher-order Subtyping for Dependent Types: 24 November 2011, Theory Seminar, Institute of Cybernetics, Tallinn, Estonia.
Similar talk given 11 November 2011 in the TCS Oberseminar, LMU Munich.
Towards a Dependently Typed Core Language: 14 September 2011, Shonan Meeting Seminar 007, Dependently Typed Programming, Shonan Village Center, near Tokyo, Japan.
On Shape Irrelevance and Polymorphism in Type Theory: 9 September 2011, Shonan Meeting Seminar 008, 14th Agda Implementor's Meeting (AIM XIV), Shonan Village Center, near Tokyo, Japan.
Higher-Order Pattern Unification for Dependently Typed Records: 1 June 2011, TLCA 2011, 10th International Conference on Typed Lambda Calculi and Applications, RDP 2011, Novi Sad, Serbia.
Similar talk given on 6 April 2011 at AIM XIII, the 13th Agda Implementors' Meeting, Chalmers University of Technology, Göteborg, Sweden.
Further, on 13 May 2011 in the TCS Oberseminar, Ludwig-Maximilians-University Munich.
Finally, on 28 June 2011 in the INRIA PI.R2 project, Paris, France.
Irrelevance in Type Theory: 28 March 2011, 14th International Conference on Foundations of Software Science and Computation Structures FoSSaCS 2011, part of European Joint Conferences on Theory and Practice of Software ETAPS 2011.
Similar talk given on 21 March 2011 in the Logic and Computation Seminar, McGill University, Montreal, Canada.
MiniAgda: Checking Termination using Sized Types: 14 March 2011, Logic and Computation Seminar, McGill University, Montreal, Canada.
Algorithmic Equality for the Calculus of Constructions: 14 February 2011, Two days on Models of the Calculus of Constructions, INRIA pi.r2, Paris, France.

2010

Irrelevance in Type Theory: 17 December 2010, TCS Oberseminar, Ludwig-Maximilians-University Munich.
MiniAgda: Towards a Core Language for Agda: 2 September 2010, 12th Agda Implementers' Meeing (AIM XII), Nottingham, UK.
Integrating Sized and Dependent Types: 15 July 2010, Workshop on Partiality and Recursion in Interactive Theorem Provers, PAR-10, Federated Logic Conference, FLoC 2010, Edinburgh, UK.
Explicit substitutions for contextual type theory: 14 July 2010, Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP 2010, Federated Logic Conference, FLoC 2010, Edinburgh, UK.
Parametric Dependent Function Types: 9 July 2010, Workshop on Dependently Typed Programming, DTP 2010 (slides), Federated Logic Conference, FLoC 2010, Edinburgh, UK.
MiniAgda: Termination Checking using Sized Types: 7 May 2010, TCS Oberseminar, Department of Computer Science, LMU Munich.
Normalization by Evaluation for the βη-Calculus of Constructions: 19 April 2010, 10th Int. Symp. on Functional and Logic Programming, FLOPS 2010, Sendai, Japan.
Towards Proof Irrelevant Equality Types in Martin-Löf Type Theory: 14 April 2010, NII Logic Seminar, National Institute for Informatics, Tokyo, Japan.
Typed and Untyped Normalization by Evaluation: 7 April 2010, Seminar of Advanced Industrial Science and Technology, AIST, Amagasaki (Osaka), Kansai, Japan.
Type-Based Termination for Dependent Types: 19 March 2010. ProVal Seminar, INRIA Saclay, Parc Orsay Universite, Paris, France.
Normalization by Evaluation for System F: 12 February 2010, Logic Seminar, LAMA, Universite de Savoie, Chambery, France.
Similar talk given on 9 March 2010, CORIAS Project Meeting, Hotel La Residence, Val d'Ajol, Vosges, France.
On Irrelevance and Extraction in Type Theory: 2 Februar 2010. Coq-Day on Equality and Termination, La Ciotat, Marseille, France.
Similar talk given on 24 March 2010, Agda Implementors' Meeting, AIM XI, Yumebutai Conference Center, Awaji Island, Japan.

2009

Remarks on Typed Equality for the Calculus of Constructions: 12 November 2009. Groupe de Travail Types and Semantics, INRIA PI.R2 and PPS, Paris, France.
Normalization by Evaluation for the Calculus of Constructions: 15 October 2009. PPS Lab, Universite Paris VII, France.
13 May 2009. International Workshop on Types for Proofs and Programs, TYPES 2009, Aussois, France.
Extensions to Definitional Equality in Agda. Or: Making Agda See More: 15 September 2009. 10th Agda Implementors' Meeting, Gothenburg, Sweden.
Type Structures and Normalization by Evaluation for System F^ω: 8 September 2009. Computer Science Logic, CSL'09, Coimbra, Portugal.
Extensional Normalization in the Logical Framework with Proof Irrelevant Equality: 15 August 2009. LiCS-affiliated Workshop on Normalization by Evaluation, NBE 2009, Los Angeles, USA.
(Attendance only): Epistemological and Ontological Aspects, a conference dedicated to Per Martin-Löf on the occasion of his retirement.
Swedish Collegium for Advanced Study, Uppsala, May 5-8, 2009.
Announcement
Normalization by Evaluation for System F: 6 April 2009. Computer Science Theory Seminar, Institute of Cybernetics Tallinn, Estonia.
30 January 2009. Copenhagen Programming Language Seminar, ITU Copenhagen, Denmark.
15 January 2009. Minisymposium on Type Theory and Foundations, Uppsala University, Sweden.

2008

Sized Types in Agda: 28 November 2008. Agda Intensive Meeting (AIM 9), Sendai, Japan.
Normalization by Evaluation for System F: 19 December 2008. TCS Seminar, Department of Computer Science, Ludwigs-Maximilians-University Munich.
5 December 2008. National Institute for Informatics (NII), Tokyo, Japan.
26 November 2008. 15th International Conference on Logics for Programming, Artificial Intelligence, and Reasoning LPAR'08, Doha, Qatar.
A more technical version of this talk:
3 September 2008. Programming Logics Group, Department of Computer Science, Chalmers University of Technology, Göteborg, Sweden.
Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory: 18 July 2008. 9th International Conference on Mathematics of Program Construction MPC'08, Marseille, France.
Normalization by Evaluation for Martin-Löf Type Theory: 27 March 2008. International Workshop on Types for Proofs and Programs, TYPES 2008, Torino, Italy. (Same talk given at LICS'07).
Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory: 19 February 2008. International Workshop on Dependently Typed Programming, DTP'08, Nottingham, UK.

2007

Type-Based Termination of Functional Programs: 11 October 2007. Kolloquium Programmiersprachen und Grundlagen der Programmierung, KPS'07, Timmendorfer Strand, Germany.
Normalization by Evaluation for Martin-Löf Type Theory with Typed Equality Judgements: 10 July 2007. Logic in Computer Science, LiCS 2007, Wroclaw, Poland.
(Similar talk given 6 July in the TCS Seminar, LMU Munich.)
Strong Normalization for Equi-(Co)inductive Types: 27 June 2007. International Conference on Typed Lambda Calculi and Applications, TLCA 2007, Paris, France.
Syntactical Strong Normalization for Intersection Types with Term Rewriting Rules: 25 June 2007. International Workshop on Higher-Order Rewriting, HOR 2007, Paris, France.
Strong Normalization for Equi-(Co)inductive Types: 2 May 2007. International Workshop on Types for Proofs and Programs, TYPES 2007, Cividale, Udine, Friuli, Italy.
Syntactical Normalization Proofs: 14 March 2007. Programming Logics Group, Department of Computer Science, Chalmers University of Technology, Göteborg, Sweden.
Type-Based Termination: 9 March 2007. Copenhagen Programming Language Seminar, ITU, Copenhagen, Denmark.
Normalization by Evaluation and Dependent Types: 27 February 2007. Protheo Seminar, LORIA, Nancy, France.

2006

Semantical Type-Checking Normalization by Evaluation Techniques and Abstract Values

December 19, 2006. TYPES Workshop Curry-Howard Implementation Techniques - Connecting Humans And Theorem provers CHIT-CHAT, Radboud University, Nijmegen, The Netherlands.
.pdf .ps.gz .dvi

Normalization by Evaluation for Martin-Löf Type Theory with One Universe

December 7, 2006. Arbeitstreffen Bern-München, Department of Mathematics, University of Munich.
.pdf .ps.gz .dvi

Normalization by Evaluation for Martin-Löf Type Theory with One Universe

November 17, 2006. TCS Seminar, Department of Computer Science, University of Munich.

Semi-continuous Sized Types and Termination

September 26, 2006. 15th Annual Conference of the EACSL, Computer Science Logic, CSL '06, Szeged, Hungary, September 25-29, 2006.
.pdf .ps.gz .dvi

A Polymorphic Lambda-Calculus with Sized Higher-Order Types

July 14, 2006. Thesis Defense. Department of Computer Science, University of Munich.

Towards Generic Programming with Sized Types

July 3, 2006. 8th International Conference on Mathematics of Program Construction, MPC '06, Kuressaare, Estonia, July 3-5, 2006.
.pdf .ps.gz .dvi

Implementing a Normalizer Using Sized Heterogeneous Types

July 2, 2006. Workshop on Mathematically Structured Functional Programming, MSFP 06, Kuressaare, Estonia.
.pdf .ps.gz .dvi

Polarized Subtyping for Sized Types

June 10, 2006. First International Computer Science Symposium in Russia (CSR 06), St. Petersburg, Russia, June 8-12, 2006
.pdf .ps.gz .dvi

Higher-Order Subtyping, Revisited

May 29, 2006. Mathematical Logic Seminar, University of Munich.

A Structurally Recursive Normalizer for Simply-Typed Lambda-Terms

April 28, Functional Programming Lunch, Nottingham University, UK.

Higher-Order Subtyping, Revisited Syntactic Completeness Proofs for Algorithmic Judgements

April 21, 2006. TYPES Workshop, Nottingham, UK.
.pdf .ps.gz .dvi

Sized (Co-)Inductive Types With Applications to Generic Programming

April 5, 2006. Programming Logics Group, Department of Computer Science, Chalmers University of Technology, Göteborg, Sweden.
.pdf .ps.gz .dvi

2005

Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs: December 8, 2005. Arbeitstreffen Bern-München, Institut für Mathematik, Universität München.
.pdf .ps.gz .dvi
Verifying Haskell Programs Using Constructive Type Theory: September 30, 2005. Haskell Workshop 2005, Tallinn, Estonia.
.pdf .ps.gz .dvi
Termination of Functions that Are Passed to their Arguments: September 13, 2005. APPSEM II Workshop 2005, Frauenchiemsee, Munich, Germany.
.pdf .ps.gz .dvi
Type-Based Termination and Productivity Checking: July 19, 2005. TCS Seminary, Department of Computer Science, Ludwigs-Maximilians-University Munich.
A more technical talk on the same subject has been given on June 17, same location.
.pdf .ps.gz .dvi
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs: May 11, 2005. Programming Logics Group, Department of Computer Science, Chalmers University of Technology, Göteborg, Sweden.
.pdf .ps.gz .dvi
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs: April 21, 2005. Typed Lambda Calculi and Applications (TLCA'05), Nara, Japan.
.pdf .ps.gz .dvi

2004

Fixed Points of Type Constructors and Primitive Recursion: September 21, 2004. Computer Science Logic (CSL'04), Karpacz, Poland.
.pdf .ps.gz .dvi
Weak Normalization for the Simply-Typed Lambda-Calculus in Twelf: July 5, 2004. Workshop on Logical Frameworks and Metalanguages (LFM'04), IJCAR 2004, Cork, Ireland.
.pdf .ps.gz .dvi
Similar talk: June 9, 2004. Programming Logics Group, Department of Computer Science, Chalmers University of Technology, Göteborg, Sweden.
.pdf .ps.gz .dvi
Sized Higher-Order Datatypes: April 15, 2004. 2nd APPSEM II Workshop, Tallinn, Estonia.
April 5, 2004. Spring School "Logic in Computer Science", Venice International University, Italy.
Sized Nested Datatypes: January 21, 2004. CoVer Project Seminar, Chalmers University of Technology, Göteborg, Sweden.
See December 12, 2003.

2003

Sized Nested Datatypes: December 12, 2003. Arbeitstreffen Bern München, Munich.
Termination and Guardedness Checking with Continuous Types: June 11, 2003. TLCA, Valencia, Spain.
.pdf .ps.gz
Termination and Guardedness Checking with Continuous Types Towards a Higher-Order Polymorphic Lambda-Calculus With Sized Types: May 30, 2003. Graduiertenkolleg Logik in der Informatik (GKLI), LMU München.
.pdf .ps.gz
Generalized Iteration and Coiteration for Higher-Order Nested Datatypes: April 8, 2003. FoSSaCS, ETAPS, Warsaw, Poland.
.pdf .ps.gz
A Higher-Order Polymorphic Lambda-Calculus With Sized Types: March 28, 2003. First APPSEM II Workshop, Nottingham, UK.
.pdf .ps.gz

2002

Generalized Iteration and Coiteration for Higher-Order Nested Datatypes: December 13, 2002. Arbeitstreffen Bern-München, LMU München.
Generalized Iteration and Coiteration for Higher-Order Nested Datatypes: November 14, 2002, Workshop on Termination and Type Theory, Hindås, Göteborg, Sweden.
.pdf .ps.gz
Selected Talks of PLI'02: November 8, 2002, Seminar on Theoretical Computer Science, Munich.
Generalized Iteration for Higher-Order Nested Datatypes: October 31, 2002, Seminar on Mathematical Logic, Munich.
Termination and Guardedness Checking with Continuous Types Yet Another Approach to General Recursion: April 26, 2002, TYPES 2002 Workshop, Berg en Dal, Nijmegen, Netherlands.
.pdf .ps.gz
Termination and Guardedness Checking with Continuous Types: February 12, 2002, Gemeinsamer Workshop der DFG Graduiertenkollegs 301 und 334, Gohrisch (near Dresden).

2001

TUTCH - A Proof Checker for Teaching Intutionistic Logics: December 13, 2001, Arbeitstreffen Bern-München, LMU München. Talk announced under the title "What if Jesus is right?".
Termination and Guardedness Checking with Types: December 7, 2001, Type-Club, Munich.
Termination Checking = Type Checking: August 03, 2001, International Summer School Marktoberdorf
Termination Checking with Types: June 27, 2001, Arbeitstreffen Bern-München, IAM Berne.
A Third-Order Representation of the λμ-Calculus: June 18, 2001, Workshop MERLIN 2001, IJCAR, Siena.
A Third-Order Representation of the λμ-Calculus: May 4, 2001, Graduiertenkolleg Logik in der Informatik (GKLI), LMU München.
A Third-Order Representation of the λμ-Calculus: March 13 and 20, 2001, Seminar of Automated Reasoning, CMU Computer Science, Pittsburgh.
An introduction to the λμ-calculus is available.

2000

Termination of Mutually Recursive Functions: May 26, 2000, Principles Of Programming Seminar, CMU Computer Science, Pittsburgh.
.pdf .ps.gz .dvi
Termination of Mutually Recursive Functions with Several Arguments by Lexicographic Orderings: April 6, 2000, Arbeitstreffen Bern-München, IAM Berne.
.pdf .ps.gz .dvi

1999

Specification and Verification of a Formal System for Non-mutual Structural Recursion: December 17, 1999, Type Club, LMU München.
.pdf .ps.gz .dvi
A Predicative Analysis of Structural Recursion: November 19, 1999, Graduiertenkolleg Logik in der Informatik (GKLI), LMU München.
.pdf .ps.gz .dvi
Strong Normalization for the Heyting Arithmetic with Inductive Types: November 12 and December 3, Seminar Selected Topics regarding Lambda Calculus and Type Theory, LMU München.
A Predicative(?) Analysis of Structural Recursion: June 15, 1999, Third Annual Meeting of the TYPES Working Group, Lökeberg, Sweden.
A Semantic Analysis of Structural Recursion: May 10, 1999, Fourth International Workshop on Termination (WST 99), Dagstuhl, Germany.
.pdf .ps.gz .dvi
A Semantic Analysis of Structural Recursion: February 26, 1999, Diploma thesis defence at the Type Club, LMU München.
.pdf .ps.gz .dvi

1998 and before

foetus - Termination Checker for Simple Functional Programs: June 15, 1998, Type Club, LMU München.
Integer Division in NC (Division nach Beame, Cook & Hoover): November 19, 1996, Seminar on Complexity Theory, LMU München.