计算机科学中的逻辑

Non-idempotent intersection types provide quantitative information about typed programs, and have been used to obtain time and space complexity measures. Intersection type systems characterize termination, so restrictions need to be made in…

We study the problem of computing the reachable principals of simulation preorder and the reachable blocks of simulation equivalence. Following a theoretical investigation of the decidability and complexity aspects of this problem, which in…

The growing complexity of decision-making in public health and health care has motivated an increasing use of mathematical modeling. An important line of health modeling is based on stock & flow diagrams. Such modeling elevates transparency…

Moving from the mathematical theory of (abstract) syntax, we develop a general relational theory of symbolic manipulation parametric with respect to, and accounting for, general notions of syntax. We model syntax relying on categorical…

We introduce Probabilistic Guarded Kleene Algebra with Tests (ProbGKAT), an extension of GKAT that allows reasoning about uninterpreted imperative programs with probabilistic branching. We give its operational semantics in terms of special…

In this early technical report on an ongoing project, we present -- to the best of our knowledge -- the first study of completeness thresholds for memory safety proofs. Specifically we consider heap-manipulating programs that iterate over…

We provide a semi-grammatical description of the set of normal proofs of positive formulae in minimal predicate logic, i.e. a grammar that generates a set of schemes, from each of which we can produce a finite number of normal proofs. This…

In the recent past, the reduction-based and the model-based methods to prove cut elimination have converged, so that they now appear just as two sides of the same coin. This paper details some of the steps of this transformation.

On the real numbers, the notions of a semi-decidable relation and that of an effectively enumerable relation differ. The second only seems to be adequate to express, in an algorithmic way, non deterministic physical theories, where…

The category Set_* of sets and partial functions is well-known to be traced monoidal, meaning that a partial function S+U -/-> T+U can be coherently transformed into a partial function S -/-> T. This transformation is generally described in…

This short note establishes positionality of mean-payoff games over infinite game graphs by constructing a well-founded monotone universal graph.

This paper develops a {\em qualitative} and logic-based notion of similarity from the ground up using only elementary concepts of first-order logic centered around the fundamental model-theoretic notion of type.

Libraries of formal proofs are an important part of our mathematical heritage, but their usability and sustainability is poor. Indeed, each library is specific to a proof system, sometimes even to some version of this system. Thus, a…

BDDs are representations of a Boolean expression in the form of a directed acyclic graph. BDDs are widely used in several fields, particularly in model checking and hardware verification. There are several implementations for BDD…

This paper defines two decreasing measures for terms of the simply typed lambda-calculus, called the W-measure and the Tm-measure. A decreasing measure is a function that maps each typable lambda-term to an element of a well-founded…

We study the complexity of proof systems augmenting resolution with inference rules that allow, given a formula $\Gamma$ in conjunctive normal form, deriving clauses that are not necessarily logically implied by $\Gamma$ but whose addition…

This paper continues the line of research aimed at investigating the relationship between logic programs and first-order theories. We extend the definition of program completion to programs with input and output in a subset of the input…

Causal Modeling Semantics (CMS, e.g., Galles and Pearl 1998; Pearl 2000; Halpern 2000) is a powerful framework for evaluating counterfactuals whose antecedent is a conjunction of atomic formulas. We extend CMS to an evaluation of the…

The essence of compiling with continuations is that conversion to continuation-passing style (CPS) is equivalent to a source language transformation converting to administrative normal form (ANF). Taking as source language Moggi's…

Cut-elimination is the bedrock of proof theory with a multitude of applications from computational interpretations to proof analysis. It is also the starting point for important meta-theoretical investigations including decidability,…