Séminaire, 26 septembre 2013
Lieu
La rencontre aura lieu à l'École Normale Supérieure de Lyon, campus Jacques Monod, dans l'amphi B. Pour venir, voir les instructions sur le site du LIP ou sur un plan, par exemple chez Google Maps. À l'entrée, se présenter à la réception, qui aura la liste des inscrits.
Programme
 10:30 – 12:00

Christophe Raffalli (LAMA, Université de Savoie)
We give here an effective proof of Hilbert's nullstellensatz and KrivineStengle's positivestellensatz using the cut elimination theorem for sequent calculus. The proof is very similar to the current techniques in constructive algebraic geometry by Henri Lombardi, but seems more modular.
In the case of the positive stellensatz, we think we prove a more general result than the original one, thanks to a new notion of justification of positiveness: PBDD (polynomial binary decision diagram). It allows both to recover KrivineStengle's justification, but also another one which seems to require lower degree.
We apply the same techniques to the nullstellensatz for differentially closed field and show that the proof is almost unchanged.
Remark: here we do not provide bound, but an effective algorithm (implemented in OCaml) to build the wanted algebraic equality. Nevertheless, we discuss how bound could probably be obtained. We also do not deal effectively with the axiom of algebraic/real closure. Those are eliminated using standard model theory.
 14:00 – 15:00

Michele BasaldellaInvited talk: An interactive semantics for classical proofs
The aim of this talk is to present a semantics for proofs in classical logic.
Classical logic: We use a variant of the proofsystem introduced by Tait (1968), a system which is often used for analyzing the prooftheory of classical arithmetic and its fragments. The language of this logic consists of infinitary propositional formulas, and the proofsystem for this language is formulated through a sequent calculus with infinitary rules of inference.
Proofs: The target of our analysis is not the derivability predicate “the formula A is derivable”, but the more subtle relation “p is a proof of the formula A”, that we abbreviate as “p der A.” In order to define this relation, we need to formalize the concept of “formulafree proofs”, i.e, proofs that does not depend (too much) on the formulas they prove. To understand the idea behind this concept, consider the untyped λcalculus. By the CurryHoward correspondence, λterms can be seen as a “formulafree” formalization of natural deduction proofs for the implicational fragment of intuitionistic propositional logic. Hence, “p der A” can be read as “the untyped λterm p has (simple) type A in the Currystyle type assignment.” Here we use a similar idea: we define a class of objects that we call tests which play the role of the untyped λterms, and in order to define p der A, we use Tait’s normal rules as type assignment.
Semantics: Our semantics is deeply inspired by Girard’s ludics (2001). As in untyped λcalculus βreduction can be seen as natural deduction normalization “without types”, we similarly define a “formulafree” cutelimination procedure which works with tests, that we call interaction. By analyzing the properties of interaction, we define another relation “p int A” between tests and formulas with the following meaning: “the result of the interaction between the test p and the countertests for A terminates.” We finally show a soundnessandcompleteness theorem: “p der A” if and only if “p int A”.
 15:30 – 16:30

Michele Pagani (LIPN, Univ. Paris 13)
Probabilistic coherence spaces PCOH yield a semantics of higherorder probabilistic computation, interpreting types as convex sets and programs as power series. We prove that the equality of interpretations in PCOH characterizes the operational indistinguishability of programs in PCF with a random primitive.
This is the first result of full abstraction for a semantics of probabilistic PCF. The key ingredient relies on the regularity of power series and introduces, in denotational semantics, techniques coming from Calculus.
Along the way to the theorem, we design a weighted intersection type assignment system giving a logical presentation of PCOH.