Recherche - Archive ouverte HAL Accéder directement au contenu

Filtrer vos résultats

23 résultats
Image document

From signatures to monads in UniMath

Benedikt Ahrens , Ralph Matthes , Anders Mörtberg
Journal of Automated Reasoning, 2019, 63 (2), pp.285-318. ⟨10.1007/s10817-018-9474-4⟩
Article dans une revue hal-01410487v3

Univalent Monoidal Categories

Kobe Wullaert , Ralph Matthes , Benedikt Ahrens
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⟩
Proceedings/Recueil des communications hal-03889672v1
Image document

Monadic translation of classical sequent calculus

José Espirito Santo , Ralph Matthes , Koji Nakazawa , Luis Pinto
Mathematical Structures in Computer Science, 2013, vol. 23 (n° 6), pp. 1111-1162. ⟨10.1017/S0960129512000436⟩
Article dans une revue hal-01138759v1
Image document

A Coinductive Approach to Proof Search

José Espírito Santo , Ralph Matthes , Luís Pinto
Fixed Points in Computer Science (FICS 2013), Sep 2013, Turin, Italy. pp. 28-43
Communication dans un congrès hal-01226485v1
Image document

Coinductive Graph Representation: the Problem of Embedded Lists

Célia Picard , Ralph Matthes
Electronic Communications of the EASST, 2011, Graph Computation Models Selected Revised Papers from the Third International Workshop on Graph Computation Models (GCM 2010), 39
Article dans une revue hal-02015853v1
Image document

Martin Hofmann's Case for Non-Strictly Positive Data Types

Ulrich Berger , Ralph Matthes , Anton Setzer
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⟩
Chapitre d'ouvrage hal-02365814v1

Substitution for Non-Wellfounded Syntax with Binders

Ralph Matthes , Kobe Wullaert , Benedikt Ahrens
2023
Pré-publication, Document de travail hal-04181049v1
Image document

A Coinductive Approach to Proof Search through Typed Lambda-Calculi

José Espírito Santo , Ralph Matthes , Luís Pinto
Annals of Pure and Applied Logic, 2021, 172 (10), ⟨10.1016/j.apal.2021.103026⟩
Article dans une revue hal-03086504v1
Image document

Verification of redecoration for infinite triangular matrices using coinduction

Ralph Matthes , Célia Picard
International Workshop on Types and Proofs for Programs - TYPES 2011, Sep 2011, Bergen, Norway. pp. 55-69
Communication dans un congrès hal-01143261v1
Image document

On a Dynamic Logic for Graph Rewriting

Mathias Winckel , Ralph Matthes
2nd International Workshop on Algebraic, Logical, and Algorithmic Methods of System Modeling, Specification and Verification (SMSV 2013), Jan 2013, Kherson, Ukraine. pp. 506-520
Communication dans un congrès hal-01233230v1
Image document

Decidability of several concepts of finiteness for simple types

José Espírito Santo , Ralph Matthes , Luís Pinto
Fundamenta Informaticae, 2019, 170 (1-3), pp.111-138. ⟨10.3233/FI-2019-1857⟩
Article dans une revue hal-02119503v1
Image document

Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic

José Espírito Santo , Ralph Matthes , Luís Pinto
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⟩
Chapitre d'ouvrage hal-03255968v1
Image document

Certification of Breadth-First Algorithms by Extraction

Dominique Larchey-Wendling , Ralph Matthes
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⟩
Communication dans un congrès hal-02333423v1

Confluence for classical logic through the distinction between values and computations

José Espirito Santo , Ralph Matthes , Koji Nakazawa , Luis Pinto
5th International Workshop on Classical Logic and Computation (CL&C 2014), Jul 2014, Vienne, Austria. pp.63--77, ⟨10.4204/EPTCS.164.5⟩
Communication dans un congrès hal-03252258v1
Image document

Verification of the Schorr-Waite Algorithm - From Trees to Graphs

Mathieu Giorgino , Martin Strecker , Ralph Matthes , Marc Pantel
Logic-Based Program Synthesis and Transformation, Jul 2010, Hagenberg, Austria. pp.67-83, ⟨10.1007/978-3-642-20551-4_5⟩
Communication dans un congrès hal-00601440v1
Image document

Implementing a Category-Theoretic Framework for Typed Abstract Syntax

Benedikt Ahrens , Ralph Matthes , Anders Mörtberg
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⟩
Communication dans un congrès hal-03475481v1
Image document

Displayed Monoidal Categories for the Semantics of Linear Logic

Benedikt Ahrens , Ralph Matthes , Niels van der Weide , Kobe Wullaert
Certified Programs and Proofs (CPP 2024), Jan 2024, London, United Kingdom. à paraître, ⟨10.1145/3636501.3636956⟩
Communication dans un congrès hal-04375376v1
Image document

Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search

José Espírito Santo , Ralph Matthes , Luís Pinto
Mathematical Structures in Computer Science, 2019, 29 (8), pp.1092-1124. ⟨10.1017/S0960129518000099⟩
Article dans une revue hal-02360678v1

19th International Conference on Types for Proofs and Programs (TYPES 2013), Toulouse, 22/04/2013 - 26/04/2013

Ralph Matthes , Aleksy Schubert
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
N°spécial de revue/special issue hal-03252259v1

Preface : Fixed Points in Computer Science (FICS) 2013

David Baelde , Arnaud Carayol , Ralph Matthes , Igor Walukiewicz
Fundamenta Informaticae, 2017, 150 (3-4), pp.i-ii. ⟨10.3233/FI-2017-1468⟩
Article dans une revue hal-03116273v1

Tenth International Workshop on Fixed Points in Computer Science (FICS 2015), Berlin, Allemagne, 11/09/2015 - 12/09/2015

Ralph Matthes , Matteo Mio
Matthes, Ralph; Mio, Matteo. Electronic Proceedings in Theoretical Computer Science, 191, 2015, ⟨10.4204/EPTCS.191⟩
Ouvrages hal-03198240v1
Image document

Permutations in Coinductive Graph Representation

Célia Picard , Ralph Matthes
11th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Mar 2012, Tallinn, Estonia. pp.218-237, ⟨10.1007/978-3-642-32784-1_12⟩
Communication dans un congrès hal-01539884v1
Image document

Heterogeneous Substitution Systems Revisited

Benedikt Ahrens , Ralph Matthes
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⟩
Chapitre d'ouvrage hal-02360681v1