Filtrer vos résultats
- 28
- 24
- 32
- 11
- 3
- 3
- 2
- 1
- 50
- 18
- 1
- 1
- 3
- 2
- 3
- 3
- 3
- 2
- 3
- 2
- 2
- 1
- 3
- 2
- 1
- 3
- 1
- 2
- 2
- 2
- 1
- 1
- 4
- 2
- 3
- 49
- 3
- 52
- 3
- 2
- 2
- 1
- 1
- 52
- 21
- 4
- 4
- 4
- 3
- 2
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
52 résultats
|
|
|
triés par
|
From Ordered Monoids to Quantales and Petri Nets: Revised Semantics and Completeness Results in Intuitionistic Linear Logic[Intern report] 99-R-116 || galmiche99k, 1999, 30 p
Rapport
inria-00098934v1
|
|||
Provability and Countermodels in Gödel-Dummett LogicsInternational Workshop on Disproving: Non-theorems, Non-validity, Non-Provability - DISPROVING'07, Jul 2007, Bremen, Germany. pp.35-52
Communication dans un congrès
hal-00580307v1
|
|||
Phase Semantics and the Undecidability of Boolean BIGEOCAL-LAC, May 2011, Vandoeuvre-lès-Nancy, France
Communication dans un congrès
hal-00607775v1
|
|||
|
|
Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky MachinesThe 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Jan 2019, Cascais, Portugal. pp.104-117, ⟨10.1145/3293880.3294096⟩
Communication dans un congrès
hal-02333390v1
|
||
Gödel-Dummett counter-models through matrix computationWorkshop on Disproving, IJCAR 2004, 2004, Ireland
Communication dans un congrès
hal-00008808v1
|
|||
Formulae-as-Resources Management for an Intuitionistic Theorem Prover5th Workshop on Logic, Language, Information and Computation - WoLLIC'98, 1998, Sao Paulo, Brazil, 6 p
Communication dans un congrès
inria-00098599v1
|
|||
Resource models and proof-search in Intuitionistic Linear Logic[Intern report] A00-R-341 || galmiche00g, 2000, 39 p
Rapport
inria-00099314v1
|
|||
|
|
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
|
||
|
|
Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive LensLogical Methods in Computer Science, 2022, 18 (2), pp.17:1-17:29. ⟨10.46298/lmcs-18(2:17)2022⟩
Article dans une revue
hal-03359508v1
|
||
|
|
Looking at Separation Algebras with Boolean BI-eyes8th IFIP International Conference on Theoretical Computer Science (TCS), Sep 2014, Rome, Italy. pp. 326-340, ⟨10.1007/978-3-662-44602-7_25⟩
Communication dans un congrès
hal-01256804v1
|
||
|
|
Nondeterministic Phase Semantics and the Undecidability of Boolean BIACM Transactions on Computational Logic, 2013, 14 (1), pp.6. ⟨10.1145/2422085.2422091⟩
Article dans une revue
hal-01256956v1
|
||
Combining proof-search and linear counter-model constructionFirst APPSEM-II Workshop 2003 - (Applied Semantics II), 2003, Nottingham/UK
Communication dans un congrès
inria-00099553v1
|
|||
|
|
Typing Total Recursive Functions in CoqInteractive Theorem Proving - 8th International Conference, ITP 2017, Sep 2017, Brasilia, Brazil. pp.371-388, ⟨10.1007/978-3-319-66107-0_24⟩
Communication dans un congrès
hal-02333333v1
|
||
|
|
Simulating Induction-Recursion for Partial Algorithms24th International Conference on Types for Proofs and Programs,TYPES 2018, Jun 2018, Braga, Portugal
Communication dans un congrès
hal-02333374v1
|
||
|
|
Bounding Resource Consumption with Gödel-Dummett Logics12th International Conference on Logic for Programming Artificial Intelligence and Reasoning - LPAR'05, Dec 2005, Montego Bay, Jamaica. pp.682-696, ⟨10.1007/11591191_47⟩
Communication dans un congrès
hal-00012536v1
|
||
|
|
Some Remarks on Relations between Proofs and GamesPierre Edouard Bour, Manuel Rebuschi, Laurent Rollet,. Construction - Festschrift for Gerhard Heinzmann, College Publications, 2010, 978-1-84890-016-5
Chapitre d'ouvrage
hal-00580302v2
|
||
|
|
The Braga Method: Extracting Certified Algorithms from Complex Recursive Schemes in CoqProof and Computation II, WORLD SCIENTIFIC, pp.305-386, 2021, ⟨10.1142/9789811236488_0008⟩
Chapitre d'ouvrage
hal-03338785v1
|
||
|
|
Separation Logic with One Quantified Variable9th International Computer Science Symposium (CSR 2014), Jun 2014, Moscou, Russia. ⟨10.1007/978-3-319-06686-8_10⟩
Communication dans un congrès
hal-01258802v1
|
||
Reference Counting for Linear Counter-Model GenerationFirst APPSEM II Workshop, 2003, Nottingham, United Kingdom
Communication dans un congrès
hal-00008811v1
|
|||
STRIP: Structural sharing and intuitionistic proof-search[Intern report] A00-R-342 || galmiche00h, 2000, 5 p
Rapport
inria-00099328v1
|
|||
Labelled Tableaux for Proofs and Models in BI logicsAutomated Deduction Day, Jul 2009, Vandoeuvre-lès-Nancy, France
Communication dans un congrès
hal-00607777v1
|
|||
|
|
Constructive Decision via Redundancy-Free Proof-SearchJournal of Automated Reasoning, 2020, Special issue: Selected Extended Papers from IJCAR 2018, ⟨10.1007/s10817-020-09555-y⟩
Article dans une revue
hal-02944196v1
|
||
Structural Sharing and Efficient Proof-Search in Propositional Intuitionistic LogicAsian Computing Science Conference - ASIAN'99, 1999, Phuket, Thailand, pp.101-112
Communication dans un congrès
inria-00098992v1
|
|||
Quantales as completions of ordered monoids: revised semantics for Intuitionistic Linear LogicElectronic Notes in Theoretical Computer Science, 2000, 35, 15 p
Article dans une revue
inria-00099226v1
|
|||
|
|
A Coq Library for Mechanised First-Order LogicThe Coq Workshop 2022, Aug 2022, Haifa, Israel
Communication dans un congrès
hal-03756335v1
|
||
|
|
Separation Logic with One Quantified VariableTheory of Computing Systems, 2017, 61 (2), pp.371-461. ⟨10.1007/s00224-016-9713-1⟩
Article dans une revue
hal-01258821v1
|
||
|
|
Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), Jul 2021, Buenos Aires, Argentina. ⟨10.4230/LIPIcs.FSCD.2021.18⟩
Communication dans un congrès
hal-03280264v1
|
||
|
|
Proof Pearl: Faithful Computation and Extraction of µ-Recursive Algorithms in Coq14th International Conference on Interactive Theorem Proving (ITP 2023), Adam Naumowicz; René Thiemann, Jul 2023, Białystok, Poland. pp.21:1--17, ⟨10.4230/LIPIcs.ITP.2023.21⟩
Communication dans un congrès
hal-04200527v1
|
||
Kripke Models of Boolean BI and Invertible ResourcesDomains IX Workshop 08, Sep 2008, Brighton, United Kingdom. pp.1
Communication dans un congrès
hal-00580400v1
|
|||
|
|
Hilbert's Tenth Problem in Coq (Extended Version)Logical Methods in Computer Science, 2022, 18 (1), ⟨10.46298/lmcs-18(1:35)2022⟩
Article dans une revue
hal-03359505v2
|
- 1
- 2