Séminaire, 12 décembre 2013

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 lambda-calculi

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 cpo-enriched models of linear logic akin to Rel, and investigate models of PCF in their co-Kleisli 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 non-deterministic PCF) or even “with what probability” (for probabilistic PCF).

Joint work with Jim Laird (Bath) and Giulio Manzonetto and Michele Pagani (LIPN, Paris-Nord)

16:00 – 17:00

Hyeonseung Im (LRI (Orsay))

Invited talk: A modal logic internalizing normal proofs

In the proof-theoretic 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)