Séminaire, 12 décembre 2013
This meeting will take place in Paris, Amphithéâtre 9E, Université Denis Diderot (Paris 7), esplanade Pierre VidalNaquet 75013 Paris (Metro Bibliothèque François Mitterrand, reachable by line 14 from Gare de Lyon).
Programme
 11:00 – 12:30

Vincent Padovani (PPS  Paris 7)Invited talk: Ticket entailment is decidable
 14:30 – 15:30

Guy McCusker (University of Bath)Invited talk: Weighted relational models of typed lambdacalculi
The category Rel of sets and relations yields one of the simplest denotational semantics of Linear Logic. Rel can be viewed as the biproduct completion of the Boolean ring. We consider the generalization of this construction to arbitrary continuous semirings, producing categories that provide cpoenriched models of linear logic akin to Rel, and investigate models of PCF in their coKleisli categories. These models contain quantitative information, provided by the elements of the semiring R. Specific instances of R allow us to compare programs not only with respect to “what they can do”, but also “in how many steps” or “in how many different ways” (for nondeterministic PCF) or even “with what probability” (for probabilistic PCF).
Joint work with Jim Laird (Bath) and Giulio Manzonetto and Michele Pagani (LIPN, ParisNord)
 16:00 – 17:00

Hyeonseung Im (LRI (Orsay))Invited talk: A modal logic internalizing normal proofs
In the prooftheoretic study of logic, the notion of normal proof has been understood and investigated as a metalogical property. Usually we formulate a system of logic, identify a class of proofs as normal proofs, and show that every proof in the system reduces to a corresponding normal proof. This paper develops a system of modal logic that is capable of expressing the notion of normal proof within the system itself, thereby making normal proofs an inherent property of the logic. Using a modality △ to express the existence of a normal proof, the system provides a means for both recognizing and manipulating its own normal proofs. We develop the system as a sequent calculus with the implication connective ⊃ and the modality △, and prove the cut elimination theorem. From the sequent calculus, we derive two equivalent natural deduction systems.
Joint Work with Sungwoo Park (Pohang)