计算机科学中的逻辑

The aim of this paper is to refine and extend proposals by Sozeau and Tabareau and by Voevodsky for universe polymorphism in type theory. In those systems judgments can depend on explicit constraints between universe levels. We here present…

Focusing, introduced by Jean-Marc Andreoli in the context of classical linear logic, defines a normal form for sequent calculus derivations that cuts down on the number of possible derivations by eagerly applying invertible rules and…

Relation reasoning in knowledge graphs (KGs) aims at predicting missing relations in incomplete triples, whereas the dominant paradigm is learning the embeddings of relations and entities, which is limited to a transductive setting and has…

Double auctions are widely used in financial markets, such as those for stocks, derivatives, currencies, and commodities, to match demand and supply. Once all buyers and sellers have placed their trade requests, the exchange determines how…

We present a new method for the verification of quantum circuits based on a novel symbolic representation of sets of quantum states using level-synchronized tree automata (LSTAs). LSTAs extend classical tree automata by labeling each…

Differential privacy is a statistical definition of privacy that has attracted the interest of both academia and industry. Its formulations are easy to understand, but the differential privacy of databases is complicated to determine. One…

This paper introduces the XOR-OR-AND normal form (XNF) for logical formulas. It is a generalization of the well-known Conjunctive Normal Form (CNF) where literals are replaced by XORs of literals. As a first theoretic result, we show that…

Coherent differentiation was introduced by Ehrhard in order to generalize differential categories to a setting in which the sum is only partially defined, in order to account for the deterministic nature of most models of computation. This…

Non-Markovian models have great expressive power, at the cost of complex analysis of the stochastic process. The method of Stochastic State Classes (SSCs) derives closed-form analytical expressions for the joint Probability Density…

In systems verification we are often concerned with multiple, inter-dependent properties that a program must satisfy. To prove that a program satisfies a given property, the correctness of intermediate states of the program must be…

In order to formally verify robotic controllers, we must tackle the inherent uncertainty of sensing and actuation in a physical environment. We can model uncertainty using stochastic hybrid systems, which combine discrete jumps with…

We develop a general framework for agent abstraction based on the situation calculus and the ConGolog agent programming language. We assume that we have a high-level specification and a low-level specification of the agent, both represented…

To refine formal methods for concurrent systems, there are several ways of enriching classical operational semantics of process calculi. One can enable the auditing and undoing of past synchronisations thanks to communication keys, thus…

We study Polynomial Lawvere logic PL, a logic defined over the Lawvere quantale of extended positive reals with sum as tensor, to which we add multiplication, thereby obtaining a semiring structure. PL is designed for complex quantitative…

Exact real computation is an alternative to floating-point arithmetic where operations on real numbers are performed exactly, without the introduction of rounding errors. When proving the correctness of an implementation, one can focus…

Dependent type theory gives an expressive type system facilitating succinct formalizations of mathematical concepts. In practice, it is mainly used for interactive theorem proving with intensional type theories, with PVS being a notable…

We introduce a constructive method applicable to a large number of description logics (DLs) for establishing the concept-based Beth definability property (CBP) based on sequent systems. Using the highly expressive DL RIQ as a case study, we…

Building on our prior work on axiomatization of exact real computation by formalizing nondeterministic first-order partial computations over real and complex numbers in a constructive dependent type theory, we present a framework for…

This thesis (Habilitation \`a diriger des recherches) presents some of my research contributions since my Ph.D defense in 2008. I have had the chance to participate in the development of quantum programming languages since their early…

One can find various temporal deontic logics in literature, most focusing on discrete time. The literature on real-time constraints and deontic norms is much sparser. Thus, many analysis techniques which have been developed for deontic…