Talks

Last update: 12 November 2009.

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.
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 Seminary, 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.

abel@informatik.uni-muenchen.de
http://www.tcs.informatik.uni-muenchen.de/~abel