-
Compact Proof Certificates for Linear Logic
International audience -
Two simulations about DPLL(T)
In this paper we relate different formulations of the DPLL(T ) procedure. The first formulation is based on a system of rewrite rules, which we denote DPLL(T ). The... -
Resource control and strong normalisation (old version)
We introduce the resource control cube, a system consisting of eight intuitionistic lambda calculi with either implicit or explicit control of resources and with... -
A sequent calculus with procedure calls
The proof of Cut-elimination is unfortunately bugged. It is repaired in "Sequent Calculi with procedure calls", hal-00779199, v4 -
Classical call-by-need sequent calculi : The unity of semantic artifacts
International audience -
Resource control and strong normalisation
We introduce the \emph{resource control cube}, a system consisting of eight intuitionistic lambda calculi with either implicit or explicit control of resources and... -
A journey through resource control lambda calculi and explicit substitution u...
In this paper we invite the reader to a journey through three lambda calculi with resource control: the lambda calculus, the sequent lambda calculus, and the lambda... -
Sequent Calculi with procedure calls
In this paper, we introduce two focussed sequent calculi, LKp(T) and LK+(T), that are based on Miller-Liang's LKF system for polarised classical logic. The novelty is... -
Syntax and Models of a non-Associative Composition of Programs and Proofs
The thesis is a contribution to the understanding of the nature, role, and mechanisms of polarisation in programming languages, proof theory and categorical models.... -
Automated reasoning techniques as proof-search in sequent calculus
Version of thesis at time of defense. -
Structural Interactions and Absorption of Structural Rules in BI Sequent Calc...
Development of a contraction-free BI sequent calculus, be it in the sense of G3i or G4i, has not been successful in literature. We address the open problem by... -
Proof Systems for Intuitionistic Provability in Linear Logic
Colloque avec actes et comité de lecture. -
From multiple sequent for Additive Linear Logic to decision procedures for Fr...
Editor S. Adian. Article dans revue scientifique avec comité de lecture. -
Sequent Calculus Viewed Modulo
Colloque avec actes et comité de lecture. internationale. -
On the Algebra of Structural Contexts
Article dans revue scientifique avec comité de lecture.
