Talks by Ralph Matthes

Always the translations of the titles of the talks held in German are given.

Talks in 2005

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

Talks in 2004

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

Talks in 2003

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?

Talks in 2002

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

Talks in 2001

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

Talks in 2000

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

Talks in 1999

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

Talks in 1998

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
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

Selected talks in 1997

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

Selected talk in 1996

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