Séminaire, 21 mai 2015

Programme

10:30 – 12:00
Étienne Miquey (Laboratoire PPS, Montevideo)
Invited talk: Realizability games for the specification problem

In Krivine classical realizability, one can understand the truth value of a formula (that is the set of its realizers) as its defenders, and the falsity value as the set of its opponents. Following this intuition, the execution of a process is a match between both players, that a realizer should win.

In this talk, we will explain how to use a notion of game to give a precise specification of the realizers of a given formula. We will focus on the particular case of arithmetical formulae, for which our definition relies on the principle of Coquand's games. In the end, we obtain an equivalence between universal realizers and winning strategies (even in presence of non-substitutive instructions such as Quote), which also directly implies the absoluteness of arithmetical formulae for classical realizability.

14:00 – 15:00
Arthur Charguéraud (Toccata - INRIA)
Invited talk: Vérification interactive de programmes impératifs, avec CFML

CFML est un outil qui permet de prouver en Coq la correction fonctionnelle de programmes Caml. CFML s'appuie sur la notion de formule caractéristique, qui permet de décrire la sémantique d'un programme impératif sous la forme d'une formule de la logique d'ordre supérieur. Les formules caractéristiques, qui sont à la fois correctes et complètes, sont de tailles linéaires et peuvent être générées automatiquement à partir du code source des programmes.

Elles s'appuient de plus sur la Logique de Séparation, qui permet d'effectuer des raisonnements modulaires, et intègrent la notion de crédits-temps, qui permet de vérifier des propriétés de complexité asymptotique. Dans cet exposé, je présenterai la théorie de CFML et j'illustrerai son utilisation en pratique, à travers plusieurs exemples.

15:30 – 16:30
Antonino Salibra (Univ. Ca' Foscari, Venezia)
Invited talk: Logics via algebras and substitutions

In this talk we present a translation of formulas and models of classical and non-classical logics into factor algebras. The correspondence:

  • Propositional variables - operator of decompositions

  • Logical operations - substitutions

  • Formulas - algebraic terms

  • Models - factor algebras,

provides a uniform calculus of provability for all the logics which admit the translation. Many examples will be discussed: classical logic, intuitionistic logic, linear logic, many-valued logics.