Publications of 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
In : Mathematical Structures in Computer Science, Cambridge University Press, Vol. 23 N. 6, pp. 1111-1162, December 2013.
URL : 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)
In : RAIRO – Theoretical Informatics and Applications, EDP Sciences, Special issue Sixth Workshop on Fixed Points in Computer Science, FICS 2009, Vol. 47 N. 1, pp. 1-2, December 2012.
Ralph Matthes, Sergei Soloviev
Preface to the special issue: commutativity of algebraic diagrams
In : Mathematical Structures in Computer Science, Cambridge University Press, Special issue CAMCAD ’09 Commutativity of Algebraic Diagrams, Vol. 22 N. 6, pp. 901-903, December 2012.
Coinductive Graph Representation : the Problem of Embedded Lists
In : Electronic Communications of the EASST (ECEASST), Electronic Communications of the EASST, Berlin – Germany, Special issue Selected Revised Papers from the Third International Workshop on Graph Computation Models (GCM 2010), Vol. 39, (on line), September 2011.
Abstract URL : http://journal.ub.tu-berlin.de/eceasst/article/view/649
BibTeXMap Fusion for Nested Datatypes in Intensional Type Theory
In : Science of Computer Programming, Elsevier, Vol. 76, pp. 204-224, 2011.
Abstract URL : 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
In : Logical Methods in Computer Science, Logical Methods in Computer Science, Germany, Vol. 5 N. 2, (on line), May 2009.
URL : 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
In : Journal of Functional Programming, Cambridge University Press, Vol. 19 N. 3&4, pp. 439-468, June 2009.
Abstract URL : http://dx.doi.org/10.1017/S095679680900731X
BibTeXRalph Matthes, Sergei Soloviev
Preface to the special issue: isomorphisms of types and invertibility of lambda terms
In : Mathematical Structures in Computer Science, Cambridge University Press, Special issue Isomorphisms of types and invertibility of lambda terms, Vol. 18, pp. 645-646, August 2008.
Ralph Matthes, Kobe Wullaert, Benedikt Ahrens
Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories
9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024), Jul 2024, Tallinn, Estonia. pp.25:1-25:22, ⟨10.4230/LIPIcs.FSCD.2024.25⟩
Benedikt Ahrens, Ralph Matthes, Niels van der Weide, Kobe Wullaert
Displayed Monoidal Categories for the Semantics of Linear Logic
CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2024, London, United Kingdom. pp.260-273, ⟨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)
In : 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), pp. 28-43, August 2013.
Abstract URL : 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)
In : 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, pp. 506-520, June 2013.
Verification of redecoration for infinite triangular matrices using coinduction (regular paper)
In : 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, pp. 55-69, January 2013.
Abstract URL : 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)
In : Theoretical and Applied Aspects of Program Systems Development (TAAPSD 2012), Kiew, 03/12/12-07/12/12, Mykola Nikitchenko (Eds.), Avangard, pp. 31-42, December 2012.
Permutations in Coinductive Graph Representation (regular paper)
In : Coalgebraic Methods in Computer Science, Tallinn, Estonie, 31/03/12-01/04/12, Vol. 7399, Dirk Pattinson, Lutz Schröder (Eds.), Springer, LNCS, pp. 218-237, 2012.
Abstract URL : 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)
In : International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2010), Hagenberg, Austria, 23/07/10-25/07/10, María Alpuente (Eds.), Springer, (on line), March 2011.
Abstract URL : 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)
In : Formalisation des Activités Concurrentes (FAC 2010), Toulouse, France, 31/03/10-01/04/10, ONERA, (on line), April 2010.
Abstract URL : http://seminaire-verif.enseeiht.fr/FAC/2010/actes.html
BibTeXCoinductive graph representation: the problem of embedded lists
In : Graph Computation Models, Enschede – The Netherlands, 02/10/10, Rachid Echahed, Annegret Habel, Mohamed Mosbah (Eds.).
URL : http://gcm-events.org/gcm2010/pages/gcm2010-preproceedings.pdf
BibTeXJosé Espírito Santo, Ralph Matthes, Luís Pinto
Monadic translation of intuitionistic sequent calculus
In : 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, pp. 100-116, June 2009.
Mathieu Giorgino, Ralph Matthes, Martin Strecker
Génération de programmes efficaces et vérifiés (short paper)
In : 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, pp. 67-68, January 2009.
Abstract URL : http://www.irit.fr/~Mathieu.Giorgino/Publications/GiMaSt2009Generation.html
BibTeXRecursion on Nested Datatypes in Dependent Type Theory
In : Computability in Europe Logic and Theory of Algorithms (CiE 2008), University of Athens, 15/06/08-20/06/08 (invited speaker), Vol. 5028, Arnold Beckmann, Costas Dimitracopoulos, Benedikt Löwe (Eds.), Springer-Verlag, LNCS, pp. 431-446, 2008.
Abstract URL : 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
In : 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, pp. 220-242, 2008.
Abstract URL : http://www.irit.fr/~Ralph.Matthes/works.html
BibTeXRalph Matthes, Martin Strecker
Verification of the Redecoration Algorithm for Triangular Matrices
In : 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, pp. 125-141, 2008.
Abstract URL : 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
In : 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, pp. 133-147, June 2007.
Abstract URL : http://www.irit.fr/~Ralph.Matthes/papers/TLCA07final.pdf
BibTeXStabilization – An Alternative to Double-Negation Translation for Classical Natural Deduction
In : 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, pp. 167-199, 2006.
Abstract URL : http://www.irit.fr/~Ralph.Matthes/works.html
BibTeXVerification of programs on truly nested datatypes in intensional type theory
In : 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), (on line), June 2006.
Abstract URL : http://www.bcs.org/server.php?show=ConWebDoc.5352
BibTeXA Datastructure for Iterated Powers
In : 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, pp. 299-315, June 2006.
Abstract URL : 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é
HDR, Université Paul Sabatier, May 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, Aleksy Schubert
19th International Conference on Types for Proofs and Programs (TYPES 2013), Toulouse, 22/04/2013 – 26/04/2013
Matthes, Ralph; Schubert, Aleksy. 19th International Conference on Types for Proofs and Programs (TYPES 2013), Apr 2013, Toulouse, France. Leibniz International Proceedings in Informatics , 26, 2014, Leibniz International Proceedings in Informatics (LIPIcs), 978-3-939897-72-9
Special Issue “Sixth Workshop on Fixed Points in Computer Science, FICS 2009”
Dans : RAIRO – Theoretical Informatics and Applications, EDP Sciences, Vol. 47 N. 1, 2013.
Ralph Matthes, Sergei Soloviev
CAMCAD ’09 Commutativity of Algebraic Diagrams
Dans : Mathematical Structures in Computer Science, Cambridge University Press, Vol. 22 N. 6, décembre 2012.
URL : http://journals.cambridge.org/action/displayIssue?jid=MSC&volumeId=22&seriesId=0&issueId=06
BibTeXRalph Matthes, Sergei Soloviev
Isomorphism of types and invertibility of lambda terms
Dans : Mathematical Structures in Computer Science, Cambridge University Press, Vol. 18, août 2008.
Kobe Wullaert, Ralph Matthes, Benedikt Ahrens
Univalent Monoidal Categories
Leibniz International Proceedings in Informatics , 269, Schloss Dagstuhl – Leibniz Center for Informatics, pp.15:1-15:21, 2023, 28th International Conference on Types for Proofs and Programs (TYPES 2022), 978-3-95977-285-3. ⟨10.4230/LIPIcs.TYPES.2022.15⟩
6th Workshop on Fixed Points in Computer Science, FICS 2009, Coimbra, Portugal, 12/09/09 – 13/09/09, Institute of Cybernetics at Tallinn University of Technology, August 2009.
4th International Workshop on Higher-Order Rewriting, Paris, 25/06/07 – 25/06/07, IRIT, June 2007.
URL : http://www.irit.fr/~Ralph.Matthes/HOR/Proceedings.pdf
BibTeX