Talks

Last update: 8 May 2012.

2012

Programming and Program Verification with Dependent Types in Agda: 8 May 2012, Seminar Lehrstuhl Theoretische Informatik, Friedrich-Alexander-Universität Erlangen.
Type-Based Termination, Inﬂationary 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.
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.

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