David Baelde

Adrien Koutsos

Joseph Lallemand

Proceedings of the 38th Annual ACM/IEEE Symposium on Logic in Computer Science, 2023

Proving Unlinkability Using ProVerif Through Desynchronised Bi-Processes.

[BibT_eX]

[DOI]

Alexandre Debant

Proceedings of the 36th IEEE Computer Security Foundations Symposium, 2023

2022

Bouncing Threads for Circular and Non-Wellfounded Proofs: Towards Compositionality with Circular Proofs.

[BibT_eX]

[DOI]

Proceedings of the LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2, 2022

Cracking the Stateful Nut: Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant.

[BibT_eX]

[DOI]

Proceedings of the 35th IEEE Computer Security Foundations Symposium, 2022

2021

An Interactive Prover for Protocol Verification in the Computational Model.

[BibT_eX]

[DOI]

Proceedings of the 42nd IEEE Symposium on Security and Privacy, 2021

Contributions to the Verification of Cryptographic Protocols. (Contributions à la Vérification des Protocoles Cryptographiques).

[BibT_eX]

[DOI]

, 2021

2020

Bouncing threads for infinitary and circular proofs.

[BibT_eX]

[DOI]

CoRR, 2020

A Method for Proving Unlinkability of Stateful Protocols.

[BibT_eX]

[DOI]

Solène Moreau

Proceedings of the 33rd IEEE Computer Security Foundations Symposium, 2020

2019

A special issue on structural proof theory, automated reasoning and computation in celebration of Dale Miller's 60th birthday.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2019

A method for unbounded verification of privacy-type properties.

[BibT_eX]

[DOI]

J. Comput. Secur., 2019

Decidable XPath Fragments in the Real World.

[BibT_eX]

[DOI]

Anthony Lick

Proceedings of the 38th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, 2019

2018

A Hypersequent Calculus with Clusters for Tense Logic over Ordinals.

[BibT_eX]

[DOI]

Anthony Lick

Proceedings of the 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2018

POR for Security Protocol Equivalences - Beyond Action-Determinism.

[BibT_eX]

[DOI]

Proceedings of the Computer Security, 2018

A Hypersequent Calculus with Clusters for Linear Frames.

[BibT_eX]

[DOI]

Anthony Lick

Proceedings of the Advances in Modal Logic 12, 2018

2017

A Reduced Semantics for Deciding Trace Equivalence.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2017

Preface.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2017

Symbolic Verification of Privacy-Type Properties for Security Protocols with XOR.

[BibT_eX]

[DOI]

Proceedings of the 30th IEEE Computer Security Foundations Symposium, 2017

2016

A Method for Verifying Privacy-Type Properties: The Unbounded Case.

[BibT_eX]

[DOI]

Proceedings of the IEEE Symposium on Security and Privacy, 2016

Towards Completeness via Proof Search in the Linear Time μ-calculus: The case of Büchi inclusions.

[BibT_eX]

[DOI]

Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

A Sequent Calculus for a Modal Logic on Finite Data Trees.

[BibT_eX]

[DOI]

Simon Lunel

Proceedings of the 25th EACSL Annual Conference on Computer Science Logic, 2016

Infinitary Proof Theory: the Multiplicative Additive Case.

[BibT_eX]

[DOI]

Amina Doumane

Alexis Saurin

Proceedings of the 25th EACSL Annual Conference on Computer Science Logic, 2016

2015

Least and Greatest Fixed Points in Ludics.

[BibT_eX]

[DOI]

Amina Doumane

Alexis Saurin

Proceedings of the 24th EACSL Annual Conference on Computer Science Logic, 2015

Partial Order Reduction for Security Protocols.

[BibT_eX]

[DOI]

Proceedings of the 26th International Conference on Concurrency Theory, 2015

2014

Abella: A System for Reasoning about Relational Specifications.

[BibT_eX]

[DOI]

J. Formaliz. Reason., 2014

A Reduced Semantics for Deciding Trace Equivalence Using Constraint Systems.

[BibT_eX]

[DOI]

Proceedings of the Principles of Security and Trust - Third International Conference, 2014

2012

Least and Greatest Fixed Points in Linear Logic.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2012

Combining Deduction Modulo and Logics of Fixed-Point Definitions.

[BibT_eX]

[DOI]

Gopalan Nadathur

Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

Towards Provably Robust Watermarking.

[BibT_eX]

[DOI]

Pierre Courtieu

David Gross-Amblard

Christine Paulin-Mohring

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

2011

Liquidsoap: A High-Level Programming Language for Multimedia Streaming.

[BibT_eX]

[DOI]

Romain Beauxis

Samuel Mimram

Proceedings of the SOFSEM 2011: Theory and Practice of Computer Science, 2011

2010

Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search

[BibT_eX]

[DOI]

Zachary Snow

Gopalan Nadathur

CoRR, 2010

A meta-programming approach to realizing dependently typed logic programming.

[BibT_eX]

[DOI]

Zachary Snow

Gopalan Nadathur

Proceedings of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2010

Focused Inductive Theorem Proving.

[BibT_eX]

[DOI]

Dale Miller

Zachary Snow

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2009

On the Proof Theory of Regular Fixed Points.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2009

2008

On the Expressivity of Minimal Generic Quantification.

[BibT_eX]

[DOI]

Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, 2008

2007

Least and Greatest Fixed Points in Linear Logic.

[BibT_eX]

[DOI]