ABSTRACT. Deduction modulo is a framework in which theories are integrated into proof systems such as natural deduction or sequent calculus by presenting them using rewriting rules. When only terms are rewritten, cut admissibility in those systems is equivalent to the confluence of the rewriting system, as shown by Dowek, RTA 2003, LNCS 2706. This is no longer true when considering rewriting rules involving propositions. In this paper, we show that, in the same way that it is possible to recover confluence using Knuth-Bendix completion, one can regain cut admissibility in the general case using standard saturation techniques. This work relies on a view of proposition rewriting rules as oriented clauses, like term rewriting rules can be seen as oriented equations. This also leads us to introduce an extension of deduction modulo with *conditional* term rewriting rules.

ABSTRACT. For an infinite-state concurrent system S with a set AP of state predicates, its predicate abstraction defines a finite-state system whose states are subsets of AP, and its transitions s --> s' are witnessed by concrete transitions between states in S satisfying the respective sets of predicates s and s'. Since it is not always possible to find such witnesses, an over-approximation adding extra transitions is often used. For systems S described by formal specifications, predicate abstractions are typically built using various automated deduction techniques. This paper presents a new method--based on rewriting, semantic unification, and variant narrowing--to automatically generate a predicate abstraction when the formal specification of S is given by a conditional rewrite theory. The method is illustrated with concrete examples showing that it naturally supports abstraction refinement and is quite accurate, i.e., it can produce abstractions not needing over-approximations.

ABSTRACT. This paper presents a language-independent proof system for reachability properties of programs written in non-deterministic (e.g. concurrent) languages, referred to as *all-path reachability logic*. It derives partial-correctness properties with all-path semantics (a state satisfying a given precondition reaches states satisfying a given postcondition on all terminating execution paths). The proof system takes as axioms any unconditional operational semantics, and is sound (partially correct) and (relatively) complete, independent of the object language; the soundness has also been mechanized (Coq). This approach is implemented in a tool for semantics-based verification as part of the K framework.

ABSTRACT. In this talk we present a paradigm of focusing proof search based on an incremental construction of ''correct'' (i.e, sequentializable) proof structures of the pure (units free) multiplicative and additive fragment of linear logic (J.-Y. Girard, 1987). The correctness of proof construction steps (or expansion steps) is ensured by means of a system of graph retraction rules; this graph rewriting system is shown to be convergent, that is, terminating and confluent. The proposed proof construction follows a specific - ''parsimonious'', indeed - retraction strategy that, at each expansion attempt, allows to take into account (abstract) graphs that are ''smaller'' (w.r.t. the size) than the starting proof structures.

ABSTRACT. This is a talk in the branch of logic known as model theory, more precisely, in o-minimality. The first example of an o-minimal structure is the ordered algebraic structure on the set of real numbers and I shall focus on expansions of this structure. Being o-minimal means that the first order definable sets in the structure do not exhibit wild phenomena (this will be made precise). After discussing some basic theory of such structures I shall present some recent applications to diophantine geometry.

ABSTRACT. The focus will be a presentation of new results and successes of semantic analyses of  concurrent programs. These are accomplished by contextual equivalence, observing may- and should-convergence, and by adapting known techniques from deterministic programs to  non-determinism and concurrency.  The techniques are context lemmata, diagram techniques, applicative similarities, infinite tree reductions, and translations. The results are equivalences, correctness of program transformations, correctness of implementations and translations.

ABSTRACT. We show how to construct a logical relation for countable nondeterminism in a guarded type theory, corresponding to the internal logic of the topos $Sh(\omega_1)$ of sheaves over $\omega_1$. In contrast to earlier work on abstract step-indexed models, we not only construct the logical relations in the guarded type theory, but also give an internal proof of the adequacy of the model with respect to standard contextual equivalence. To state and prove adequacy of the logical relation, we introduce a new propositional modality. In connection with this modality we show why it is necessary to work in the logic of $\Sh(\omega_1)$.

ABSTRACT. We add an abstract datatype for a closed interval of real numbers to type theory, providing a representation-independent approach to programming with real numbers. The abstract datatype requires only function types and a natural numbers type for its formulation, so can be added to any type theory that extends Goedel's System T. Our main result establishes that programming with the abstract datatype is equivalent in power to programming intensionally with representations of real numbers. We also consider representing arbitrary real numbers using a mantissa-exponent representation in which the mantissa is taken from the abstract interval.

ABSTRACT. We establish that the local store monad defined by Plotkin and Power is a monad with arities for an appropriate notion of arities in the category of presheaves over the category of injections. From this follows that the monad is associated to a graded Lawvere theory. We explain how to present this graded theory by generators and relations, which we then depict in the graphical language of string diagrams.

ABSTRACT. The notion of subtyping has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in programming languages. The soundness and the completeness, together referred to as the preciseness of subtyping, can be considered from two different points of view: denotational and operational. The former preciseness is based on the denotation of a type which is a mathematical object that describes the meaning of the type in accordance with the denotations of other expressions from the language. The latter preciseness has been recently developed with respect to type safety, i.e. the safe replacement of a term of a smaller type when a term of a bigger type is expected.

We proposes a technique for formalising and proving operational preciseness of the subtyping relation in the setting of a concurrent lambda calculus with intersection and union types. The key feature is the link between typings and the operational semantics. We prove then soundness and completeness getting that the subtyping relation of this calculus enjoys both denotational and operational preciseness.