Séminaire, 8 décembre 2011

Programme

10:30 – 12:00

Jean-Christophe Filliâtre (LRI - Université Paris Sud)

Invited talk: Deductive Program Verification with Why3

Why3 is the next generation of the Why software verification platform. Why3 clearly separates the purely logical specification part from generation of verification conditions for programs. Regarding the former, Why3 comes with a new enhanced language of logical specification. It features a rich library of proof task transformations that can be chained to produce a suitable input for a large set of theorem provers, including SMT solvers, TPTP provers, as well as interactive proof assistants. Regarding the latter, Why3 comes with a powerful programming language featuring recursive functions, local bindings, pattern matching, exceptions, and records with possibly mutable fields. Aliasing are excluded by type checking to allow the computation of natural verification conditions through a weakest precondition calculus.

14:00 – 15:00

Alexis Bernardet (LIX-ENS Cachan)

A simple presentation of the effective topos

Topos theory can be used to abstract models of higher-order logic the same way Heyting algebras can be used for propositional logic. A topos is a cartesian closed category that satisfies certain properties (e.g. the category of sets is a topos), but it is interesting to see whether it also satisfies some of these:

(1) The internal logic of the topos has the law of excluded middle (2) Every morphism of the topos is computable (3) The topos has an object of natural integers (definition of Lawvere)

With these three properties, the halting problem can be proved computable; hence, a (non-degenerated) topos cannot have these three properties at the same time:

• With properties (1) and (3), we have classical logic: the category of sets is a good example.
• With properties (1) and (2), we have finite logic: the category of finite sets is a good example

• With properties (2) and (3), we have intuitionistic logic.

  One of the most famous topos satisfying these two properties is Hyland's effective topos, which can be seen as the universe of realisability. While it is quite simple to check that the category of sets and the category of finite sets are topos, proving that the effective topos is indeed a topos is much harder.

We introduce here an alternative definition of Hyland's effective topos, based on a realisability framework with two levels of abstraction: a low level and a high level. With this definition, the proof that this framework forms a topos is almost as simple as proving that the category of sets is a topos. Moreover, the high level of the framework can be directly used as a model of higher-order intuitionistic systems.

Indeed, topos satisfying (2) and (3) are the most interesting ones for computer science because they ensure that a programming language based on topos theory can be given a constructive semantics. In such a programming language, we can only write functions that terminate, as in proof assistants like Coq, so the language cannot be Turing-complete. The main advantage of having a programming language based on topos theory over more usual intuitionistic systems such as Martin-Loef type theory is the notion of equality: it is extensional, has proof-irrelevance, and allows the axiom of unique choice.

15:30 – 16:30

Damien Pous (Sardes - Grenoble)

Hopcroft, Karp, and up-to techniques

(joint work with Filippo Bonchi)

We present a (hopefully) new algorithm for determining if two non-deterministic finite automata are language equivalent. We exploit coinductive up-to techniques to improve the standard algorithm by Hopcroft and Karp for deterministic finite automata, so as to avoid computing the whole deterministic automata. Although the proposed algorithm remains exponential in worst case (the problem is PSPACE-complete), experimental results show that it can be much faster than the standard algorithm: in most cases, only a very small portion of the underlying deterministic automata has to be explored.