Publications : DEDUCTEAM

[BGH19]
F. Blanqui, G. Genestier, and O. Hermant. Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting. In Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD'19), volume 131 of Leibniz International Proceedings in Informatics, pages 9:1--9:21, Dortmund, Germany, June 2019. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.FSCD.2019.9.
BibTex | DOI | Web page | PDF ]
[DD19]
A. Díaz-Caro and G. Dowek. Proof Normalisation in a Logic Identifying Isomorphic Propositions. In Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD'19), volume 131 of Leibniz International Proceedings in Informatics, pages 14:1--14:23, Dortmund, Germany, June 2019. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.FSCD.2019.14.
BibTex | DOI | Web page | PDF ]
[CLS19]
S. Colin, R. Lepigre, and G. Scherer. Unboxing Mutually Recursive Type Definitions. In Actes des 30èmes Journées Francophones sur les Langages Applicatifs (JFLA'19), Lamoura, France, January 2019. To appear.
BibTex | PDF ]
[Bur18a]
G. Burel. Linking Focusing and Resolution with Selection. In Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS'18), volume 117 of Leibniz International Proceedings in Informatics, pages 9:1--9:14, Liverpool, UK, August 2018. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.MFCS.2018.9.
BibTex | DOI | Web page | PDF ]
[LR18a]
R. Lepigre and C. Raffalli. Abstract Representation of Binders in OCaml using the Bindlib Library. In Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'18), pages 42--56, Oxford, UK, July 2018. ACM Press.
doi: 10.4204/EPTCS.274.4.
BibTex | DOI | Web page | PDF ]
[Gil18]
F. Gilbert. Extending higher-order logic with predicate subtyping. Thèse de doctorat, Université Paris 7, Paris, France, April 2018.
BibTex | PDF ]
[Bur18b]
G. Burel. Linking Focusing and Resolution with Selection. Research Report hal-01670476, HAL Research Report, April 2018.
BibTex | Web page | PDF ]
[Bla18]
F. Blanqui. Size-based termination of higher-order rewriting. Journal of Functional Programming, 28, April 2018.
doi: 10.1017/S0956796818000072.
BibTex | DOI | Web page | PDF ]
[LR18b]
R. Lepigre and C. Raffalli. Practical Subtyping for Curry-Style Languages. ACM Transactions on Programming Languages and Systems, 41(1):5:1--5:58, 2018.
doi: 10.1145/3285955.
BibTex | DOI | PDF ]
[Lep18]
R. Lepigre. PML_2: Integrated Program Verification in ML. In Proceedings of the 23rd International Conference on Types for Proofs and Programs (TYPES'17, volume 104 of Leibniz International Proceedings in Informatics, pages 4:1--4:27, Budapest, Hungary, 2018. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.TYPES.2017.4.
BibTex | DOI | Web page | PDF ]
[Thi17]
F. Thiré. Exporting an Arithmetic Library from Dedukti to HOL. Research Report hal-01668250, HAL Research Report, December 2017.
BibTex | Web page | PDF ]
[Gil17b]
F. Gilbert. Proof Certificates in PVS. In Proceedings of the 8th International Conference on Interactive Theorem Proving (ITP'17), volume 10499 of Lecture Notes in Computer Science, pages 262--268, Brasília, Brazil, September 2017. Springer.
doi: 10.1007/978-3-319-66107-0_17.
BibTex | DOI | Web page | PDF ]
[Bur17]
G. Bury. mSAT: An OCaml SAT Solver. In OCaml Users and Developers Workshop, Oxford, UK, September 2017. Poster.
BibTex | Web page | PDF ]
[Sub17]
C. L. Subramaniam. Cubical Type Theory in Dedukti. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, September 2017.
BibTex ]
[Gen17]
G. Genestier. Termination checking in the λΠ-calculus modulo theory. Rapport de Master, Université Paris 7, Paris, France, September 2017.
BibTex | Web page | PDF ]
[Def17]
A. Defourné. Proof Tactics in Dedukti. Rapport de Master, Inria Saclay, September 2017.
BibTex | Web page | PDF ]
[Dow17a]
G. Dowek. Analyzing Individual Proofs as the Basis of Interoperability between Proof Systems. In Proceedings of the 5th Workshop on Proof eXchange for Theorem Proving (PxTP'17), volume 262 of Electronic Proceedings in Theoretical Computer Science, pages 3--12, Brasília, Brazil, September 2017.
doi: 10.4204/EPTCS.262.1.
BibTex | DOI | Web page | PDF ]
[Dow17c]
G. Dowek. Models and termination of proof reduction in the λΠ-calculus modulo theory. In Proceedings of the 44th International Colloquium on Automata, Languages and Programming (ICALP'17), volume 80 of Leibniz International Proceedings in Informatics, pages 109:1--109:14, Warsaw, Poland, July 2017. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.ICALP.2017.109.
BibTex | DOI | Web page | PDF ]
[JS17]
J.-P. Jouannaud and P.-Y. Strub. Coq without Type Casts: A Complete Proof of Coq Modulo Theory. In Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'17), volume 46 of EPiC Series in Computing, pages 474--489, Maun, Botswana, May 2017. EasyChair.
BibTex | Web page | PDF ]
[Gil17a]
F. Gilbert. Automated Constructivization of Proofs. In Proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'17), Lecture Notes in Computer Science, pages 480--495, Uppsala, Sweden, April 2017. Springer.
doi: 10.1007/978-3-662-54458-7_28.
BibTex | DOI | Web page | PDF ]
[Dow17b]
G. Dowek. Lineal: A linear-algebraic Lambda-calculus. Logical Methods in Computer Science, 13(1):1--33, March 2017.
doi: 10.23638/LMCS-13(1:8)2017.
BibTex | DOI | Web page | PDF ]
[AM17]
P. Arrighi and S. Martiel. Quantum causal graph dynamics. Physical Review D, 96(2), 2017.
BibTex | PDF ]
[AD17]
S. Abiteboul and G. Dowek. Le temps des algorithmes. Editions Le Pommier, 2017.
BibTex | Web page ]
[DD17]
A. Díaz-Caro and G. Dowek. Typing Quantum Superpositions and Measurement. In Proceedings of the 6th International Conference on Theory and Practice of Natural Computing (TPNC'17), volume 10687 of Lecture Notes in Computer Science, pages 281--293, Prague, Czech Republic, 2017. Springer.
doi: 10.1007/978-3-319-71069-3_22.
BibTex | DOI | Web page ]
[Dow17d]
G. Dowek. Rules and derivations in an elementary logic course. IfCoLoG Journal of Logics and their Applications, 4(1):21--32, 2017. Special Issue: Tools for Teaching Logic.
BibTex | PDF ]
[AD16b]
P. Arrighi and G. Dowek. What is the Planck constant the magnitude of? preprint, December 2016.
BibTex | Web page | PDF ]
[Hal16a]
P. Halmagrand. Automated Deduction and Proof Certification for the B Method. Thèse de doctorat, Conservatoire National Des Arts et Métiers, Paris, December 2016.
BibTex | Web page ]
[Cau16b]
R. Cauderlier. Object-Oriented Mechanisms for Interoperability between Proof Systems. Thèse de doctorat, Conservatoire National Des Arts et Métiers, Paris, October 2016.
BibTex | Web page | PDF ]
[Hal16b]
P. Halmagrand. Soundly Proving B Method Formulae Using Typed Sequent Calculus. In Proceedings of the 13th International Colloquium on Theoretical Aspects of Computing (ICTAC'16), volume 9965 of Lecture Notes in Computer Science, pages 196--213, Taipei, Taiwan, October 2016. Springer.
doi: 10.1007/978-3-319-46750-4_12.
BibTex | DOI | Web page | PDF ]
[CD16]
R. Cauderlier and C. Dubois. ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti. In Proceedings of the 13th International Colloquium on Theoretical Aspects of Computing (ICTAC'16), volume 9965 of Lecture Notes in Computer Science, pages 459--468, Taipei, Taiwan, October 2016. Springer.
BibTex | Web page | PDF ]
[Thi16]
F. Thiré. Reverse engineering on arithmetic proofs. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, August 2016. 26 pages.
BibTex | Web page | PDF ]
[AMP16]
P. Arrighi, S. Martiel, and S. Perdrix. Reversible Causal Graph Dynamics. In 8th Conference on Reversible Computation (RC'16), volume 9720 of Lecture Notes in Computer Science, pages 73--88, Bologna, Italy, July 2016. Springer.
doi: 10.1007/978-3-319-40578-0_5.
BibTex | DOI | Web page ]
[Cau16a]
R. Cauderlier. A Rewrite System for Proof Constructivization. In Proceedings of the 11th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'16), pages 2:1--2:7, Porto, Portugal, June 2016. ACM Press.
doi: 10.1007/978-3-319-40578-0_5.
BibTex | DOI | Web page | PDF ]
[AD16a]
P. Arrighi and G. Dowek. Free fall and cellular automata. In Proceedings of the 11th International Workshop on Developments in Computational Models (DCM'15), volume 204 of Electronic Proceedings in Theoretical Computer Science, pages 1--10, Cali, Colombia, March 2016.
doi: 10.4204/EPTCS.204.1.
BibTex | DOI | Web page ]
[DD16]
A. Díaz-Caro and G. Dowek. Quantum superpositions and projective measurement in the lambda calculus. Research Report 1601.04294, Computing Research Repository, January 2016. 22 pages.
BibTex | Web page | PDF ]
[ADJL16a]
A. Assaf, G. Dowek, J.-P. Jouannaud, and J. Liu. Encoding Proofs in Dedukti: the case of Coq proofs. In Preliminary Proceedings of the 1st International Workshop on Hammers for Type Theories (HaTT'16), Coimbra, Portugal, 2016.
BibTex | Web page | PDF ]
[ADJL16b]
A. Assaf, G. Dowek, J.-P. Jouannaud, and J. Liu. Untyped Confluence in Dependent Type Theories. In Proceedings of the 8th International Workshop on Higher-Order Rewriting (HOR'16), Porto, Portugal, 2016.
BibTex | Web page | PDF ]
[ABC+16]
A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek, C. Dubois, F. Gilbert, P. Halmagrand, O. Hermant, and R. Saillard. Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system. In Proceedings of the 22nd International Conference on Types for Proofs and Programs (TYPES'16), volume 97 of Leibniz International Proceedings in Informatics, Novi Sad, Serbia, 2016. Leibniz-Zentrum für Informatik. To appear.
BibTex ]
[Dow16]
G. Dowek. Rules and derivations in an elementary logic course. preprint, January 2016.
BibTex | Web page | PDF ]

This file was generated by bibtex2html 1.98.

About LSV