- March 11 in Nancy, France (Third Workshop on Mathematical Logic and its Applications - MLA 2019, Loria)
- Finiteness properties of simple types through a coinductive lambda-calculus
- September 12 in Swansea, United Kingdom (2nd Workshop on Proof Theory and its Applications, The Proof Society, Department of Computer Science, Univ. of Swansea)
- Martin Hofmann's case for non-strictly positive data types - reloaded - this is the version augmented by Anton Setzer for the sake of presenting it (original version)

- January 24 in Nijmegen, The Netherlands (EUTypes 2018 Working Meeting, Radboud University, Nijmegen)
- Intensional and univalent aspects of rule-based programming
- June 20 in Braga, Portugal (Types Conference 2018, University of Minho, Braga)
- Martin Hofmann's case for non-strictly positive data types (organizers' version)

- September 1st in Torino, Italy (FICS 2013, 9th International Workshop on Fixed Points in Computer Science)
- A coinductive approach to proof search
- November 7 in Palaiseau, France (LIX Colloquium 2013: Theory and Application of Formal Proofs)
- A classical theory of values and computations
- November 8 in Palaiseau, France (PSATTT 2013, International Workshop on Proof-Search in Axiomatic Theories and Type Theories)
- A coinductive approach to proof search (with quite some new material w.r.t. the FICS talk)

- February 28 in Grenoble (Kickoff of Climt project ANR-11-BS02-016)
- Coinduction and all that
- April 1 in Tallinn, Estonia (CMCS'12)
- Permutations in coinductive graph representation
- May 11 in Braga, Portugal (Seminar "Algebra, Logic and Computation")
- Varieties of Polymorphism
- May 21 and June 4 in Toulouse (course of 4 hours for PhD students at the PhD school on Mathematics, Informatics and Telecommunication in Toulouse)
- Polymorphism (in English! - 33 "real" slides + lots of overhead available on request for the first two hours)

- September 9 in Toulouse
- Magic formulas in intuitionistic propositional logic with quantification over propositions - a presentation of a result of Tatsuta, Fujita, Hasegawa and Nakano

- November 17 in Paris (16èmes Rencontres LAC)
- Intensional equality for a truly nested datatype

- February 5 in Braga (Seminar in Algebra and Logics of the Centre of Mathematics of the University of Minho)
- Category theory on a computer - the example of the Coq system
- March 16 in Lyon (Journées GEOCAL-LAC at ENS Lyon)
- Monadic translation of intuitionistic and classical sequent calculus
- May 19 in Toulouse (Séminaire vérification de Toulouse)
- Translation in continuation-passing style, its variants, and its generalisation to monads
- October 20 in Paris (seminar "Sémantique et Réalisabilité" of PPS)
- Strict Simulation of CBN Lambda-bar-mu-mu-tilde in Simply-Typed Lambda Calculus
- October 21 in Créteil near Paris (Second meeting of the working group LTP of the "groupement de recherche" GPL at University of Paris 12)
- A Truly Nested Inductive Equivalence for Lambda Calculus with Explicit Flattening
- November 3 in Toulouse (Séminaire vérification de Toulouse)
- Strict Simulation of a Lambda Calculus for Classical Logic in Simply-Typed Lambda Calculus

- February 19 in Nottingham (Dependently Typed Programming 2008)
- Programming with nested datatypes through dependent types
- March 27 in Torino (TYPES 2008)
- A representation of untyped lambda-calculus with explicit flattening through a nested datatype
- April 11 in Oberwolfach (Seminar "Mathematical Logic: Proof Theory, Constructive Mathematics")
- Programming with and reasoning about a monad of lambda terms that has explicit monad multiplication
- May 5 and May 19 in Toulouse
- The monadic approach to functional programming
- May 26 and 27 in Tallinn (Software Department of the Institute of Cybernetics)
- Monads for programming and verification, a small course of 6 hours for PhD students
- June 18 in Athens (invited speaker to special session "Higher-Type Recursion and Applications" at the conference CiE 2008)
- Recursion on Nested Datatypes in Dependent Type Theory
- July 16 in Marseille (conference MPC '08)
- Nested datatypes with generalized Mendler iteration: map fusion and the example of the representation of untyped lambda calculus with explicit flattening
- November 28 in Évry near Paris (Workshop Langages, Types et Preuves of GdR GPL in ENSIEE)
- Verification of redecoration for infinite triangular matrices in Coq

- February 8 in Chambéry (GdT LAC du GdR IM)
- Verification of an algorithm that uses an inductive family of types
- May 3 in Cividale del Friuli (TYPES 2007)
- Verification of the redecoration algorithm for triangular matrices
- May 29 in Braga (Seminar in Algebra and Logics of the Centre of Mathematics of the University of Minho)
- Substitution - surprising challenges with inductive families
- June 23 in Munich (Workshop Proof and Computation II)
- Continuation-passing style and strong normalisation for sequent calculi
- June 26 in Paris (TLCA 2007)
- Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi
- July 6 in Chambéry (Séminaires de logique du LAMA)
- Substitution - surprising challenges with inductive families (same title as May 29, but only 50% overlapping)
- September 13 in Göteborg (Programming Logic Seminar)
- Verification of programs involving nested datatypes in intensional type theory
- September 14 in Göteborg
- Dependent Type Theory with Parameterized First-Order Data Types and Well-Founded Recursion - Opponent's Presentation of David Wahlstedt's PhD Thesis (PDF presentation)
- December 12 in Chambéry (Séminaires de l'équipe LIMD du LAMA)
- Substitution - surprising solutions with inductive families (the subtle change in the title shows that a substantial progress has been made after May 29)

- March 14 in Toulouse (FéRIA-SVF)
- Nested Datatypes: Programming and Verifying
- March 30 in Munich (invitation by the GKLI)
- Towards verifying terminating programs involving nested datatypes
- April 20 in Nottingham (TYPES 2006)
- Verification of Programs with Truly Nested Datatypes in Coq
- April 27 in Nottingham (SSDGP 2006)
- Generic definition and proof in intensional type theory of map fusion for nested datatypes
- June 1st in Paris (Colloquium of PPS in Paris VII)
- Program verification for nested datatypes in intensional type theory
- June 14 in Toulouse (EJCP '06)
- Category Theory for Software Engineering
- July 2nd in Kuressaare, Estonia (MSFP '06)
- Verification of programs on truly nested datatypes in intensional type theory
- July 3rd in Kuressaare, Estonia (MPC '06)
- A Datastructure for Iterated Powers
- October 6 in Toulouse
- Categories for software engineering I: colimits
- October 12 in Braga, Portugal (Seminar on Algebra and Logics of the Centre of Mathematics of the University of Minho)
- On the importance of normalization for typed rewrite systems
- December 1 in Toulouse
- Categories for software engineering II: CommUnity in practice

- 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
- October 28 in Toulouse (Second International Workshop on Isomorphisms of Types)
- Retracts for Inheritance of Strong Normalization in Typed Lambda-Calculus with Fixed Points

- 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 (Workshop on Proof Theory and Algorithms)
- Programs with nested datatypes from proofs
- April 12 in Warsaw (Workshop Fixed Points in Computer Science FICS'03)
- 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 (Workshop Fixed Points in Computer Science)
- 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). Slides in German language are available

Ralph Matthes Last modified (date in French): lun. févr. 3 18:22:19 CET 2020