Publications : DEDUCTEAM
-
[HB21]
-
G. Hondet and F. Blanqui.
Encoding of Predicate Subtyping with Proof Irrelevance in the
ΛΠ-Calculus Modulo Theory.
In Proceedings of the 26th International Conference on Types
for Proofs and Programs (TYPES'20), volume 188 of Leibniz International
Proceedings in Informatics, pages 6:1--6:18, Turin, Italy, 2021.
Leibniz-Zentrum für Informatik.
doi:
10.4230/LIPIcs.TYPES.2020.6.
[ BibTex |
DOI |
Web page |
PDF ]
-
[DM21]
-
B. Dinis and É. Miquey.
Realizability with stateful computations for nonstandard
analysis.
In Proceedings of the 29th Annual EACSL Conference on
Computer Science Logic (CSL'21), Leibniz International Proceedings in
Informatics, pages 19:1--19:23, Ljubljana, Slovenia, January 2021.
Leibniz-Zentrum für Informatik.
doi:
10.4230/LIPIcs.CSL.2021.19.
[ BibTex |
DOI |
Web page |
PDF ]
-
[Thi20]
-
F. Thiré.
Meta-theory of Cumulative Types Systems and their embeddings to
the ΛΠ-calculus modulo theory.
Thèse de doctorat, École Normale Supérieure Paris-Saclay,
France, December 2020.
[ BibTex |
Web page |
PDF ]
-
[Gen20a]
-
G. Genestier.
Dependently-Typed Termination and Embedding of Extensional
Universe-Polymorphic Type Theory using Rewriting.
Thèse de doctorat, École Normale Supérieure Paris-Saclay,
France, December 2020.
[ BibTex ]
-
[DD20]
-
A. Díaz-Caro and G. Dowek.
Extensional proofs in a propositional logic modulo
isomorphisms.
Research Report 2002.03762v3, Computing Research Repository, July
2020.
[ BibTex |
Web page |
PDF ]
-
[HM20]
-
H. Herbelin and É. Miquey.
A calculus of expandable stores.
Continuation-and-environment-passing style translations.
In Proceedings of the 35th Annual ACM/IEEE Symposium on
Logic In Computer Science (LICS'20), pages 564--577, Saarbrucken,
Germany, July 2020. IEEE Press.
[ BibTex |
Web page ]
-
[Bla20]
-
F. Blanqui.
Type safety of rewriting rules in dependent types.
In Proceedings of the 5th International Conference on Formal
Structures for Computation and Deduction (FSCD'20), Leibniz International
Proceedings in Informatics, Paris, France, June 2020. Leibniz-Zentrum für
Informatik.
doi:
10.4230/LIPIcs.FSCD.2020.13.
[ BibTex |
DOI |
Web page |
PDF ]
-
[Gen20b]
-
G. Genestier.
Encoding Agda Programs using Rewriting.
In Proceedings of the 5th International Conference on Formal
Structures for Computation and Deduction (FSCD'20), Leibniz International
Proceedings in Informatics, Paris, France, June 2020. Leibniz-Zentrum für
Informatik.
doi:
10.4230/LIPIcs.FSCD.2020.31.
[ BibTex |
DOI |
Web page |
PDF ]
-
[HB20]
-
G. Hondet and F. Blanqui.
The new rewriting engine of Dedukti (System Description).
In Proceedings of the 5th International Conference on Formal
Structures for Computation and Deduction (FSCD'20), Leibniz International
Proceedings in Informatics, pages 35:1--35:16, Paris, France, June 2020.
Leibniz-Zentrum für Informatik.
doi:
10.4230/LIPIcs.FSCD.2020.35.
[ BibTex |
DOI |
Web page |
PDF ]
-
[AMP20]
-
P. Arrighi, S. Martiel, and S. Perdrix.
Reversible causal graph dynamics: invertibility, block
representation, vertex-preservation.
Natural Computing, 19(1):157--178, 2020.
doi:
10.1007/s11047-019-09768-0.
[ BibTex |
DOI |
Web page |
PDF ]
-
[BM20]
-
B. Barras and V. Maestracci.
Implementation of Two Layers Type Theory in Dedukti and
Application to Cubical Type Theory.
In Proceedings of the 15th International Workshop on Logical
Frameworks and Meta-Languages: Theory and Practice (LFMTP'20),
pages 54--67, Paris, France, 2020. ACM Press.
doi:
10.4204/EPTCS.332.4.
[ BibTex |
DOI |
Web page |
PDF ]
-
[BJO20]
-
F. Blanqui, J. Jouannaud, and M. Okada.
Corrigendum to Inductive-data-type systems [Theoret.
Comput. Sci. 272 (1-2) (2002) 41-68].
Theoretical Computer Science, 817:81--82, 2020.
doi:
10.1016/j.tcs.2018.01.010.
[ BibTex |
DOI |
Web page ]
-
[ABF20]
-
P. Arrighi, C. Bény, and T. Farrelly.
A quantum cellular automaton for one-dimensional QED.
Quantum Information Processing, 19(88), 2020.
doi:
10.1007/s11128-019-2555-4.
[ BibTex |
DOI |
Web page ]
-
[MA20]
-
G. D. Molfetta and P. Arrighi.
A quantum walk with both a continuous-time limit and a
continuous-spacetime limit.
Quantum Information Processing, 19(47), 2020.
doi:
10.1007/s11128-019-2549-2.
[ BibTex |
DOI |
Web page ]
-
[JLDJ20]
-
Y. Jiang, J. Liu, G. Dowek, and K. Ji.
Towards Combining Model Checking and Proof Checking.
The Computer Journal, 62(9):1365--1402, 2020.
doi:
10.1093/comjnl/bxy112.
[ BibTex |
DOI |
PDF ]
-
[BBC+20]
-
G. Burel, G. Bury, R. Cauderlier, D. Delahaye, P. Halmagrand,
and O. Hermant.
First-Order Automated Reasoning with Theories: When Deduction
Modulo Theory Meets Practice.
Journal of Automated Reasoning, 64:1001--1050, 2020.
doi:
10.1007/s10817-019-09533-z.
[ BibTex |
DOI |
Web page |
PDF ]
-
[Gri19]
-
E. Grienenberger.
Concept alignment in Logipedia - Alignement of logical
connectives between HOL Light and Dedukti.
Rapport de Master, Master Parisien de Recherche en
Informatique, Paris, France, September 2019.
[ BibTex ]
-
[EHBB19]
-
M. El Haddad, G. Burel, and F. Blanqui.
Ekstrakto: A tool to reconstruct Dedukti proofs from
TSTP files (extended abstract).
In Proceedings of the 6th Workshop on Proof eXchange for
Theorem Proving (PxTP'19), volume 301 of Electronic Proceedings in
Theoretical Computer Science, pages 27--35, Natal, Brazil, August 2019.
[ BibTex |
Web page |
PDF ]
-
[Gen19]
-
G. Genestier.
SizeChangeTool: A Termination Checker for
Rewriting Dependent Types.
In Proceedings of the 10th International Workshop on
Higher-Order Rewriting (HOR'19), pages 14--19, Dortmund, Germany,
June 2019.
[ BibTex |
PDF ]
-
[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 ]
-
[Bur19]
-
G. Bury.
Integrating rewriting, tableau and superposition into SMT.
Thèse de doctorat, École Normale Supérieure Paris-Saclay,
France, May 2019.
[ BibTex |
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 ]
-
[DDR19]
-
A. Díaz-Caro, G. Dowek, and J. P. Rinaldi.
Two linearities for quantum computing in the lambda calculus.
Biosystems, 186, 2019.
doi:
10.1016/j.biosystems.2019.104012.
[ BibTex |
DOI |
Web page ]
-
[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 ]
-
[BG18]
-
F. Blanqui and G. Genestier.
Termination of λΠ modulo rewriting using the
size-change principle.
In Proceedings of the 16th International Workshop on
Termination (WST'18), pages 10--14, Oxford, UK, July 2018.
[ BibTex |
PDF ]
-
[Thi18]
-
F. Thiré.
Sharing a Library between Proof Assistants: Reaching
out to the HOL Family *.
In Proceedings of the 13th International Workshop on Logical
Frameworks and Meta-Languages: Theory and Practice (LFMTP'18),
pages 57--71, Oxford, UK, July 2018. ACM Press.
doi:
10.4204/EPTCS.274.4.
[ 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.