Talks by Ralph Matthes

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

Invited talks in 2019

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)

Talks at events where I came by invitation in 2018

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)

Talks in 2014-2017

ought to be put here some time in the future

Talks in 2013

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)

Talks in 2012

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)

Talks in 2011

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

Talks in 2010

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

Talks in 2009

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

Talks in 2008

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

Talks in 2007

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)

Talks in 2006

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

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

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

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 (Workshop Fixed Points in Computer Science)
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). Slides in German language are available

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