Publications HAL du labo/EPI deducteam

2018

Journal articles

titre
Size-based termination of higher-order rewriting
auteur
Frédéric Blanqui
article
Journal of Functional Programming, Cambridge University Press (CUP), 2018, 〈10.1017/S0956796818000072〉
identifiant
hal-01424921
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01424921/file/main.pdf BibTex

Conference papers

titre
Drags: A Simple Algebraic Framework For Graph Rewriting
auteur
Nachum Dershowitz, Jean-Pierre Jouannaud
article
TERMGRAPH 2018 - 10th International Workshop on Computing with Terms and Graphs, Jul 2018, Oxford, United Kingdom
identifiant
hal-01853836
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01853836/file/GraphRewritingTG-Final.pdf BibTex

Preprints, Working Papers, ...

titre
A logic identifying isomorphic propositions
auteur
Alejandro Díaz-Caro, Gilles Dowek
article
2018
identifiant
hal-01109104
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01109104/file/paper.pdf BibTex
titre
Linking Focusing and Resolution with Selection
auteur
Guillaume Burel
article
2018
identifiant
hal-01670476
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01670476/file/lipics.pdf BibTex

2017

Journal articles

titre
Rules and derivations in an elementary logic course
auteur
Gilles Dowek
article
IfColog Journal of Logics and their Applications (FLAP), College Publications, 2017, 4 (1)
identifiant
hal-01252124
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01252124/file/ttl.pdf BibTex
titre
Quantum causal graph dynamics
auteur
Pablo Arrighi, Simon Martiel
article
Physical Review D, American Physical Society, 2017, 96 (2), pp.024026
identifiant
hal-01785461
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01785461/file/1607.06700.pdf BibTex

Conference papers

titre
Typing Quantum Superpositions and Measurement
auteur
Alejandro Díaz-Caro, Gilles Dowek
article
Carlos Martín-Vide; Roman Neruda; Miguel A. Vega-Rodríguez. TPNC 2017 - 6th International Conference on the Theory and Practice of Natural Computing, Dec 2017, Prague, Czech Republic. Springer, 10687, pp.13, 2017, Lecture Notes in Computer Science. 〈http://grammars.grlmc.com/TPNC2017/〉. 〈10.1007/978-3-319-71069-3_22〉
identifiant
hal-01670387
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01670387/file/quantumsuperposition.pdf BibTex
titre
Proof certificates in PVS
auteur
Frédéric Gilbert
article
ITP 2017 - 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. Springer, LNCS, 10499, pp.262-268, 2017, ITP 2017: Interactive Theorem Proving. 〈http://itp2017.cic.unb.br/〉. 〈10.1007/978-3-319-66107-0_17〉
identifiant
hal-01673517
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01673517/file/main.pdf BibTex
titre
Analyzing individual proofs as the basis of interoperability between proof systems
auteur
Gilles Dowek
article
PxTP 2017 - Fifth Workshop on Proof eXchange for Theorem Proving, Sep 2017, Brasilia, Brazil
identifiant
hal-01670394
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01670394/file/analyzing.pdf BibTex
titre
Coq without Type Casts: A Complete Proof of Coq Modulo Theory
auteur
Jean-Pierre Jouannaud, Pierre-Yves Strub
article
LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, May 2017, Maun, Botswana
identifiant
hal-01664457
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01664457/file/final-version.pdf BibTex
titre
Automated Constructivization of Proofs
auteur
Frédéric Gilbert
article
FoSSaCS 2017, Apr 2017, Uppsala, Sweden. 2017, 〈10.1007/978-3-662-54458-7_28〉
identifiant
hal-01516788
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01516788/file/constructivization.pdf BibTex

Master thesis

titre
Termination checking in the λΠ-calculus modulo theory. From a practical and a theoretical viewpoint
auteur
Guillaume Genestier
article
Logic in Computer Science [cs.LO]. 2017
identifiant
hal-01676409
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01676409/file/Genestier_RapportLMFI.pdf BibTex
titre
Tactiques de preuve dans Dedukti
auteur
Antoine Defourné
article
Logique en informatique [cs.LO]. 2017
identifiant
hal-01661872
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01661872/file/rapport_pfe_ensimag.pdf BibTex

Books

titre
Le temps des algorithmes
auteur
Serge Abiteboul, Gilles Dowek
article
Editions Le Pommier, pp.192, 2017, 978-2746511750
identifiant
hal-01502505
Accès au bibtex
BibTex

Poster communications

titre
mSAT:An OCaml SAT Solver
auteur
Guillaume Bury
article
OCaml Users and Developers Workshop, Sep 2017, Oxford, United Kingdom
identifiant
hal-01670765
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01670765/file/poster.pdf BibTex

Preprints, Working Papers, ...

titre
Extending higher-order logic with predicate subtyping: application to PVS
auteur
Frédéric Gilbert
article
2017
identifiant
hal-01673518
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01673518/file/dissertation.pdf BibTex
titre
Exporting an Arithmetic Library from Dedukti to HOL
auteur
François Thiré
article
2017
identifiant
hal-01668250
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01668250/file/sttforall-fscd.pdf BibTex
titre
Models and termination of proof reduction in the λΠ-calculus modulo theory
auteur
Gilles Dowek
article
2017
identifiant
hal-01101834
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01101834/file/superpi.pdf BibTex
titre
Untyped Confluence In Dependent Type Theories
auteur
Ali Assaf, Gilles Dowek, Jean-Pierre Jouannaud, Jiaxiang Liu
article
2017
identifiant
hal-01515505
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01515505/file/conf.pdf BibTex

2016

Journal articles

titre
Free fall and cellular automata
auteur
Pablo Arrighi, Gilles Dowek
article
Electronic Proceedings in Theoretical Computer Science, EPTCS, 2016, 204, pp.1 - 10. 〈10.4204/EPTCS.204.1〉
identifiant
hal-01421712
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01421712/file/freefall.pdf BibTex

Conference papers

titre
ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti
auteur
Raphaël Cauderlier, Catherine Dubois
article
ICTAC 2016 - 13th International Colloquium on Theoretical Aspects of Computing, Oct 2016, Taipei, Taiwan. Theoretical Aspects of Computing – ICTAC 2016, 9965, pp.459-468, 2016, LNCS. 〈http://cc.ee.ntu.edu.tw/~ictac2016/〉. 〈10.1007/978-3-319-46750-4_26〉
identifiant
hal-01420638
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01420638/file/ICTAC_2016.pdf BibTex
titre
Soundly Proving B Method Formulae Using Typed Sequent Calculus
auteur
Pierre Halmagrand
article
Augusto Sampaio; Farn Wang. 13th International Colloquium on Theoretical Aspects of Computing (ICTAC), Oct 2016, Taipei, Taiwan. Springer International Publishing, Theoretical Aspects of Computing – ICTAC 2016, 9965, pp 196-213, 2016, Lecture Notes in Computer Science. 〈http://cc.ee.ntu.edu.tw/~ictac2016/〉. 〈10.1007/978-3-319-46750-4_12〉
identifiant
hal-01342849
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01342849/file/ictac-34.pdf BibTex
titre
Resolution in Solving Graph Problems
auteur
Kailiang Ji
article
8th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2016), Jul 2016, Toronto, Canada
identifiant
hal-01245138
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01245138/file/paper.pdf BibTex
titre
Encoding Proofs in Dedukti: the case of Coq proofs
auteur
Ali Assaf, Gilles Dowek, Jean-Pierre Jouannaud, Jiaxiang Liu
article
Proceedings Hammers for Type Theories, Jul 2016, Coimbra, Portugal. Easy Chair, Proc. HaTT, 2016, Proc. Higher-Order rewriting Workshop. 〈http://hatt2016.inria.fr/〉
identifiant
hal-01330980
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01330980/file/HaTT_2016_paper_3.pdf BibTex
titre
Reversible Causal Graph Dynamics
auteur
Pablo Arrighi, Simon Martiel, Simon Perdrix
article
Reversible Computation, Jul 2016, Bologna, Italy. 9720, pp.73-88, 2016, Lecture Notes in Computer Science. 〈10.1007/978-3-319-40578-0_5〉
identifiant
hal-01361427
Accès au bibtex
https://arxiv.org/pdf/1502.04368v2 BibTex
titre
Untyped Confluence in Dependent Type Theories
auteur
Ali Assaf, Gilles Dowek, Jean-Pierre Jouannaud, Jiaxiang Liu
article
Proceedings Higher-Order Rewriting Workshop, Jun 2016, Porto, Portugal. Easy-Chair, Higher-Order Rewriting Workshop, 2016, Proc. Higher-Order rewriting Workshop. 〈http://www.diku.dk/hjemmesider/ansatte/simonsen/HOR2016/〉
identifiant
hal-01330955
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01330955/file/HOR_2016_paper.pdf BibTex
titre
A Rewrite System for Proof Constructivization
auteur
Raphaël Cauderlier
article
Workshop on Logical Frameworks and Meta-Languages: Theory and Practice 2016, Jun 2016, Porto, Portugal. Workshop on Logical Frameworks and Meta-Languages: Theory and Practice 2016, pp.1 - 7, 2016, 〈http://dlicata.web.wesleyan.edu/events/lfmtp2016/〉. 〈10.1145/2966268.2966270〉
identifiant
hal-01420634
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01420634/file/LFMTP_2016.pdf BibTex
titre
Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system
auteur
Ali Assaf, Guillaume Burel, Raphal Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, Ronan Saillard
article
22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 2016, Novi SAd, Serbia
identifiant
hal-01441751
Accès au texte intégral et bibtex
https://hal-mines-paristech.archives-ouvertes.fr/hal-01441751/file/A-654.pdf BibTex
titre
Higher Order Proof Engineering: Proof Collaboration, Transformation, Checking and Retrieval
auteur
Shuai Wang
article
AITP 2016 - Conference on Artificial Intelligence and Theorem Proving, Apr 2016, Obergurgl, Austria
identifiant
hal-01250197
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01250197/file/aitp_2016_final.pdf BibTex

Master thesis

titre
Internship report MPRI 2 Reverse engineering on arithmetic proofs
auteur
François Thiré
article
Computer Science [cs]. 2016
identifiant
hal-01424816
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01424816/file/main.pdf BibTex

Theses

titre
Automated Deduction and Proof Certification for the B Method
auteur
Pierre Halmagrand
article
Logic in Computer Science [cs.LO]. Conservatoire National Des Arts et Métiers, Paris, 2016. English
identifiant
tel-01420460
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01420460/file/halmagrand-thesis.pdf BibTex
titre
Object-Oriented Mechanisms for Interoperability between Proof Systems
auteur
Raphaël Cauderlier
article
Logic in Computer Science [cs.LO]. Conservatoire National Des Arts et Métiers, Paris, 2016. English
identifiant
tel-01415945
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01415945/file/main.pdf BibTex

Preprints, Working Papers, ...

titre
What is the Planck constant the magnitude of?
auteur
Pablo Arrighi, Gilles Dowek
article
2016
identifiant
hal-01421711
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01421711/file/planck.pdf BibTex

2015

Journal articles

titre
Termination of rewrite relations on λ-terms based on Girard's notion of reducibility
auteur
Frédéric Blanqui
article
Theoretical Computer Science, Elsevier, 2015, 611 (50-86), pp.37. 〈10.1016/j.tcs.2015.07.045〉
identifiant
hal-01191693
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01191693/file/main.pdf BibTex
titre
The Computability Path Ordering
auteur
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2015, 〈10.2168/LMCS-11(4:3)2015〉
identifiant
hal-01163091
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01163091/file/main.pdf BibTex

Conference papers

titre
Discrete Geodesics and Cellular Automata
auteur
Pablo Arrighi, Gilles Dowek
article
Theory and Practice of Natural Computing, Dec 2015, Mieres, Spain. 2015, 〈10.1007/978-3-319-26841-5_11〉
identifiant
hal-01252131
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01252131/file/perihelion.pdf BibTex
titre
Decidability, Introduction Rules and Automata
auteur
Gilles Dowek, Ying Jiang
article
International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Bula, Fiji. 2015, International Conferences on Logic for Programming, Artificial Intelligence and Reasoning. 〈10.1007/978-3-662-48899-7_8〉
identifiant
hal-01252135
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01252135/file/intro.pdf BibTex
titre
Normalization by Completeness with Heyting Algebras
auteur
Gaëtan Gilbert, Olivier Hermant
article
LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji
identifiant
hal-01204599
Accès au texte intégral et bibtex
https://hal-mines-paristech.archives-ouvertes.fr/hal-01204599/file/A-614.pdf BibTex
titre
A Lightweight Double-negation Translation
auteur
Frédéric Gilbert
article
LPAR-20. 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji. EasyChair Proceedings in Computing, EasyChair Proceedings in Computing
identifiant
hal-01245021
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01245021/file/paper_36.pdf BibTex
titre
Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo
auteur
Guillaume Bury, David Delahaye, Damien Doligez, Pierre Halmagrand, Olivier Hermant
article
LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji. pp 42-58
identifiant
hal-01204701
Accès au texte intégral et bibtex
https://hal-mines-paristech.archives-ouvertes.fr/hal-01204701/file/A-615-v2.pdf BibTex
titre
Implementing Polymorphism in Zenon
auteur
Guillaume Bury, Raphaël Cauderlier, Pierre Halmagrand
article
11th International Workshop on the Implementation of Logics (IWIL), Nov 2015, Suva, Fiji. 11th International Workshop on the Implementation of Logics (IWIL), 2015, 〈http://www.eprover.org/EVENTS/IWIL-2015.html〉
identifiant
hal-01243593
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01243593/file/zenmo.pdf BibTex
titre
A Completion Method to Decide Reachability in Rewrite Systems
auteur
Guillaume Burel, Gilles Dowek, Ying Jiang
article
Carsten Lutz; Silvio Ranise. International Symposium on Frontiers of Combining Systems FroCoS'15, Sep 2015, Wroclaw, Poland. Springer, 9322, pp.205-219, 2015, Lecture Notes in Computer Science. 〈http://frocos2015.ii.uni.wroc.pl/〉. 〈10.1007/978-3-319-24246-0_13〉
identifiant
hal-01252138
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01252138/file/pkb.pdf BibTex
titre
Confluence of layered rewrite systems
auteur
Jiaxiang Liu, Jean-Pierre Jouannaud, Mizuhito Ogawa
article
24th EACSL Annual Conference on Computer Science Logic (CSL 2015), Sep 2015, Berlin, Germany. 41, pp.423--440, 〈http://logic.las.tu-berlin.de/csl2015/〉. 〈10.4230/LIPIcs.CSL.2015.423〉
identifiant
hal-01199062
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01199062/file/CSL-finalversion-150719.pdf BibTex
titre
Translating HOL to Dedukti
auteur
Ali Assaf, Guillaume Burel
article
Cezary Kaliszyk; Andrei Paskevich. Fourth Workshop on Proof eXchange for Theorem Proving, PxTP'15, Aug 2015, Berlin, Germany. 186, pp.74-88, 2015, EPTCS. 〈http://pxtp15.lri.fr/〉. 〈10.4204/EPTCS.186.8〉
identifiant
hal-01097412
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01097412/file/translating-hollight-dedukti-pxtp-2015.pdf BibTex
titre
Rewriting Modulo β in the λ Π-Calculus Modulo
auteur
Ronan Saillard
article
Logical Frameworks and Meta Languages: Theory and Practic, Affiliated with CADE-25, Aug 2015, Berlin, Germany. 185, pp 87-101, Electronic Proceedings in Theoretical Computer Science. 〈 http://eptcs.web.cse.unsw.edu.au/content.cgi?LFMTP15〉. 〈10.4204/EPTCS.185.6〉
identifiant
hal-01176715
Accès au texte intégral et bibtex
https://hal-mines-paristech.archives-ouvertes.fr/hal-01176715/file/A-610.pdf BibTex
titre
CTL Model Checking in Deduction Modulo
auteur
Kailiang Ji
article
Automated Deduction - CADE-25, Aug 2015, Berlin, Germany. pp 295-310, 2015, 〈10.1007/978-3-319-21401-6_20〉
identifiant
hal-01241132
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01241132/file/paper_20.pdf BibTex
titre
Checking Zenon Modulo Proofs in Dedukti
auteur
Raphaël Cauderlier, Pierre Halmagrand
article
Fourth Workshop on Proof eXchange for Theorem Proving (PxTP), Aug 2015, Berlin, Germany. 2015, 〈http://pxtp15.lri.fr/〉
identifiant
hal-01171360
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01171360/file/zendk.pdf BibTex
titre
Médiation en sciences du numériques : un levier pour comprendre notre quotidien ?
auteur
Sylvie Alayrangues, Gilles Dowek, Erwan Kerrien, Jean Mairesse, Thierry Viéville
article
Science & You, Jun 2015, Nancy, France. http://www.science-and-you.com, 2015
identifiant
hal-01211457
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01211457/file/S%26Y%20texte%20actes.pdf BibTex

Book sections

titre
On the definition of the classical connectives and quantifiers
auteur
Gilles Dowek
article
Edward Hermann Haeusler; Wagner de Campos Sanz; Bruno Lopes. Why is this a Proof?, Festschrift for Luiz Carlos Pereira , College Publications, 2015
identifiant
hal-01252221
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01252221/file/classical.pdf BibTex

Theses

titre
Un Calcul des Constructions implicite avec sommes dépendantes et à inférence de type décidable.
auteur
Bruno Bernardo
article
Langage de programmation [cs.PL]. École polytechnique, 2015. Français
identifiant
tel-01197380
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01197380/file/main.pdf BibTex
titre
A framework for defining computational higher-order logics
auteur
Ali Assaf
article
Computer Science [cs]. École polytechnique, 2015. English
identifiant
tel-01235303
Accès au texte intégral et bibtex
https://pastel.archives-ouvertes.fr/tel-01235303/file/thesis.pdf BibTex
titre
Model Checking and Theorem Proving
auteur
Kailiang Ji
article
Computation and Language [cs.CL]. Paris Diderot, 2015. English
identifiant
tel-01251073
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01251073/file/thesis_jikl.pdf BibTex
titre
Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond
auteur
Simon Cruanes
article
Logic in Computer Science [cs.LO]. École polytechnique, 2015. English
identifiant
tel-01223502
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/tel-01223502/file/thesis%20%281%29.pdf https://hal.archives-ouvertes.fr/tel-01223502/file/thesis.pdf BibTex

Preprints, Working Papers, ...

titre
Objects and subtyping in the λΠ-calculus modulo
auteur
Raphaël Cauderlier, Catherine Dubois
article
2015
identifiant
hal-01097444
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01097444/file/article_types.pdf BibTex
titre
Cut-elimination and the decidability of reachability in alternating pushdown systems
auteur
Gilles Dowek, Ying Jiang
article
2015
identifiant
hal-01101835
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01101835/file/reachability.pdf BibTex
titre
Conservativity of embeddings in the lambda-Pi calculus modulo rewriting (long version)
auteur
Ali Assaf
article
2015
identifiant
hal-01084165
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01084165/file/conservativity-embeddings-long.pdf BibTex
titre
Mixing HOL and Coq in Dedukti (Rough Diamond)
auteur
Ali Assaf, Raphaël Cauderlier
article
2015
identifiant
hal-01141789
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01141789/file/dedukti-interop.pdf BibTex

2014

Journal articles

titre
Call-by-value, call-by-name and the vectorial behaviour of the algebraic λ-calculus
auteur
Ali Assaf, Alejandro Díaz-Caro, Simon Perdrix, Christine Tasson, Benoît Valiron
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2014, 10:4 (8), pp.40. 〈http://lmcs-online.org/ojs/viewarticle.php?id=1567〉. 〈10.2168/LMCS-10(4:8)2014〉
identifiant
hal-01097602
Accès au bibtex
https://arxiv.org/pdf/1005.2897 BibTex
titre
Tableaux Modulo Theories Using Superdeduction
auteur
Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois
article
Global Journal of Advanced Software Engineering (GJASE), Avanti Publishers, 2014, 1, pp.1 - 13. 〈http://www.avantipublishers.com/downloads/gjasev1n1a1/〉. 〈10.1007/978-3-642-31365-3_26〉
identifiant
hal-01099338
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01099338/file/tab-sded.pdf BibTex

Conference papers

titre
Logtk : A Logic ToolKit for Automated Reasoning and its Implementation
auteur
Simon Cruanes
article
4th Workshop on Practical Aspects of Automated Reasoning, Jul 2014, Vienna, Austria. Konev, Boris and de Moura, Leonardo and Schulz, Stephan. 4th Workshop on Practical Aspects of Automated Reasoning (PAAR 2014), Jul 2014, Vienna, Austria
identifiant
hal-01101057
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01101057/file/logtk_paar.pdf BibTex
titre
Deduction modulo theory
auteur
Gilles Dowek
article
All about proofs. Proofs for all., Jul 2014, Wien, Austria
identifiant
hal-01101829
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01101829/file/wien.pdf BibTex
titre
Cut Admissibility by Saturation
auteur
Guillaume Burel
article
Gilles Dowek. Joint International Conference, RTA-TLCA 2014, Jul 2014, Vienna, Austria. Springer, 8560, pp.124-138, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-319-08918-8_9〉
identifiant
hal-01097428
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01097428/file/lncs.pdf BibTex
titre
Using Deduction Modulo in Set Theory
auteur
Pierre Halmagrand
article
SETS14, 1st International Workshop about Sets and Tools, Jun 2014, Toulouse, France. SETS14, 1st International Workshop about Sets and Tools, 2014, Toulouse, France, EasyChair., pp.12, 2014, 〈http://sets2014.cnam.fr/〉
identifiant
hal-01100512
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01100512/file/zen-mod.pdf BibTex
titre
A calculus of constructions with explicit subtyping
auteur
Ali Assaf
article
Hugo Herbelin; Pierre Letouzey; Matthieu Sozeau. 20th International Conference on Types for Proofs and Programs (TYPES 2014), May 2014, Institut Henri Poincaré, Paris, France. 39, 2015, LIPICS
identifiant
hal-01097401
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01097401/file/coc-explicit-subtyping-types-2014%20%281%29.pdf BibTex
titre
Objects and subtyping in the lambda-Pi-calculus modulo
auteur
Raphaël Cauderlier, Ali Assaf, Catherine Dubois
article
TYPES 2014, May 2014, Paris, France. pp.2, 2014
identifiant
hal-01126394
Accès au bibtex
BibTex

Poster communications

titre
Dedukti : un vérificateur de preuves universel
auteur
Ronan Saillard
article
Journées de seconde année de l'Ecole Doctorale à Mines ParisTech, Jun 2014, Paris, France
identifiant
hal-01100519
Accès au texte intégral et bibtex
https://hal-mines-paristech.archives-ouvertes.fr/hal-01100519/file/A-585-poster.pdf BibTex

Preprints, Working Papers, ...

titre
A point on fixpoints in posets
auteur
Frédéric Blanqui
article
2014
identifiant
hal-01097809
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01097809/file/main.pdf BibTex
titre
A Logical Approach to CTL
auteur
Gilles Dowek, Ying Jiang
article
2014
identifiant
hal-00919467
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00919467/file/ctl.pdf BibTex
titre
Axiomatizing truth in a finite model
auteur
Gilles Dowek, Ying Jiang
article
2014
identifiant
hal-00919469
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00919469/file/classes.pdf BibTex

2013

Journal articles

titre
A Formal Proof of Square Root and Division Elimination in Embedded Programs
auteur
Pierre Neron
article
Journal of Formalized Reasoning, ASDD-AlmaDL, 2013, 6 (1), pp.89-111
identifiant
hal-00924367
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00924367/file/JFRarticle.pdf BibTex
titre
Causal graph dynamics
auteur
Pablo Arrighi, Gilles Dowek
article
Information and Computation, Elsevier, 2013, 223, pp.78-93. 〈10.1016/j.ic.2012.10.019〉
identifiant
hal-00944459
Accès au bibtex
BibTex
titre
Universality in two dimensions
auteur
Nachum Dershowitz, Gilles Dowek
article
Journal of Logic and Computation, Oxford University Press (OUP), 2013, 〈10.1093/logcom/ext022〉
identifiant
hal-00919604
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00919604/file/universality2d.pdf BibTex
titre
Lineal: A linear-algebraic lambda-calculus
auteur
Pablo Arrighi, Gilles Dowek
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2013
identifiant
hal-00919625
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00919625/file/jlineal.pdf BibTex
titre
Typing linear algebra: A biproduct-oriented approach
auteur
Hugo Macedo, José Oliveira
article
Science of Computer Programming, Elsevier, 2013, 78 (11), pp.2160-2191. 〈http://www.sciencedirect.com/science/article/pii/S0167642312001402〉. 〈10.1016/j.scico.2012.07.012〉
identifiant
hal-00919866
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00919866/file/scp11.pdf BibTex

Conference papers

titre
Semantic A-translation and Super-consistency entail Classical Cut Elimination
auteur
Lisa Allali, Olivier Hermant
article
Ken McMillan and Aart Middeldorp and Andrei Voronkov. LPAR 19 - 19th Conference on Logic for Programming, Artificial Intelligence, and Reasoning - 2013, Dec 2013, Stellenbosch, South Africa. Springer, 8312, pp.407-422, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-45221-5_28〉
identifiant
hal-00923915
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00923915/file/SemanticTranslation.pdf BibTex
titre
Polarizing Double Negation Translations
auteur
Mélanie Boudard, Olivier Hermant
article
Ken McMillan and Aart Middeldorp and Andrei Voronkov. LPAR, Dec 2013, Stellenbosch, South Africa. Springer, 8312, pp.182-197, 2013, LNCS ARCoSS
identifiant
hal-00920224
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00920224/file/main.pdf BibTex
titre
Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo
auteur
David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant
article
Ken McMillan and Aart Middeldorp and Andrei Voronkov. LPAR - Logic for Programming Artificial Intelligence and Reasoning - 2013, Dec 2013, Stellenbosch, South Africa. Springer, 8312, pp.274-290, 2013, LNCS. 〈10.1007/978-3-642-45221-5_20〉
identifiant
hal-00909784
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00909784/file/Zenon-modulo-lpar-19.pdf BibTex
titre
Towards explicit rewrite rules in the λΠ-calculus modulo
auteur
Ronan Saillard
article
IWIL - 10th International Workshop on the Implementation of Logics, Dec 2013, Stellenbosch, South Africa. 2013
identifiant
hal-00921340
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00921340/file/article.pdf BibTex
titre
Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps
auteur
David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant
article
Stephan Schulz and Geoff Sutcliffe and Boris Konev. IWIL - 10th International Workshop on the Implementation of Logics - 2013, Dec 2013, Stellenbosch, South Africa. EasyChair, 2013
identifiant
hal-00909688
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00909688/file/zenon-modulo-iwil-2013.pdf BibTex
titre
Detection of First Order Axiomatic Theories
auteur
Guillaume Burel, Simon Cruanes
article
Pascal Fontaine and Christophe Ringeissen and Renate A. Schmidt. FroCoS - 9th International Symposium on Frontiers of Combining Systems - 2013, Sep 2013, Nancy, France. Springer, 8152, pp.229-244, 2013, Frontiers of Combining Systems. 〈http://link.springer.com/chapter/10.1007/978-3-642-40885-4_16〉. 〈10.1007/978-3-642-40885-4_16〉
identifiant
hal-00919759
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00919759/file/theory_detection_free.pdf BibTex
titre
Mining Malware Specifications through Static Reachability Analysis
auteur
Hugo Macedo, Tayssir Touili
article
Jason Crampton; Sushil Jajodia; Keith Mayes. ESORICS 2013 - 18th European Symposium on Research in Computer Security, Sep 2013, Egham, United Kingdom. Springer, 18th European Symposium on Research in Computer Security, Proceedings, 8134, pp.517-535, 2013, Lecture Notes in Computer Science. 〈http://link.springer.com/chapter/10.1007%2F978-3-642-40203-6_29〉. 〈10.1007/978-3-642-40203-6_29〉
identifiant
hal-00919782
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00919782/file/ims.pdf BibTex
titre
The probability of non-confluent systems
auteur
Alejandro Díaz-Caro, Gilles Dowek
article
Mauricio Ayala Rincón and Eduardo Bonelli and Ian Mackie. DCM - 9th International Workshop on Developments in Computational Models - 2013, Aug 2013, Buenos Aires, Argentina. 144, pp.1-15, 2014, Electronic Proceedings in Theoretical Computer Science. 〈http://dcm-workshop.org.uk/2013/〉. 〈10.4204/EPTCS.144.1〉
identifiant
hal-00919546
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00919546/file/probas.pdf BibTex
titre
Square root and division elimination in PVS
auteur
Pierre Neron
article
Sandrine Blazy and Christine Paulin-Mohring and David Pichardie. ITP - 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. Springer, 7998, pp.457-462, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-39634-2_33〉
identifiant
hal-00924359
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00924359/file/main.pdf BibTex
titre
Real numbers, chaos, and the principle of a bounded density of information
auteur
Gilles Dowek
article
Bulatov, Andrei A. and Shur, Arseny M. CSR 2013 - 8th International Computer Science Symposium in Russia, Jun 2013, Ekaterinburg, Russia. Springer, 7913, pp.347-353, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-38536-0_30〉
identifiant
hal-00919543
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00919543/file/csr.pdf BibTex
titre
Programming Robots With Events
auteur
Truong Giang Le, Dmitriy Fedosov, Olivier Hermant, Matthieu Manceny, Renaud Pawlak, Renaud Rioboo
article
Gunar Schirner; Marcelo Götz; Achim Rettberg; Mauro C. Zanella; Franz J. Rammig. 4th International Embedded Systems Symposium (IESS), Jun 2013, Paderborn, Germany. Springer, IFIP Advances in Information and Communication Technology, AICT-403, pp.14-25, 2013, Embedded Systems: Design, Analysis and Verification. 〈10.1007/978-3-642-38853-8_2〉
identifiant
hal-00924489
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00924489/file/iess2013.pdf BibTex
titre
A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo
auteur
Guillaume Burel
article
Jasmin Christian Blanchette and Josef Urban. PxTP - Third International Workshop on Proof Exchange for Theorem Proving - 2013, Jun 2013, Lake Placid, United States. EasyChair, 14, pp.43-57, 2013, PxTP 2013. 〈http://www.easychair.org/publications/?page=90156058〉
identifiant
hal-00921513
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00921513/file/easychair.pdf BibTex
titre
Call-by-value non-determinism in a linear logic type discipline
auteur
Alejandro Díaz-Caro, Giulio Manzonetto, Michele Pagani
article
Sergei Artemov and Anil Nerode. LFCS - Logical Foundations of Computer Science - 2013, Jan 2013, San Diego, CA, United States. Springer, 7734, pp.164-178, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-35722-0_12〉
identifiant
hal-00919463
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00919463/file/main.pdf BibTex
titre
Using Event-Based Style for Developing M2M Applications
auteur
Truong Giang Le, Olivier Hermant, Matthieu Manceny, Renaud Pawlak, Renaud Rioboo
article
James Park and Hamid Arabnia and Cheonshik Kim and Weisong Shi and Joon-Min Gil. GPC - 8th International Conference on Grid and Pervasive Computing - 2013, 2013, Seoul, South Korea. Springer, 7861, pp.348-357, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-38027-3_37〉
identifiant
hal-00924491
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00924491/file/gpc2013_version_2_.pdf BibTex

Books

titre
Informatique et sciences du numérique : Édition spéciale Python
auteur
Gilles Dowek, Jean-Pierre Archambault, Emmanuel Baccelli, Claudio Cimellli, Albert Cohen, Christine Eisenbeis, Thierry Viéville, Benjamin Wack, Hugues Bersini, Guillaume Le Blanc
article
Eyrolles, pp.352, 2013, 978-2212136760
identifiant
hal-01262640
Accès au bibtex
BibTex
titre
Informatique pour tous en classes préparatoires aux grandes écoles : Manuel d'algorithmique et programmation structurée avec Python
auteur
Judicaël Courant, Marc De Falco, Stéphane Gonnord, Jean-Christophe Filliâtre, Sylvain Conchon, Gilles Dowek, Benjamin Wack
article
Eyrolles, pp.1-390, 2013, 978-2-212-13700-2
identifiant
hal-00880268
Accès au bibtex
BibTex

Poster communications

titre
Dedukti:un vérificateur de preuves universel
auteur
Ali Assaf, Raphaël Cauderlier, Ronan Saillard
article
Journées nationales GDR - GPL - CIEL - AFADL, Apr 2013, Nancy, France
identifiant
hal-01086609
Accès au texte intégral et bibtex
https://hal-mines-paristech.archives-ouvertes.fr/hal-01086609/file/A-526-poster.pdf BibTex
titre
Elimination des racines et divisions pour du code embarqué
auteur
Pierre Neron
article
Journées du GDR-GPL, Apr 2013, Nancy, France
identifiant
hal-00924394
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00924394/file/poster.pdf BibTex

Reports

titre
Médiation Scientifique : une facette de nos métiers de la recherche
auteur
Antoine Rousseau, Aurélie Darnaud, Brice Goglin, Céline Acharian, Christine Leininger, Christophe Godin, Clarisse Holik, Claude Kirchner, Diane Rives, Elodie Darquie, Erwan Kerrien, Fabrice Neyret, Florent Masseglia, Florian Dufour, Gérard Berry, Gilles Dowek, Hélène Robak, Hélène Xypas, Irina Illina, Isabelle Gnaedig, Joanna Jongwane, Jocelyne Ehrel, Laurent Viennot, Laure Guion, Lisette Calderan, Lola Kovacic, Marie Collin, Marie-Agnès Enard, Marie-Hélène Comte, Martin Quinson, Martine Olivi, Mathieu Giraud, Mathilde Dorémus, Mia Ogouchi, Muriel Droin, Nathalie Lacaux, Nicolas Rougier, Nicolas Roussel, Pascal Guitton, Pierre Peterlongo, Rose-Marie Cornus, Simon Vandermeersch, Sophie Maheo, Sylvain Lefebvre, Sylvie Boldo, Thierry Viéville, Véronique Poirel, Aline Chabreuil, Arnaud Fischer, Claude Farge, Claude Vadel, Isabelle Astic, Jean-Pierre Dumont, Loic Féjoz, Patrick Rambert, Pierre Paradinas, Sophie De Quatrebarbes, Stéphane Laurent
article
[Interne] none. 2013, pp.34
identifiant
hal-00804915
Accès au bibtex
BibTex

Theses

titre
A Quest for Exactness: Program Transformation for Reliable Real Numbers
auteur
Pierre Neron
article
Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2013. English
identifiant
pastel-00960808
Accès au texte intégral et bibtex
https://pastel.archives-ouvertes.fr/pastel-00960808/file/pnthese.pdf BibTex

Preprints, Working Papers, ...

titre
On the definition of the classical connectives and quantifiers
auteur
Gilles Dowek
article
2013
identifiant
hal-00919437
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00919437/file/classical.pdf BibTex

2012

Journal articles

titre
A simple proof that super consistency implies cut elimination
auteur
Gilles Dowek, Olivier Hermant
article
Notre Dame Journal of Formal Logic, University of Notre Dame, 2012, 53 (4), pp. 93-106. 〈10.1215/00294527-1722692〉
identifiant
hal-00793008
Accès au texte intégral et bibtex
https://hal-mines-paristech.archives-ouvertes.fr/hal-00793008/file/A-516.pdf BibTex
titre
The Physical Church-Turing Thesis and the Principles of Quantum Theory
auteur
Pablo Arrighi, Gilles Dowek
article
International Journal of Foundations of Computer Science, World Scientific Publishing, 2012, 23 (5), pp.1131-1146. 〈10.1142/S0129054112500153〉
identifiant
hal-00944482
Accès au bibtex
BibTex

Conference papers

titre
ML Dependency Analysis for Assessors
auteur
François Pessaux, Vincent Benayoun, Catherine Dubois, Philippe Ayrault
article
Software Engineering and Formal Methods (SEFM) 2012, Oct 2012, Thessaloniki, Greece. Springer Verlag, 7504, pp.278-292, 〈10.1007/978-3-642-33826-7_19〉
identifiant
hal-01203505
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01203505/file/ML_deps_assess.pdf BibTex
titre
Non determinism through type isomorphism
auteur
Alejandro Díaz-Caro, Gilles Dowek
article
Delia Kesner and Petrucio Viana. LSFA - 7th Workshop on Logical and Semantic Frameworks with Applications - 2012, Sep 2012, Rio de Janeiro, Brazil. Open Publishing Association, 113, pp.137-144, 2013, Electronic Proceedings in Theoretical Computer Science. 〈10.4204/EPTCS.113.13〉
identifiant
hal-00925001
Accès au bibtex
https://arxiv.org/pdf/1303.7334 BibTex
titre
Causal Graph Dynamics
auteur
Pablo Arrighi, Gilles Dowek
article
Artur Czumaj and Kurt Mehlhorn and Andrew Pitts and Roger Wattenhofer. ICALP 2012 - 39th International ColloquiumAutomata, Languages, and Programming, Jul 2012, Warwick, United Kingdom. Springer, 7392, pp.54-66, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-31585-5_9〉
identifiant
hal-00944492
Accès au bibtex
BibTex

Directions of work or proceedings

titre
Natural Computing
auteur
Olivier Bournez, Gilles Dowek
article
France. Springer, pp.1, 2012
identifiant
hal-00760732
Accès au bibtex
BibTex

Master thesis

titre
Traduction de HOL en Dedukti
auteur
Ali Assaf
article
Logique en informatique [cs.LO]. 2012
identifiant
hal-00919871
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00919871/file/rapport.pdf BibTex

Books

titre
Informatique et Sciences du Numérique - Spécialité ISN en Terminale S
auteur
Gilles Dowek, Jean-Pierre Archambault, Emmanuel Baccelli, Claudio Cimellli, Albert Cohen, Christine Eisenbeis, Thierry Viéville, Benjamin Wack
article
Eyrolles, pp.303, 2012, ISBN 978-2-212-13543-5
identifiant
hal-00765220
Accès au bibtex
BibTex
titre
Informatique et sciences du numérique ― Spécialité ISN en terminale S, avec des exercices corrigés et des idées de projets
auteur
Gilles Dowek, Jean-Pierre Archambault, Emmanuel Baccelli, Claudio Cimelli, Albert Cohen, Christine Eisenbeis, Thierry Viéville, Benjamin Wack, Gérard Berry (préface)
article
Eyrolles, 2012
identifiant
hal-01257263
Accès au bibtex
BibTex

Preprints, Working Papers, ...

titre
Causal graph dynamics
auteur
Pablo Arrighi, Gilles Dowek
article
25 pages, 9 figures, LaTeX, v2: Minor presentation improvements, v3: Typos corrected, figure added. 2012
identifiant
hal-00944505
Accès au bibtex
https://arxiv.org/pdf/1202.1098 BibTex

2011

Conference papers

titre
The physical Church-Turing thesis and the principles of quantum theory
auteur
Pablo Arrighi, Gilles Dowek
article
QIPC, 2011, Zurich, Switzerland. Local proceedings, 2011
identifiant
hal-00944544
Accès au bibtex
https://arxiv.org/pdf/1102.1612 BibTex

Books

titre
Une introduction à la science informatique pour les enseignants de la discipline en lycée
auteur
Gilles Dowek, Jean-Pierre Archambault, Emmanuel Baccelli, Sylvie Boldo, Denis Bouhineau, Patrick Cegielski, Thomas Heide Clausen, Irène Guessarian, Stéphane Lopes, Laurent Mounier, Benjamin Nguyen, Franck Quessette, Anne Rasse, Brigitte Rozoy, Claude Timsit, Thierry Viéville, Jean-Marc Vincent
article
Gilles Dowek. CRDP Paris, pp.376, 2011, Repères pour agir (RPA disciplines & compétences), Christine Moulin, 978-2-86631-188-9
identifiant
hal-00765226
Accès au bibtex
BibTex