
Talks
Last update: 16 July 2019.
 Normalization by Evaluation for CallByPushValue
 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
 CorrectByConstruction 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 ProofRelevant Relations and EvidenceAware 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, 2125 May 2018.
 On the Syntax and Semantics of Quantitative Type Theory
 19 April 2018,
Workshop
on Mixed InductiveCoinductive 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' nonpublic 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
38 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)
BolzanoBozen, South Tyrol, Italy, 1526 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, LudwigMaximiliansUniversitä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 HighLevel and LowLevel 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 GIconference
Software Engineering 2014,
ChristianAlbrechtsUniversität Kiel, Germany.
Abstract
published in CEUR SEWS 2014.
 Productive Infinite Objects via Copatterns and Sized Types in Agda
 30 January 2014,
Representing Streams II,
LorentzCenter, 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, LudwigMaximiliansUniversity 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
LambdaCalculus II: Semantic Methods
 6 Dec 2012, Lecture given for the
Logic and Computation Group,
McGill University, Montreal, Canada.
 Strong Normalization for
LambdaCalculus 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,
FriedrichAlexanderUniversität Erlangen.
Agda code
Similar talk given at the PUMA/RISE Workshop, Goldegg, Austria, 27 September 2012.
 TypeBased Termination,
Inflationary FixedPoints, and
Mixed InductiveCoinductive 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 InductiveCoinductive Types
 22 February 2012,
15th Agda Implementor's Meeting,
AIM XV,
Fischbachau, near Munich, Germany.
2011
 Higherorder 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.
 HigherOrder 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, LudwigMaximiliansUniversity 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, LudwigMaximiliansUniversity 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, PAR10,
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 MartinLö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.
 TypeBased 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. CoqDay 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. LiCSaffiliated Workshop on Normalization by Evaluation, NBE 2009, Los Angeles, USA.
 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, LudwigsMaximiliansUniversity 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 MartinLöf Type Theory
 18 July 2008. 9th International Conference on Mathematics of Program Construction MPC'08, Marseille, France.
 Normalization by Evaluation for
MartinLö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 MartinLöf Type Theory
 19 February 2008. International Workshop on Dependently Typed Programming,
DTP'08, Nottingham, UK.
2007
 TypeBased Termination of Functional Programs
 11 October 2007. Kolloquium Programmiersprachen und Grundlagen der Programmierung, KPS'07, Timmendorfer Strand, Germany.
 Normalization by Evaluation for
MartinLö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 HigherOrder 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.
 TypeBased 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 TypeChecking
Normalization by Evaluation Techniques and Abstract Values
 December 19, 2006. TYPES Workshop CurryHoward Implementation Techniques  Connecting Humans And Theorem provers CHITCHAT, Radboud University, Nijmegen, The Netherlands.
.pdf
.ps.gz
.dvi
 Normalization by Evaluation for MartinLöf Type Theory with One Universe
 December 7, 2006. Arbeitstreffen BernMünchen, Department of Mathematics, University of Munich.
.pdf
.ps.gz
.dvi
 Normalization by Evaluation for MartinLöf Type Theory with One Universe
 November 17, 2006. TCS Seminar, Department of Computer Science, University of Munich.
 Semicontinuous Sized Types and Termination
 September 26, 2006. 15th Annual Conference of the EACSL, Computer Science Logic, CSL '06, Szeged, Hungary, September 2529, 2006.
.pdf
.ps.gz
.dvi
 A Polymorphic LambdaCalculus with Sized HigherOrder 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 35, 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 812, 2006
.pdf
.ps.gz
.dvi
 HigherOrder Subtyping, Revisited
 May 29, 2006. Mathematical Logic Seminar, University of Munich.
 A Structurally Recursive Normalizer for SimplyTyped LambdaTerms
 April 28, Functional Programming Lunch, Nottingham University, UK.
 HigherOrder 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 MartinLöf's Logical Framework with Surjective Pairs
 December 8, 2005. Arbeitstreffen BernMü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
 TypeBased Termination and Productivity Checking
 July 19, 2005. TCS Seminary, Department of Computer Science, LudwigsMaximiliansUniversity 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 MartinLö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 MartinLö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 SimplyTyped LambdaCalculus 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 HigherOrder 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 HigherOrder Polymorphic LambdaCalculus With Sized Types

May 30, 2003. Graduiertenkolleg Logik in der Informatik
(GKLI),
LMU München.
.pdf
.ps.gz
 Generalized Iteration and Coiteration for HigherOrder Nested Datatypes

April 8, 2003. FoSSaCS, ETAPS, Warsaw, Poland.
.pdf
.ps.gz
 A HigherOrder Polymorphic LambdaCalculus With Sized Types

March 28, 2003. First
APPSEM II Workshop, Nottingham, UK.
.pdf
.ps.gz
2002
 Generalized Iteration and Coiteration for HigherOrder Nested Datatypes

December 13, 2002. Arbeitstreffen BernMünchen, LMU München.
 Generalized Iteration and Coiteration for HigherOrder 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 HigherOrder 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 BernMünchen, LMU München. Talk
announced under the title "What if Jesus is right?".

Termination and Guardedness Checking with Types

December 7, 2001, TypeClub, Munich.

Termination Checking = Type Checking

August 03, 2001, International Summer School Marktoberdorf

Termination Checking with Types

June 27, 2001, Arbeitstreffen BernMünchen,
IAM Berne.
 A ThirdOrder Representation of the λμCalculus

June 18, 2001, Workshop MERLIN 2001, IJCAR, Siena.

A ThirdOrder Representation of the λμCalculus

May 4, 2001, Graduiertenkolleg Logik in der Informatik
(GKLI),
LMU München.

A ThirdOrder 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 BernMünchen,
IAM Berne.
.pdf
.ps.gz
.dvi
1999

Specification and Verification of a Formal System
for Nonmutual 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.
[ Home
 CV
 Professional Service
 Projects
 Publications
 Talks
 Teaching
 Supervision
]
