iBet uBet web content aggregator. Adding the entire web to your favor.
Link to original content: https://www.irit.fr/~Ralph.Matthes/
I have a permanent CNRS research position at IRIT (Institute for Computer Science of Toulouse), located on the campus of the Technical University Toulouse. My postal address is (the first line is essential with both ingredients!)
I am member of the research group ACADIE that is the common successor to SVF and ZENO. The French acronym stands for "Assistance with the Certification of Distributed and Embedded Applications".
As a CNRS researcher, I belong to Section 6 of the National Committee of Scientific Research (after splitting the former 7 into 6 and 7).
A recent photo: 
I am working in Theoretical Computer Science, but this could as well be called Foundations of Computer Science. Within theoretical computer science, I tend towards logic in computer science, semantics and theory of programming. My work resides at the interface between mathematics and computer science. I am strongly interested in computer formalization of my research results and thus in having automatically verifiable artefacts representing these results. This necessitates (and thus comprises) the computer formalization of mathematical structures, such as data types and their recursion schemes and, in general, the structures known from category theory. Still, for me, computer formalization of known mathematics is not an end in itself and only a prerequisite for formalization projects aiming at establishing new results.
My work is based on the following research topics: lambda calculus, proof theory, term rewriting, type theory, interactive theorem proving, coinductive methods, category theory - the latter in particular as a semantic framework for lambda-calculus, type theory and coinductive methods. Category theory had even long before inspired many notions in my analysis of recursion schemes, but in my current research, category theory is being employed.
My current main research efforts go into two directions:
In the past, I directed many of my publications towards uses of parametric polymorphism to guarantee the termination of inductive and coinductive recursion schemes for data types that could come as families and that could go beyond strictly positive data types - the latter made them unfeasible for the Coq theorem prover, but such schemes could still be formally justified by a shallow embedding into Coq (assuming impredicative Set). Coinductive methods played an important role for the representation of graphs and their transformations. Even earlier, I worked just on lambda-calculi and their foundational properties, in particular for extensions and variations that featured permutative/commuting conversions. My accent there was on the careful inductive definition of auxiliary concepts, so as to guarantee smooth proofs following that inductive structure. Permutative/commuting conversions are also a challenge to overcome in my (now old) work on continuation-passing style transformations.
A very important part of the research sketched here was obtained with collaborators. The research interests are mine, and they are being shown here.
12th Workshop Fixed Points in Computer Science 2024 (FICS 2024) on February 19 and 20 in Naples, Italy, a satellite of CSL 2024. I chaired the steering committee.
29th International Conference on Types for Proofs and Programs (TYPES 2023), 12-17 June 2023 in València, Spain. I was in the PC.
11th Workshop Fixed Points in Computer Science 2023 (FICS 2023) on February 17 in Warsaw, Poland, a satellite of CSL 2023. I chaired the steering committee and I was in the PC.
7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), August 2-8, 2022 in Haifa, Israel. I was in the PC.
School on Univalent Mathematics, July 17-23, 2022 in Cortona, Italy. I was one of the lecturers.
27th International Conference on Types for Proofs and Programs (TYPES 2021), 14 - 18 June 2021 virtually (online), hosted by Leiden University, The Netherlands. I was chair of the steering committee and I in the PC.
School and Workshop on Univalent Mathematics, July 27-31, 2020 in Cortona, Italy (cancelled because of the COVID-19 sanitary crisis). I would have been one of the lecturers/mentors.
26th International Conference on Types for Proofs and Programs (TYPES 2020), 2 - 5 March 2020 in Torino, Italy (cancelled only days before the conference because of the COVID-19 outbreak in Piedmont, with the whole programme already set up). I have chaired the steering committee, and I was in the PC.
18th Workshop Proof, Computation, Complexity 2019 (PCC 2019), July 15-19, 2019 in Djursholm close to Stockholm, Sweden at the Institut Mittag-Leffler. I was in the SC and co-organizer.
International Workshop Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'19), June 22, 2019 in Vancouver, Canada (affiliated with LICS 2019). I was in the PC.
25th International Conference on Types for Proofs and Programs (TYPES 2019), 11 - 14 June 2019 in Oslo, Norway. I have chaired the steering committee, and I was in the PC.
School and Workshop on Univalent Mathematics, April 1-5, 2019 in Birmingham, UK. I was one of the lecturers/mentors.
To see also older events, please refer to the full list.
Last modified (date in French): mer. août 28 17:04:21 CEST 2024