Publications de Ralph MATTHES
José Espírito Santo, Ralph Matthes, Luís Pinto
A Coinductive Approach to Proof Search through Typed Lambda-Calculi
Annals of Pure and Applied Logic, 2021, 172 (10), ⟨10.1016/j.apal.2021.103026⟩
José Espírito Santo, Ralph Matthes, Luís Pinto
Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search
Mathematical Structures in Computer Science, 2019, 29 (8), pp.1092-1124. ⟨10.1017/S0960129518000099⟩
Benedikt Ahrens, Ralph Matthes, Anders Mörtberg
From signatures to monads in UniMath
Journal of Automated Reasoning, 2019, 63 (2), pp.285-318. ⟨10.1007/s10817-018-9474-4⟩
José Espírito Santo, Ralph Matthes, Luís Pinto
Decidability of several concepts of finiteness for simple types
Fundamenta Informaticae, 2019, 170 (1-3), pp.111-138. ⟨10.3233/FI-2019-1857⟩
David Baelde, Arnaud Carayol, Ralph Matthes, Igor Walukiewicz
Preface : Fixed Points in Computer Science (FICS) 2013
Fundamenta Informaticae, 2017, 150 (3-4), pp.i-ii. ⟨10.3233/FI-2017-1468⟩
José Espírito Santo, Ralph Matthes, Koji Nakazawa, Luís Pinto
Monadic translation of classical sequent calculus
Dans : Mathematical Structures in Computer Science, Cambridge University Press, Vol. 23 N. 6, p. 1111-1162, décembre 2013.
Accès : http://dx.doi.org/10.1017/S0960129512000436 – https://oatao.univ-toulouse.fr/12342/
BibTeXPreface (to Sixth Workshop on Fixed Points in Computer Science, FICS 2009)
Dans : RAIRO – Theoretical Informatics and Applications, EDP Sciences, Numéro spécial Sixth Workshop on Fixed Points in Computer Science, FICS 2009, Vol. 47 N. 1, p. 1-2, décembre 2012.
Ralph Matthes, Sergei Soloviev
Preface to the special issue: commutativity of algebraic diagrams
Dans : Mathematical Structures in Computer Science, Cambridge University Press, Numéro spécial CAMCAD ’09 Commutativity of Algebraic Diagrams, Vol. 22 N. 6, p. 901-903, décembre 2012.
Coinductive Graph Representation : the Problem of Embedded Lists
Dans : Electronic Communications of the EASST (ECEASST), Electronic Communications of the EASST, Berlin – Germany, Numéro spécial Selected Revised Papers from the Third International Workshop on Graph Computation Models (GCM 2010), Vol. 39, (en ligne), septembre 2011.
Résumé Accès : http://journal.ub.tu-berlin.de/eceasst/article/view/649
BibTeXMap Fusion for Nested Datatypes in Intensional Type Theory
Dans : Science of Computer Programming, Elsevier, Vol. 76, p. 204-224, 2011.
Résumé Accès : http://dx.doi.org/10.1016/j.scico.2010.05.008
BibTeXJosé Espírito Santo, Ralph Matthes, Luís Pinto
Continuation-passing style and strong normalisation for intuitionistic sequent calculi
Dans : Logical Methods in Computer Science, Logical Methods in Computer Science, Germany, Vol. 5 N. 2, (en ligne), mai 2009.
Accès : http://www.lmcs-online.org/ojs/viewarticle.php?id=404&layout=abstract – http://arxiv.org/pdf/0903.1822
BibTeXAn induction principle for nested datatypes in intensional type theory
Dans : Journal of Functional Programming, Cambridge University Press, Vol. 19 N. 3&4, p. 439-468, juin 2009.
Résumé Accès : http://dx.doi.org/10.1017/S095679680900731X
BibTeXRalph Matthes, Sergei Soloviev
Preface to the special issue: isomorphisms of types and invertibility of lambda terms
Dans : Mathematical Structures in Computer Science, Cambridge University Press, Numéro spécial Isomorphisms of types and invertibility of lambda terms, Vol. 18, p. 645-646, août 2008.
Benedikt Ahrens, Ralph Matthes, Niels van der Weide, Kobe Wullaert
Displayed Monoidal Categories for the Semantics of Linear Logic
Certified Programs and Proofs (CPP 2024), Jan 2024, London, United Kingdom. à paraître, ⟨10.1145/3636501.3636956⟩
Benedikt Ahrens, Ralph Matthes, Anders Mörtberg
Implementing a Category-Theoretic Framework for Typed Abstract Syntax
11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2022), ACM SIGPLAN; ACM SIGLOG, Jan 2022, Philadelphia, United States. pp.307–323, ⟨10.1145/3497775.3503678⟩
Dominique Larchey-Wendling, Ralph Matthes
Certification of Breadth-First Algorithms by Extraction
13th International Conference on Mathematics of Program Construction, MPC 2019, Oct 2019, Porto, Portugal. pp.45-75, ⟨10.1007/978-3-030-33636-3_3⟩
José Espirito Santo, Ralph Matthes, Koji Nakazawa, Luis Pinto
Confluence for classical logic through the distinction between values and computations
5th International Workshop on Classical Logic and Computation (CL&C 2014), Jul 2014, Vienne, Austria. pp.63–77, ⟨10.4204/EPTCS.164.5⟩
José Espírito Santo, Ralph Matthes, Luís Pinto
A Coinductive Approach to Proof Search (regular paper)
Dans : Fixed Points in Computer Science (FICS 2013), Turin (Italie), 01/09/13, Vol. 126, David Baelde, Arnaud Carayol (Eds.), Electronic Proceedings in Theoretical Computer Science (EPTCS), p. 28-43, août 2013.
Résumé Accès : http://dx.doi.org/10.4204/EPTCS.126.3 – https://oatao.univ-toulouse.fr/12636/
BibTeXMathias Winckel, Ralph Matthes
On a Dynamic Logic for Graph Rewriting (regular paper)
Dans : Algebraic, Logical, and Algorithmic Methods of System Modeling, Specification and Verification (SMSV 2013), Kherson, Ukraine, 20/01/13-21/01/13, Vol. 1000, Vadim Ermolayev, Heinrich C. Mayr, Mykola Nikitchenko, Aleksander Spivakovsky (Eds.), CEUR-WS : Workshop proceedings, p. 506-520, juin 2013.
Verification of redecoration for infinite triangular matrices using coinduction (regular paper)
Dans : International Workshop on Types and Proofs for Programs (TYPES 2011), Bergen, Norvège, 08/09/11-11/09/11, Vol. 19, Nils Anders Danielsson, Bengt Nordström (Eds.), Schloss Dagstuhl Leibniz-Zentrum fur Informatik, LIPIcsLeibniz International Proceedings in Informatics, p. 55-69, janvier 2013.
Résumé Accès : http://www.irit.fr/~Ralph.Matthes/papers/MatthesPicardTYPES11PostProcLIPIcs.pdf – https://oatao.univ-toulouse.fr/12343/
BibTeXMathias Winckel, Ralph Matthes
Formalization of a dynamic logic for graph transformation in the Coq proof assistant (regular paper)
Dans : Theoretical and Applied Aspects of Program Systems Development (TAAPSD 2012), Kiew, 03/12/12-07/12/12, Mykola Nikitchenko (Eds.), Avangard, p. 31-42, décembre 2012.
Permutations in Coinductive Graph Representation (regular paper)
Dans : Coalgebraic Methods in Computer Science, Tallinn, Estonie, 31/03/12-01/04/12, Vol. 7399, Dirk Pattinson, Lutz Schröder (Eds.), Springer, LNCS, p. 218-237, 2012.
Résumé Accès : http://www.irit.fr/~Ralph.Matthes/papers/PicardMatthesCMCS12Preproceedings.pdf
BibTeXMathieu Giorgino, Martin Strecker, Ralph Matthes, Marc Pantel
Verification of the Schorr-Waite algorithm – From trees to graphs (regular paper)
Dans : International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2010), Hagenberg, Austria, 23/07/10-25/07/10, María Alpuente (Eds.), Springer, (en ligne), mars 2011.
Résumé Accès : http://www.irit.fr/~Mathieu.Giorgino/Publications/GiSt2010SchorrWaite.html
BibTeXMathieu Giorgino, Martin Strecker, Ralph Matthes, Marc Pantel
Verification of the Schorr-Waite algorithm – From trees to graphs (regular paper)
Dans : Formalisation des Activités Concurrentes (FAC 2010), Toulouse, France, 31/03/10-01/04/10, ONERA, (en ligne), avril 2010.
Résumé Accès : http://seminaire-verif.enseeiht.fr/FAC/2010/actes.html
BibTeXCoinductive graph representation: the problem of embedded lists
Dans : Graph Computation Models, Enschede – The Netherlands, 02/10/10, Rachid Echahed, Annegret Habel, Mohamed Mosbah (Eds.).
Accès : http://gcm-events.org/gcm2010/pages/gcm2010-preproceedings.pdf
BibTeXJosé Espírito Santo, Ralph Matthes, Luís Pinto
Monadic translation of intuitionistic sequent calculus
Dans : Conference of the Types Project (TYPES 2008), Torino, Italie, 26/03/08-29/03/08, Stefano Berardi, Ferruccio Damiani, Ugo de’Liguoro (Eds.), Springer, Lecture Notes in Computer Science 5497, p. 100-116, juin 2009.
Mathieu Giorgino, Ralph Matthes, Martin Strecker
Génération de programmes efficaces et vérifiés (short paper)
Dans : Approches Formelles dans l’Assistance au Développement de Logiciels (AFADL 2009), Toulouse, 26/01/09-28/01/09, Marc Pantel, Christel Seguin (Eds.), IRIT, p. 67-68, janvier 2009.
Résumé Accès : http://www.irit.fr/~Mathieu.Giorgino/Publications/GiMaSt2009Generation.html
BibTeXRecursion on Nested Datatypes in Dependent Type Theory
Dans : Computability in Europe Logic and Theory of Algorithms (CiE 2008), University of Athens, 15/06/08-20/06/08 (conférencier invité), Vol. 5028, Arnold Beckmann, Costas Dimitracopoulos, Benedikt Löwe (Eds.), Springer-Verlag, LNCS, p. 431-446, 2008.
Résumé Accès : http://www.irit.fr/~Ralph.Matthes/works.html
BibTeXNested Datatypes with Generalized Mendler Iteration: Map Fusion and the Example of the Representation of Untyped Lambda Calculus with Explicit Flattening
Dans : International Conference on Mathematics of Program Construction (MPC 2008), Marseille, 15/07/08-18/07/08, Vol. 5133, Philippe Audebaud, Christine Paulin-Mohring (Eds.), Springer-Verlag, LNCS, p. 220-242, 2008.
Résumé Accès : http://www.irit.fr/~Ralph.Matthes/works.html
BibTeXRalph Matthes, Martin Strecker
Verification of the Redecoration Algorithm for Triangular Matrices
Dans : Conference of the Types Project (TYPES 2007), Cividale, Italie, 02/05/07-05/05/07, Vol. 4941, Marino Miculan, Ivan Scagnetto, Furio Honsell (Eds.), Springer-Verlag, Lecture Notes in Computer Science, p. 125-141, 2008.
Résumé Accès : http://www.irit.fr/~Ralph.Matthes/works.html
BibTeXJosé Espírito Santo, Ralph Matthes, Luís Pinto
Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi
Dans : Typed Lambda Calculi and Applications, Paris, France, 26/06/07-28/06/07, Vol. 4583, Simona Ronchi Della Rocca (Eds.), Springer-Verlag, Lecture Notes in Computer Science, p. 133-147, juin 2007.
Résumé Accès : http://www.irit.fr/~Ralph.Matthes/papers/TLCA07final.pdf
BibTeXStabilization – An Alternative to Double-Negation Translation for Classical Natural Deduction
Dans : Logic Colloquium (LC 2003), Helsinki, Finland, 14/08/03-20/08/03, Vol. 24, Viggo Stoltenberg-Hansen, Jouko Väänänen (Eds.), A K Peters, Lecture Notes in Logic, p. 167-199, 2006.
Résumé Accès : http://www.irit.fr/~Ralph.Matthes/works.html
BibTeXVerification of programs on truly nested datatypes in intensional type theory
Dans : Workshop on Mathematically Structured Functional Programming (MSFP 2006), Kuressaare, Estonie, 02/07/06, Conor McBride, Tarmo Uustalu (Eds.), British Computer Society, Electronic Workshops in Computing (eWiC), (en ligne), juin 2006.
Résumé Accès : http://www.bcs.org/server.php?show=ConWebDoc.5352
BibTeXA Datastructure for Iterated Powers
Dans : International Conference on Mathematics of Program Construction (MPC 2006), Kuressaare, Estonie, 03/07/06-05/07/06, Vol. 4014, Tarmo Uustalu (Eds.), Springer-Verlag, LNCS, p. 299-315, juin 2006.
Résumé Accès : http://www.irit.fr/~Ralph.Matthes/papers/mpc06final.pdf
BibTeX
José Espírito Santo, Ralph Matthes, Luís Pinto
Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic
Ugo de’Liguoro; Stefano Berardi; Thorsten Altenkirch. LIPIcs : 26th International Conference on Types for Proofs and Programs (TYPES 2020), 188, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany, 2021, LIPIcs : Leibniz International Proceedings in Informatics ; ISSN : 1868-8969, 978-3-95977-182-5. ⟨10.4230/LIPIcs.TYPES.2020.4⟩
Ulrich Berger, Ralph Matthes, Anton Setzer
Martin Hofmann’s Case for Non-Strictly Positive Data Types
Peter Dybjer; José Espírito Santo; Luís Pinto. 24th International Conference on Types for Proofs and Programs (TYPES 2018), 130, Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, pp.1:1-1:22, 2019, Leibniz International Proceedings in Informatics (LIPIcs), 978-3-95977-106-1. ⟨10.4230/LIPIcs.TYPES.2018.1⟩
Benedikt Ahrens, Ralph Matthes
Heterogeneous Substitution Systems Revisited
Tarmo Uustalu. 21st International Conference on Types for Proofs and Programs (TYPES 2015), 69, Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, pp.2:1-2:23, 2018, Leibniz International Proceedings in Informatics (LIPIcs), 978-3-95977-030-9. ⟨10.4230/LIPIcs.TYPES.2015.2⟩
Types inductifs au-delà de la stricte positivité
Habilitation à diriger des recherches, Université Paul Sabatier, mai 2005.
Tenth International Workshop on Fixed Points in Computer Science (FICS 2015), Berlin, Allemagne, 11/09/2015 – 12/09/2015
Matthes, Ralph; Mio, Matteo. Electronic Proceedings in Theoretical Computer Science, 191, 2015, ⟨10.4204/EPTCS.191⟩
Ralph Matthes, Kobe Wullaert, Benedikt Ahrens
Substitution for Non-Wellfounded Syntax with Binders
2023