Talks by Ralph Matthes

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

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

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)