- February 4 in Munich (Colloquium of the GKLI)
- Higher-Order Inductive Types - 4 Years Later
- March 25 in Oberwolfach (Workshop "Mathematical Logic: Proof Theory, Type Theory and Constructive Mathematics")
- Monadic Stabilization for Operationalized Second-Order Classical Logic with Disjunction and Permutative Conversions
- May 16 in Toulouse (IRIT = Institut de Recherche en Informatique de Toulouse)
- Types Inductifs au-delà de la Stricte Positivité (inductive types beyond strict positivity)
- May 19 in Munich (12. Jahrestagung der GI-Fachgruppe "Logik in der Informatik")
- Explicit and not so explicit substitution - a case study in nested data types

- April 5 and April 6 in Venice (Spring School "Logic in Computer Science")
- Higher datatypes and XML (Tutorial, 4 hours)
- September 16 in Dagstuhl (Seminar on Dependently Typed Programming)
- Towards iteration for truly nested datatypes
- December 13 in Jouy en Josas (near Paris, TYPES 2004)
- Truly nested datatypes through dependent datatypes - a challenge for Coq

- March 20 in Chambéry (Séminaire de logique)
- Generalized (co-)iteration versus primitive (co-)recursion for nested datatypes
- March 26 in Edinburgh (Proof Theory and Algorithms)
- Programs with nested datatypes from proofs
- April 12 in Warsaw (FICS03)
- Primitive recursion for rank-2 inductive types
- April 17 in Munich
- Remarks on lambda-mu-calculus
- April 30 in Torino (TYPES 2003)
- Specification and verification of programs with nested datatypes: Illuminating examples
- August 17 in Helsinki (Logic Colloquium 2003)
- Inductive constructions for classical natural deduction
- October 23 in Munich
- Remark on polarized kinds
- November 21 and November 28 in Munich (Colloquium of the GKLI)
- Lambda calculi for classical logic within intuitionistic logic
- December 12 in Munich (Arbeitstagung Bern - München)
- What is a syntactically monotone lambda term?

- January 10 in Munich
- Lyndon Interpolation for Intuitionistic Propositional Logic: Schütte vs. Pitts
- February 13 in Kurort Gohrisch/Dresden (Joint Workshop of Graduiertenkolleg 301 and Graduiertenkolleg 334)
- Recursion and Corecursion for Nested Datatypes
- February 21 in Luminy/Marseille (Logic and Interaction Weeks)
- Coinductive Datatypes for Non-Wellfounded Syntax with Variable Binding
- March 18 in Tallinn (Institute of Cybernetics of the Technical University of Tallinn)
- Contraction-Aware Lambda-Calculus
- April 9 in Oberwolfach (Meeting Mathematische Logik)
- Contraction-Aware Lambda-Calculus
- April 11 in Oberwolfach
- Contraction-Aware Lambda-Calculus - Examples and Discussion
- April 24 in Berg en Dal/Nijmegen (TYPES 2002)
- On (Co-)Iteration of Rank 2
- May 30 in Bourget du Lac/Chambéry (Séminaire de logique de LAMA)
- Short proofs of normalization for simply-typed lambda-calculus and Gödel's system T
- June 10 in Berne (Arbeitstagung Bern - München)
- A New Approach to Uniform Interpolation?
- June 13 in Paris (Séminaire PPS)
- Contraction-Aware Lambda-Calculus
- June 20 in Toulouse (IRIT=Institut de Recherche en Informatique de Toulouse)
- Intensional Aspects of Coinductive Syntax
- July 5 in Orsay/Paris (LRI=Laboratoire de Recherche en Informatique)
- Substitution for Non-Wellfounded Terms with Variable Binding
- November 7 in Munich
- Remarks on Mendler-style in all finite ranks
- November 15 in Hindås/Göteborg (Workshop in Termination and Type Theory)
- Strong Normalization for Nested (Co-)Recursion

- January 12 in Munich
- Chris Okasaki's adventure in types
- May 4 in Cracow (=Kraków in Polish; TLCA 2001)
- Parigot's second order lambda-mu-calculus and inductive types
- May 25 in Munich (Colloquium of the GKLI)
- Monotone Inductive and Coinductive Constructors of Rank 2
- June 26 in Berne (Arbeitstagung Bern - München)
- Datatypes for Complex Term Trees
- September 13 in Paris (CSL '01)
- Monotone Inductive and Coinductive Constructors of Rank 2
- October 11 in Dagstuhl (Proof Theory in Computer Science)
- A refinement of interpolation for natural deduction
- October 25 in Munich
- A lambda calculus for the study of contraction-free sequent calculus
- November 15 in Munich
- The contraction-free lambda-calculus LambdaJT
- December 13 in Munich (Arbeitstagung Bern - München)
- Contraction-aware lambda-calculus

- January 14 in Munich (Colloquium of the GKLI)
- Standardization for lambda calculus with generalized applications
- January 18 and January 25 in Munich
- Lambda calculus with recursion on hierarchical and simultaneous strictly positive inductive structures
- March 14 in Munich
- Towards a characterization of the strongly normalizing terms of LambdaJ via strict intersection types
- April 6 in Berne (Arbeitstagung Bern - München)
- Permutative conversions and intersection types (Slides in German including an abstract written in English, use orientation swap landscape when viewing with ghostview)
- July 12 in Norwich (RTA 2000)
- Standardization and confluence for a lambda calculus with generalized applications (joint work with Felix Joachimski)
- July 15 in Geneva (=Genève in French; ITRS '00)
- Characterizing Strongly Normalizing Terms of a Lambda-Calculus with Generalized Applications via Intersection Types
- August 3 in Munich
- An application of the SN method to stability reductions
- August 7-18 in Birmingham (ESSLLI 2000)
- Lambda Calculus: A Case for Inductive Definitions
- October 5 in Paris (Seminaire Preuves, Programmes et Systèmes)
- Parigot's lambda-mu-calculus and inductive types
- October 20 and November 3 in Munich
- Parigot's lambda-mu-calculus and inductive types
- November 13 in Tübingen (Kolloquium Logik und Sprachtheorie)
- Operationalization of proofs by contradiction via and with induction
- November 24 in Munich
- Hereditarily monotone inductive constructors of finite kind
- December 11 in Durham (TYPES 2000)
- Monotone (co-)inductive constructors of finite kind
- December 22 in Munich (Arbeitstagung Bern - München)
- Higher-order extensions of monotone (co-)inductive types

- February 2 in Munich
- Monotone inductive types (thesis defense)
- February 9 in Munich
- Another proof of strong normalisation for permutative conversions
- May 8 in Berlin (Research Colloquium Foundations of the Formal Sciences)
- Tarski's fixed-point theorem and higher-order term rewrite systems (Slides in German including an abstract written in English, use orientation swap landscape when viewing with ghostview)
- May 25 in Munich
- Confluence for untyped lambda calculus with omega rule and permutative conversions
- June 2 in Berne (Arbeitstagung Bern - München)
- A new extensional reduction rule for sum types as a challenge for proofs of normalisation
- September 6 in Mainz (DMV-Tagung 1999)
- Monotone inductive types (Slides in German; even two pages on one)
- September 28, October 12 and 16 in Munich
- Term systems for natural deduction with general eliminations

- January 8 in Munich
- Proof of strong normalization for permutative conversions for sum types
- January 21 in Oberwolfach (Meeting on Mathematical Logic)
- Lambda Calculi with Monotone Inductive Types
- January 22 in Oberwolfach
- Two very easy proofs of normalization of simply typed lambda-calculus using inductive definitions
- January 30 in Munich
- A MODULAR proof of strong normalization for permutative conversions in lambda calculus
- March 28 in Irsee (TYPES 98)
- Full primitive recursion on monotone inductive types (Slides (DVI), without colours (DVI))
- May 4 in Munich
- Monotone fixed-point types and strong normalization
- June 24 in Berne (Arbeitstagung Bern - München)
- Standardization and permutative conversions (Slides in German, use orientation swap landscape when viewing with ghostview)
- August 10 in Prague (Logic Colloquium '98)
- Functoriality of monotonicity witnesses in the system of positive (interleaved) inductive types (submitted abstract)
- August 27 in Brno (CSL '98)
- Monotone Fixed-Point Types And Strong Normalization (Slides - use orientation swap landscape when viewing with ghostview)
- August 28 in Brno (FICS '98)
- Monotone (Co)Inductive Types and Positive Fixed-Point Types
- September 21 in Munich
- Standardisation
- November 13 in Munich
- Short proofs of normalization for the simply-typed lambda-calculus, permutative conversions and Gödel's T
- November 17 in Munich
- A lack of duality of the embeddings of monotone inductive and monotone coinductive types into non-interleaving positive fixed-point types

- April 2 in Berne (Arbeitstagung Bern - München)
- Relating iteration and primitive recursion in the system of positive inductive types (on the difficulties which arise with `map' and `comap' when trying to define the predecessor function)
- October 16 in Munich
- Permutative conversions and variable elimination conversions for sum types
- October 23 in Munich
- Definition of permutative conversions for interleaved inductive types
- December 18 in Munich (Arbeitstagung Bern - München)
- Lambda calculi with monotone inductive types

- December 19 in Munich (Arbeitstagung Bern - München)
- Naïve reduction-free normalization (proofs of strong normalization without analysis of reducts and without making use of category theory, here: an extension of Mendler's system)

Ralph Matthes Last modified: Fri May 20 13:47:30 CEST 2005