Filtrer vos résultats
- 17
- 6
- 9
- 7
- 3
- 1
- 1
- 1
- 1
- 1
- 23
- 8
- 1
- 2
- 1
- 2
- 5
- 1
- 1
- 1
- 2
- 4
- 1
- 2
- 23
- 23
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 23
- 5
- 5
- 4
- 3
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
23 résultats
|
|
triés par
|
|
From signatures to monads in UniMathJournal of Automated Reasoning, 2019, 63 (2), pp.285-318. ⟨10.1007/s10817-018-9474-4⟩
Article dans une revue
hal-01410487v3
|
||
|
Univalent Monoidal CategoriesLeibniz 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
|
||
|
Monadic translation of classical sequent calculusMathematical Structures in Computer Science, 2013, vol. 23 (n° 6), pp. 1111-1162. ⟨10.1017/S0960129512000436⟩
Article dans une revue
hal-01138759v1
|
||
|
A Coinductive Approach to Proof SearchFixed Points in Computer Science (FICS 2013), Sep 2013, Turin, Italy. pp. 28-43
Communication dans un congrès
hal-01226485v1
|
||
|
Coinductive Graph Representation: the Problem of Embedded ListsElectronic 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
|
||
|
Martin Hofmann's Case for Non-Strictly Positive Data TypesPeter 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 Binders2023
Pré-publication, Document de travail
hal-04181049v1
|
||
|
A Coinductive Approach to Proof Search through Typed Lambda-CalculiAnnals of Pure and Applied Logic, 2021, 172 (10), ⟨10.1016/j.apal.2021.103026⟩
Article dans une revue
hal-03086504v1
|
||
|
Verification of redecoration for infinite triangular matrices using coinductionInternational Workshop on Types and Proofs for Programs - TYPES 2011, Sep 2011, Bergen, Norway. pp. 55-69
Communication dans un congrès
hal-01143261v1
|
||
|
On a Dynamic Logic for Graph Rewriting2nd 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
|
||
|
Decidability of several concepts of finiteness for simple typesFundamenta Informaticae, 2019, 170 (1-3), pp.111-138. ⟨10.3233/FI-2019-1857⟩
Article dans une revue
hal-02119503v1
|
||
|
Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional LogicUgo 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
|
||
|
Certification of Breadth-First Algorithms by Extraction13th 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 computations5th 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
|
||
|
Verification of the Schorr-Waite Algorithm - From Trees to GraphsLogic-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
|
||
|
Implementing a Category-Theoretic Framework for Typed Abstract Syntax11th 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
|
||
|
Displayed Monoidal Categories for the Semantics of Linear LogicCertified Programs and Proofs (CPP 2024), Jan 2024, London, United Kingdom. à paraître, ⟨10.1145/3636501.3636956⟩
Communication dans un congrès
hal-04375376v1
|
||
|
Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof searchMathematical 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/2013Matthes, 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) 2013Fundamenta 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/2015Matthes, Ralph; Mio, Matteo. Electronic Proceedings in Theoretical Computer Science, 191, 2015, ⟨10.4204/EPTCS.191⟩
Ouvrages
hal-03198240v1
|
||
|
Permutations in Coinductive Graph Representation11th 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
|
||
|
Heterogeneous Substitution Systems RevisitedTarmo 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
|