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
- 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). Slides in German language are available
Ralph Matthes
Last modified (date in French): lun. févr. 3 18:22:19 CET 2020
https://www.irit.fr/~Ralph.Matthes/talks.html