Stéphane Lengrand

Steve Lu

Rafail Ostrovsky

Vitor Pereira

IACR Cryptol. ePrint Arch., 2023

QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment.

[BibT_eX]

[DOI]

Christophe Vauthier

Proceedings of the Automated Deduction - CADE 29, 2023

2022

Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs.

[BibT_eX]

[DOI]

J. Autom. Reason., 2022

CDSAT for Nondisjoint Theories with Shared Predicates: Arrays With Abstract Length.

[BibT_eX]

[DOI]

Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022), 2022

2021

Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head.

[BibT_eX]

[DOI]

José Carlos Bacelar Almeida

Hugo Pacheco

Vitor Pereira

IACR Cryptol. ePrint Arch., 2021

Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head.

[BibT_eX]

[DOI]

Manuel Barbosa

Karim Eldefrawy

Hugo Pacheco

Vitor Pereira

CoRR, 2021

Semantic parsing of geometry statements using supervised machine learning on synthetic data.

[BibT_eX]

[DOI]

Salwa Tabet Gonzalez

Julien Narboux

Proceedings of the Joint Proceedings of the FMM, FVPS, MathUI,NatFoM, and OpenMath Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2021 co-located with the 14th Conference on Intelligent Computer Mathematics (CICM 2021), Virtual Event, Timisoara, Romania, July 26, 2021

2020

Tight typings and split bounds, fully developed.

[BibT_eX]

[DOI]

Beniamino Accattoli

J. Funct. Program., 2020

Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness.

[BibT_eX]

[DOI]

J. Autom. Reason., 2020

Solving bitvectors with MCSAT: explanations from bits and pieces (long version).

[BibT_eX]

[DOI]

Dejan Jovanovic

Bruno Dutertre

CoRR, 2020

Solving Bitvectors with MCSAT: Explanations from Bits and Pieces.

[BibT_eX]

[DOI]

Dejan Jovanovic

Bruno Dutertre

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

A Proof-Theoretic Perspective on SMT-Solving for Intuitionistic Propositional Logic.

[BibT_eX]

[DOI]

Camillo Fiorentini

Rajeev Goré

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

2018

Tight typings and split bounds.

[BibT_eX]

[DOI]

Beniamino Accattoli

Proc. ACM Program. Lang., 2018

Proofs in conflict-driven theory combination.

[BibT_eX]

[DOI]

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2017

An MCSAT treatment of Bit-Vectors.

[BibT_eX]

[DOI]

Dejan Jovanovic

Proceedings of the 15th International Workshop on Satisfiability Modulo Theories affiliated with the International Conference on Computer-Aided Verification (CAV 2017), Heidelberg, Germany, July 22, 2017

Satisfiability Modulo Theories and Assignments.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 26, 2017

2016

Special Issue on Computational Logic in Honour of Roy Dyckhoff.

[BibT_eX]

[DOI]

Didier Galmiche

J. Log. Comput., 2016

2015

Realisability semantics of abstract focussing, formalised.

[BibT_eX]

[DOI]

Proceedings of the Proceedings First International Workshop on Focusing, 2015

Axiomatic Constraint Systems for Proof Search Modulo Theories.

[BibT_eX]

[DOI]

Damien Rouhling

Jean-Marc Notin

Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

2014

Axiomatisation of constraint systems to specify a tableaux calculus modulo theories.

[BibT_eX]

[DOI]

Damien Rouhling

Jean-Marc Notin

CoRR, 2014

Polarities & Focussing: a journey from Realisability to Automated Reasoning.

[BibT_eX]

[DOI]

CoRR, 2014

Polarities & Focussing: a journey from Realisability to Automated Reasoning.

[BibT_eX]

[DOI]

, 2014

2013

Sequent Calculi with procedure calls

[BibT_eX]

[DOI]

CoRR, 2013

Non-idempotent intersection types and strong normalisation.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2013

A simple presentation of the effective topos.

[BibT_eX]

[DOI]

CoRR, 2013

Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture.

[BibT_eX]

[DOI]

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

A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus.

[BibT_eX]

[DOI]

Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, 2013

2012

Two simulations about DPLL(T)

[BibT_eX]

[DOI]

CoRR, 2012

A sequent calculus with procedure calls

[BibT_eX]

[DOI]

CoRR, 2012

2011

A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems

[BibT_eX]

[DOI]

James McKinna

Log. Methods Comput. Sci., 2011

Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computational Structures, 2011

Filter Models: Non-idempotent Intersection Types, Orthogonality and Polymorphism.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 2011

2009

The lambda-context calculus (extended version).

[BibT_eX]

[DOI]

Murdoch James Gabbay

Inf. Comput., 2009

2008

Termination of lambda-calculus with the extra Call-By-Value rule known as assoc

[BibT_eX]

[DOI]

CoRR, 2008

Classical Fomega, orthogonality and symmetric candidates.

[BibT_eX]

[DOI]

Alexandre Miquel

Ann. Pure Appl. Log., 2008

Strong Normalisation of Cut-Elimination That Simulates beta-Reduction.

[BibT_eX]

[DOI]

Kentaro Kikuchi

Proceedings of the Foundations of Software Science and Computational Structures, 2008

2007

Call-by-Value lambda-calculus and LJQ.

[BibT_eX]

[DOI]

J. Log. Comput., 2007

Resource operators for lambda-calculus.

[BibT_eX]

[DOI]

Inf. Comput., 2007

The lambda-context Calculus.

[BibT_eX]

[DOI]

Murdoch Gabbay

Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2007

2006

A Sequent Calculus for Type Theory.

[BibT_eX]

[DOI]

James McKinna

Proceedings of the Computer Science Logic, 20th International Workshop, 2006

LJQ: A Strongly Focused Calculus for Intuitionistic Logic.

[BibT_eX]

[DOI]

Proceedings of the Logical Approaches to Computational Barriers, 2006

Strong Cut-Elimination Systems for Hudelmaier's Depth-Bounded Sequent Calculus for Implicational Logic.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005

Extending the Explicit Substitution Paradigm.

[BibT_eX]

[DOI]

Proceedings of the Term Rewriting and Applications, 16th International Conference, 2005

The Language chi: Circuits, Computations and Classical Logic.

[BibT_eX]

[DOI]

Steffen van Bakel

Pierre Lescanne

Proceedings of the Theoretical Computer Science, 9th Italian Conference, 2005

2004

Intersection types for explicit substitutions.

[BibT_eX]

[DOI]

Mariangiola Dezani-Ciancaglini

Pierre Lescanne

Daniel J. Dougherty

Steffen van Bakel

Inf. Comput., 2004

2003

Call-by-value, call-by-name, and strong normalization for the classical sequent calculus.

[BibT_eX]

[DOI]

Proceedings of the 3rd International Workshop on Reduction Strategies in Rewriting and Programming, 2003

2002

An Improved System of Intersection Types for Explicit Substitutions.

[BibT_eX]

[DOI]

Daniel J. Dougherty