Author name cluster

Patrick Baillot

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

17 papers

2 author rows

CSL Conference 2025 Conference Paper

A Kleene Algebra with Tests for Union Bound Reasoning About Probabilistic Programs

Leandro Gomes 0001
Patrick Baillot
Marco Gaboardi

Kleene Algebra with Tests (KAT) provides a framework for algebraic equational reasoning about imperative programs. The recent variant Guarded KAT (GKAT) allows to reason on non-probabilistic properties of probabilistic programs. Here we introduce an extension of this framework called approximate GKAT (aGKAT), which equips GKAT with a partially ordered monoid (real numbers) enabling to express satisfaction of (deterministic) properties except with a probability up to a certain bound. This allows to represent in equational reasoning "à la KAT" proofs of probabilistic programs based on the union bound, a technique from basic probability theory. We show how a propositional variant of approximate Hoare Logic (aHL), a program logic for union bound, can be soundly encoded in our system aGKAT. We then illustrate the use of aGKAT with an example of accuracy analysis from the field of differential privacy.

Details

FSCD Conference 2024 Conference Paper

A Linear Type System for L^p-Metric Sensitivity Analysis

Victor Sannier
Patrick Baillot

When working in optimisation or privacy protection, one may need to estimate the sensitivity of computer programs, i. e. , the maximum multiplicative increase in the distance between two inputs and the corresponding two outputs. In particular, differential privacy is a rigorous and widely used notion of privacy that is closely related to sensitivity. Several type systems for sensitivity and differential privacy based on linear logic have been proposed in the literature, starting with the functional language Fuzz. However, they are either limited to certain metrics (L¹ and L^∞), and thus to the associated privacy mechanisms, or they rely on a complex notion of type contexts that does not interact well with operational semantics. We therefore propose a graded linear type system - inspired by Bunched Fuzz [{w}under et al. , 2023] - called Plurimetric Fuzz that handles L^p vector metrics (for 1 ≤ p ≤ +∞), uses standard type contexts, gives reasonable bounds on sensitivity, and has good metatheoretical properties. We also provide a denotational semantics in terms of metric complete partial orders, and translation mappings from and to Fuzz.

Details

TCS Journal 2020 Journal Article

Combining linear logic and size types for implicit complexity

Patrick Baillot
Alexis Ghyselen

Several type systems have been proposed to statically control the time complexity of lambda-calculus programs and characterize complexity classes such as FPTIME or FEXPTIME. A first line of research stems from linear logic and restricted versions of its! -modality controlling duplication. An instance of this is light linear logic for polynomial time computation [5]. A second approach relies on the idea of tracking the size increase between input and output, and together with a restricted recursion scheme, to deduce time complexity bounds. This second approach is illustrated for instance by non-size-increasing types [8]. However, both approaches suffer from limitations. The first one, that of linear logic, has a limited intensional expressivity, that is to say some natural polynomial time programs are not typable. As to the second approach it is essentially linear, more precisely it does not allow for a non-linear use of functional arguments. In the present work we incorporate both approaches into a common type system, in order to overcome their respective constraints. The source language we consider is a lambda-calculus with data-types and iteration, that is to say a variant of Gödel's system T. Our goal is to design a system for this language allowing both to handle non-linear functional arguments and to keep a good intensional expressivity. We illustrate our methodology by choosing the system of elementary linear logic (ELL) and combining it with a system of linear size types. We discuss the expressivity of this new type system, called sEAL, and prove that it gives a characterization of the complexity classes FPTIME and 2k-FEXPTIME, for k ≥ 0.

Details DOI

I&C Journal 2018 Journal Article

Characterizing polynomial and exponential complexity classes in elementary lambda-calculus

Patrick Baillot
Erika De Benedetti
Simona Ronchi Della Rocca

In this paper an implicit characterization of the complexity classes k - EXP and k - FEXP, for k ≥ 0, is given, by a type assignment system for a stratified λ-calculus, where types for programs are witnesses of the corresponding complexity class. Types are formulae of Elementary Linear Logic (ELL), and the hierarchy of complexity classes k - EXP is characterized by a hierarchy of types.

Details DOI

CSL Conference 2018 Conference Paper

Combining Linear Logic and Size Types for Implicit Complexity

Patrick Baillot
Alexis Ghyselen

Details

CSL Conference 2016 Conference Paper

Free-Cut Elimination in Linear Logic and an Application to a Feasible Arithmetic

Patrick Baillot
Anupam Das 0002

We prove a general form of 'free-cut elimination' for first-order theories in linear logic, yielding normal forms of proofs where cuts are anchored to nonlogical steps. To demonstrate the usefulness of this result, we consider a version of arithmetic in linear logic, based on a previous axiomatisation by Bellantoni and Hofmann. We prove a witnessing theorem for a fragment of this arithmetic via the `witness function method', showing that the provably convergent functions are precisely the polynomial-time functions. The programs extracted are implemented in the framework of 'safe' recursive functions, due to Bellantoni and Cook, where the! modality of linear logic corresponds to normal inputs of a safe recursive program.

Details

I&C Journal 2016 Journal Article

Higher-order interpretations and program complexity

Patrick Baillot
Ugo Dal Lago

Polynomial interpretations and their generalizations like quasi-interpretations have been used in the setting of first-order functional languages to design criteria ensuring statically some complexity bounds on programs [10]. This fits in the area of implicit computational complexity, which aims at giving machine-free characterizations of complexity classes. In this paper, we extend this approach to the higher-order setting. For that we consider simply-typed term rewriting systems [35], we define higher-order polynomial interpretations for them, and we give a criterion ensuring that a program can be executed in polynomial time. In order to obtain a criterion flexible enough to validate interesting programs using higher-order primitives, we introduce a notion of polynomial quasi-interpretations, coupled with a simple termination criterion based on linear types and path-like orders.

Details DOI

LPAR Conference 2015 Conference Paper

Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs

Patrick Baillot
Gilles Barthe
Ugo Dal Lago

Abstract We define a call-by-value variant of Gödel’s System \(\mathsf {T} \) with references, and equip it with a linear dependent type and effect system, called \(\mathsf {d}\ell \mathsf {T} \), that can estimate the complexity of programs, as a function of the size of their inputs. We prove that the type system is intentionally sound, in the sense that it over-approximates the complexity of executing the programs on a variant of the CEK abstract machine. Moreover, we define a sound and complete type inference algorithm which critically exploits the subrecursive nature of \(\mathsf {d}\ell \mathsf {T} \). Finally, we demonstrate the usefulness of \(\mathsf {d}\ell \mathsf {T} \) for analyzing the complexity of cryptographic reductions by providing an upper bound for the constructed adversary of the Goldreich-Levin theorem.

Details

I&C Journal 2015 Journal Article

On the expressivity of elementary linear logic: Characterizing Ptime and an exponential time hierarchy

Patrick Baillot

Elementary linear logic is a simple variant of linear logic due to Girard and which characterizes in the proofs-as-programs approach the class of elementary functions, that is to say functions computable in time bounded by a tower of exponentials of fixed height. Other systems like light and soft linear logics have then been defined to characterize in a similar way the more interesting complexity class of polynomial time functions, but at the price of either a more complicated syntax or of more sophisticated encodings. These logical systems can serve as the basis of type systems for λ-calculus ensuring polynomial time complexity bounds on well-typed terms. This paper aims at reviving interest in elementary linear logic by showing that, despite its simplicity, it can capture smaller complexity classes than that of elementary functions. For that we carry a detailed analysis of its normalization procedure, and study the complexity of functions represented by a given type. We then show that by considering a slight variant of this system, with type fixpoints and free weakening (elementary affine logic with fixpoints) we can characterize the complexity of functions of type! W ⊸! k + 2 B, where W and B are respectively types for binary words and booleans. The key point is a sharper study of the normalization bounds. We characterize in this way the class P of polynomial time predicates, and more generally the hierarchy of classes k - EXP, for k ≥ 0, where k - EXP is the union of DTIME ( 2 k n i ), for i ≥ 1.

Details DOI

CSL Conference 2012 Conference Paper

Higher-Order Interpretations and Program Complexity

Patrick Baillot
Ugo Dal Lago

Polynomial interpretations and their generalizations like quasi-interpretations have been used in the setting of first-order functional languages to design criteria ensuring statically some complexity bounds on programs. This fits in the area of implicit computational complexity, which aims at giving machine-free characterizations of complexity classes. In this paper, we extend this approach to the higher-order setting. For that we consider the notion of simply-typed term rewriting systems, we define higher-order polynomial interpretations for them and give a criterion ensuring that a program can be executed in polynomial time. In order to obtain a criterion flexible enough to validate interesting programs using higher-order primitives, we introduce a notion of polynomial quasi-interpretations, coupled with a simple termination criterion based on linear types and path-like orders.

Details

I&C Journal 2011 Journal Article

Light logics and optimal reduction: Completeness and complexity

Patrick Baillot
Paolo Coppola
Ugo Dal Lago

Typing of lambda-terms in elementary and light affine logic (EAL and LAL, respectively) has been studied for two different reasons: on the one hand the evaluation of typed terms using LAL (EAL, respectively) proof-nets admits a guaranteed polynomial (elementary, respectively) bound; on the other hand these terms can also be evaluated by optimal reduction using the abstract version of Lamping’s algorithm. The first reduction is global while the second one is local and asynchronous. We prove that for LAL (EAL, respectively) typed terms, Lamping’s abstract algorithm also admits a polynomial (elementary, respectively) bound. We also give a proof of its soundness and completeness (for EAL and LAL with type fixpoints), by using a simple geometry of interaction model (context semantics).

Details DOI

TCS Journal 2010 Journal Article

Linear logic by levels and bounded time complexity

Patrick Baillot
Damiano Mazza

We give a new characterization of elementary and deterministic polynomial time computation in linear logic through the proofs-as-programs correspondence. Girard’s seminal results, concerning elementary and light linear logic, achieve this characterization by enforcing a stratification principle on proofs, using the notion of depth in proof nets. Here, we propose a more general form of stratification, based on inducing levels in proof nets by means of indices, which allows us to extend Girard’s systems while keeping the same complexity properties. In particular, it turns out that Girard’s systems can be recovered by forcing depth and level to coincide. A consequence of the higher flexibility of levels with respect to depth is the absence of boxes for handling the paragraph modality. We use this fact to propose a variant of our polytime system in which the paragraph modality is only allowed on atoms, and which may thus serve as a basis for developing lambda-calculus type assignment systems with more efficient typing algorithms than existing ones.

Details DOI

I&C Journal 2009 Journal Article

Light types for polynomial time computation in lambda calculus

Patrick Baillot
Kazushige Terui

We present a polymorphic type system for lambda calculus ensuring that well-typed programs can be executed in polynomial time: dual light affine logic (DLAL). DLAL has a simple type language with a linear and an intuitionistic type arrow, and one modality. It corresponds to a fragment of light affine logic (LAL). We show that contrarily to LAL, DLAL ensures good properties on lambda-terms (and not only on proof-nets): subject reduction is satisfied and a well-typed term admits a polynomial bound on the length of any of its beta reduction sequences. We also give a translation of LAL into DLAL and deduce from it that all polynomial time functions can be represented in DLAL.

Details DOI

CSL Conference 2006 Conference Paper

Verification of Ptime Reducibility for System F Terms Via Dual Light Affine Logic

Vincent Atassi
Patrick Baillot
Kazushige Terui

Abstract In a previous work we introduced Dual Light Affine Logic ( DLAL ) ([BT04]) as a variant of Light Linear Logic suitable for guaranteeing complexity properties on lambda-calculus terms: all typable terms can be evaluated in polynomial time and all Ptime functions can be represented. In the present work we address the problem of typing lambda-terms in second-order DLAL. For that we give a procedure which, starting with a term typed in system F, finds all possible ways to decorate it into a DLAL typed term. We show that our procedure can be run in time polynomial in the size of the original Church typed system F term.

Details

TCS Journal 2004 Journal Article

Stratified coherence spaces: a denotational semantics for light linear logic

Patrick Baillot

Light linear logic (LLL) was introduced by Girard as a logical system capturing the class of polytime functions within the proofs-as-programs approach. In the present paper, we undertake a semantical analysis of LLL: a variant of coherence spaces is introduced and we prove that it is a sound model for this system, but not for usual linear logic. A simpler version of the model yields a sound semantics of Elementary linear logic, which is the analog of LLL for the class of Kalmar elementary functions. We illustrate our semantical method by showing how various principles fail in these models.

Details DOI

TCS Journal 2004 Journal Article

Type inference for light affine logic via constraints on words

Patrick Baillot

Light Affine Logic (LAL) is a system due to Girard and Asperti capturing the complexity class P in a proof-theoretical approach based on Linear Logic. LAL provides a typing for lambda-calculus which guarantees that a well-typed program is executable in polynomial time on any input. We prove that the LAL type inference problem for lambda-calculus is decidable (for propositional LAL). To establish this result we reformulate the type-assignment system into an equivalent one which makes use of subtyping and is more flexible. We then use a reduction to a satisfiability problem for a system of inequations on words over a binary alphabet, for which we provide a decision procedure.

Details DOI

CSL Conference 1998 Conference Paper

Timeless Games

Patrick Baillot
Vincent Danos
Thomas Ehrhard
Laurent Regnier

Abstract Two models of classical linear logic are set up. First our recent version of AJM games model which will be our source model. Then the target model, polarized pointed relations, a variant of the plain relational model which is constructed in two steps: first the model of pointed relations, then the additional polarization structure which yields a proper duality. Then the natural time-forgetting map is shown to generate a lax functor from the source to the target. Finally a further refinement of the target model using bipolarities is sketched, giving a closer link with the games model for the interpretation of syntax. Thus a bridge is constructed that goes from a dynamic model to a static model of evaluation.

Details