Publications : David BAELDE
-
[BDJ+21]
-
D. Baelde, S. Delaune, C. Jacomme, A. Koutsos, and
S. Moreau.
An Interactive Prover for Protocol Verification in the
Computational Model.
In Proceedings of the 42nd IEEE Symposium on Security and Privacy
(S&P'21), online, May 2021. IEEE Press.
To appear.
[ BibTex |
Web page |
PDF ]
-
[Bae21]
-
D. Baelde.
Contributions to the Verification of Cryptographic
Protocols.
Mémoire d'habilitation, École Normale Supérieure
Paris-Saclay, France, February 2021.
[ BibTex |
Web page |
PDF ]
-
[BDM20]
-
D. Baelde, S. Delaune, and S. Moreau.
A Method for Proving Unlinkability of Stateful Protocols.
In Proceedings of the 33rd IEEE Computer Security
Foundations Symposium (CSF'20), pages 169--183, Boston, MA, USA, July
2020. IEEE Computer Society Press.
[ BibTex |
Web page ]
-
[BFNS20]
-
D. Baelde, A. P. Felty, G. Nadathur, and A. Saurin.
A special issue on structural proof theory, automated reasoning
and computation in celebration of Dale Miller's 60th birthday.
Mathematical Structures in Computer Science, 29(8):1007--1008, 2020.
doi:
10.1017/S0960129519000136.
[ BibTex |
DOI ]
-
[BLS19]
-
D. Baelde, A. Lick, and S. Schmitz.
Decidable XPath Fragments in the Real World.
In Proceedings of the 38th Annual ACM
SIGACT-SIGMOD-SIGART Symposium on Principles of Database
Systems (PODS'19), pages 285--302, Amsterdam, Netherlands, June-July
2019. ACM Press.
doi:
10.1145/3294052.3319685.
[ BibTex |
DOI |
Web page ]
-
[HBD19]
-
L. Hirschi, D. Baelde, and S. Delaune.
A method for unbounded verification of privacy-type properties.
Journal of Computer Security, 27(3):277--342, 2019.
doi:
10.3233/JCS-171070.
[ BibTex |
DOI |
Web page |
PDF ]
-
[BLS18b]
-
D. Baelde, A. Lick, and S. Schmitz.
A Hypersequent Calculus with Clusters for Tense Logic over
Ordinals.
In Proceedings of the 38th Conference on Foundations of
Software Technology and Theoretical Computer Science (FSTTCS'18),
volume 122 of Leibniz International Proceedings in Informatics, pages
15:1--15:19, Ahmedabad, India, December 2018. Leibniz-Zentrum für
Informatik.
doi:
10.4230/LIPIcs.FSTTCS.2018.15.
[ BibTex |
DOI |
Web page |
PDF ]
-
[BDH18]
-
D. Baelde, S. Delaune, and L. Hirschi.
POR for Security Protocol Equivalences - Beyond
Action-Determinism.
In Proceedings of the 23rd European Symposium on Research in
Computer Security (ESORICS'18), volume 11098 of Lecture Notes in
Computer Science, pages 385--405, Barcelona, Spain, September 2018. Springer.
doi:
10.1007/978-3-319-99073-6_19.
[ BibTex |
DOI |
Web page ]
-
[BLS18a]
-
D. Baelde, A. Lick, and S. Schmitz.
A Hypersequent Calculus with Clusters for Linear Frames.
In Proceedings of the 10th Conference on Advances in Modal
Logics (AiML'18), pages 36--55, Bern, Switzerland, August 2018. College
Publications.
[ BibTex |
Web page ]
-
[BDGK17]
-
D. Baelde, S. Delaune, I. Gazeau, and S. Kremer.
Symbolic Verification of Privacy-Type Properties for Security
Protocols with XOR.
In Proceedings of the 30th IEEE Computer Security
Foundations Symposium (CSF'17), pages 234--248, Santa Barbara,
California, USA, August 2017. IEEE Computer Society Press.
doi:
10.1109/CSF.2017.22.
[ BibTex |
DOI |
Web page |
PDF ]
-
[BCMW17]
-
D. Baelde, A. Carayol, R. Matthes, and I. Walukiewicz.
Preface: Special Issue of Fixed Points in Computer Science
(FICS'13).
Fundamenta Informaticae, 150(3-4):i--ii, 2017.
doi:
10.3233/FI-2017-1468.
[ BibTex |
DOI |
Web page ]
-
[BDH17]
-
D. Baelde, S. Delaune, and L. Hirschi.
A Reduced Semantics for Deciding Trace Equivalence.
Logical Methods in Computer Science, 13(2:8):1--48, 2017.
doi:
10.23638/LMCS-13(2:8)2017.
[ BibTex |
DOI |
Web page |
PDF ]
-
[DBS16]
-
A. Doumane, D. Baelde, and A. Saurin.
Infinitary proof theory: the multiplicative additive case.
In Proceedings of the 25th Annual EACSL Conference on
Computer Science Logic (CSL'16), volume 62 of Leibniz International
Proceedings in Informatics, pages 42:1--42:17, Marseille, France, September
2016. Leibniz-Zentrum für Informatik.
doi:
10.4230/LIPIcs.CSL.2016.42.
[ BibTex |
DOI ]
-
[BLS16]
-
D. Baelde, S. Lunel, and S. Schmitz.
A Sequent Calculus for a Modal Logic on Finite Data Trees.
In Proceedings of the 25th Annual EACSL Conference on
Computer Science Logic (CSL'16), volume 62 of Leibniz International
Proceedings in Informatics, pages 32:1--32:16, Marseille, France, September
2016. Leibniz-Zentrum für Informatik.
doi:
10.4230/LIPIcs.CSL.2016.32.
[ BibTex |
DOI |
Web page ]
-
[DBHS16]
-
A. Doumane, D. Baelde, L. Hirschi, and A. Saurin.
Towards Completeness via Proof Search in the Linear Time
μ-calculus.
In Proceedings of the 31st Annual ACM/IEEE Symposium on
Logic In Computer Science (LICS'16), pages 377--386, New York City,
USA, July 2016. ACM Press.
doi:
10.1145/2933575.2933598.
[ BibTex |
DOI |
Web page |
PDF ]
-
[HBD16]
-
L. Hirschi, D. Baelde, and S. Delaune.
A method for verifying privacy-type properties: the unbounded
case.
In Proceedings of the 37th IEEE Symposium on Security and
Privacy (S&P'16), pages 564--581, San Jose, California, USA, May 2016.
IEEECSP.
doi:
10.1109/SP.2016.40.
[ BibTex |
DOI |
Web page |
PDF ]
-
[BDS15]
-
D. Baelde, A. Doumane, and A. Saurin.
Least and Greatest Fixed Points in Ludics.
In Proceedings of the 24th Annual EACSL Conference on
Computer Science Logic (CSL'15), volume 41 of Leibniz International
Proceedings in Informatics, pages 549--566, Berlin, Germany, September 2015.
Leibniz-Zentrum für Informatik.
doi:
10.4230/LIPIcs.CSL.2015.549.
[ BibTex |
DOI |
Web page |
PDF ]
-
[BDH15]
-
D. Baelde, S. Delaune, and L. Hirschi.
Partial Order Reduction for Security Protocols.
In Proceedings of the 26th International Conference on
Concurrency Theory (CONCUR'15), volume 42 of Leibniz International
Proceedings in Informatics, pages 497--510, Madrid, Spain, September 2015.
Leibniz-Zentrum für Informatik.
doi:
10.4230/LIPIcs.CONCUR.2015.497.
[ BibTex |
DOI |
Web page |
PDF ]
-
[BDK15]
-
D. Baelde, S. Delaune, and S. Kremer.
Decision procedures for equivalence based properties
(part II).
Deliverable VIP 3.2 (ANR-11-JS02-0006), September 2015.
9 pages.
[ BibTex |
Web page |
PDF ]
-
[BDH14]
-
D. Baelde, S. Delaune, and L. Hirschi.
A reduced semantics for deciding trace equivalence using
constraint systems.
In Proceedings of the 3rd International Conference on
Principles of Security and Trust (POST'14), volume 8414 of Lecture
Notes in Computer Science, pages 1--21, Grenoble, France, April 2014.
Springer.
doi:
10.1007/978-3-642-54792-8_1.
[ BibTex |
DOI |
Web page |
PDF ]
-
[BCG+14]
-
D. Baelde, K. Chaudhuri, A. Gacek, D. Miller, G. Nadathur,
A. Tiu, and Y. Wang.
Abella: A System for Reasoning about Relational Specifications.
Journal of Formalized Reasoning, 7(2):1--89, 2014.
doi:
10.6092/issn.1972-5787/4650.
[ BibTex |
DOI |
Web page |
PDF ]
-
[BCGP12]
-
D. Baelde, P. Courtieu, D. Gross-Amblard, and
Ch. Paulin-Mohring.
Towards Provably Robust Watermarking.
In Proceedings of the Third International Conference on
Interactive Theorem Proving (ITP'12), volume 7406 of Lecture Notes in
Computer Science, pages 201--216, Princeton, New Jersey, USA, August 2012.
Springer.
doi:
10.1007/978-3-642-32347-8_14.
[ BibTex |
DOI |
Web page |
PDF ]
-
[BN12]
-
D. Baelde and G. Nadathur.
Combining Deduction Modulo and Logics of Fixed-Point
Definitions.
In Proceedings of the 27th Annual IEEE Symposium on Logic
in Computer Science (LICS'12), pages 105--114, Dubrovnik, Croatia, June
2012. IEEE Computer Society Press.
doi:
10.1109/LICS.2012.22.
[ BibTex |
DOI |
Web page |
PDF ]
-
[Bae12]
-
D. Baelde.
Least and greatest fixed points in linear logic.
ACM Transactions on Computational Logic, 13(1), January 2012.
doi:
10.1145/2071368.2071370.
[ BibTex |
DOI |
Web page |
PDF ]
-
[BBM11]
-
D. Baelde, R. Beauxis, and S. Mimram.
Liquidsoap: a High-Level Programming Language for Multimedia
Streaming.
In Proceedings of the 37th International Conference on Current
Trends in Theory and Practice of Computer Science (SOFSEM'11), volume 6543
of Lecture Notes in Computer Science, pages 99--110, Nový Smokovec,
Slovakia, January 2011. Springer.
doi:
10.1007/978-3-642-18381-2_8.
[ BibTex |
DOI |
Web page |
PDF ]
-
[SBN10]
-
Z. Snow, D. Baelde, and G. Nadathur.
A Meta-Programming Approach to Realizing Dependently Typed Logic
Programming.
In Proceedings of the 12th International ACM SIGPLAN
Conference on Principles and Practice of Declarative Programming
(PPDP'10), pages 187--198, Hagenberg, Austria, July 2010. ACM Press.
doi:
10.1145/1836089.1836113.
[ BibTex |
DOI |
Web page |
PDF ]
-
[BMS10]
-
D. Baelde, D. Miller, and Z. Snow.
Focused Inductive Theorem Proving.
In Proceedings of the 5th International Joint Conference on
Automated Reasoning (IJCAR'10), volume 6173 of Lecture Notes in
Artificial Intelligence, pages 278--292, Edinburgh, Scotland, UK, July 2010.
Springer-Verlag.
doi:
10.1007/978-3-642-14203-1_24.
[ BibTex |
DOI |
Web page |
PDF ]
-
[Bae09b]
-
D. Baelde.
On the proof theory of regular fixed points.
In Proceedings of the 18th International Workshop on Theorem
Proving with Analytic Tableaux and Related Methods (TABLEAUX'09),
volume 5607 of Lecture Notes in Artificial Intelligence, pages 93--107, Oslo,
Norway, July 2009. Springer.
doi:
10.1007/978-3-642-02716-1_8.
[ BibTex |
DOI |
Web page |
PDF ]
-
[Bae09a]
-
D. Baelde.
On the Expressivity of Minimal Generic Quantification.
In International Workshop on Logical Frameworks and
Meta-Languages: Theory and Practice (LFMTP'08), volume 228 of
Electronic Notes in Theoretical Computer Science, pages 3--19, Pittsburgh,
Pennsylvania, USA, January 2009. Elsevier Science Publishers.
doi:
10.1016/j.entcs.2008.12.113.
[ BibTex |
DOI |
Web page |
PDF ]
-
[BM08]
-
D. Baelde and S. Mimram.
De la webradio lambda à la λ-webradio.
In Actes des 19èmes Journées Francophones sur les
Langages Applicatifs (JFLA'08), pages 47--61, Étretat, France,
January 2008. INRIA.
[ BibTex |
Web page |
PDF ]
-
[BM07]
-
D. Baelde and D. Miller.
Least and greatest fixed points in linear logic.
In Proceedings of the 14th International Conference on Logic
for Programming, Artificial Intelligence, and Reasoning (LPAR'07),
volume 4790 of Lecture Notes in Artificial Intelligence, pages 92--106,
Yerevan, Armenia, October 2007. Springer.
doi:
10.1007/978-3-540-75560-9_9.
[ BibTex |
DOI |
Web page |
PDF ]
-
[BGM+07]
-
D. Baelde, A. Gacek, D. Miller, G. Nadathur, and A. Tiu.
The Bedwyr system for model checking over syntactic
expressions.
In Proceedings of the 21st International Conference on
Automated Deduction (CADE'07), volume 4603 of Lecture Notes in
Artificial Intelligence, pages 391--397, Bremen, Germany, July 2007.
Springer.
doi:
10.1007/978-3-540-73595-3_28.
[ BibTex |
DOI |
Web page |
PDF ]
This file was generated by
bibtex2html 1.98.