BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A compositional account of Herbrand's theorem via concurrent games
  - Pierre Clairambault\, ENS Lyon
DTSTART:20161118T140000Z
DTEND:20161118T150000Z
UID:TALK67372@talks.cam.ac.uk
CONTACT:Dominic Mulligan
DESCRIPTION:Herbrand's theorem\, often regarded as a cornerstone of proof 
 theory\,\nexposes some of the constructive content of classical logic. In 
 its\nsimplest form\, it reduces the validity of a first-order purely exist
 ential formula  ∃x.φ(x) (with φ quantifier-free) to that of a finite d
 isjunction φ(t₁) ∨ ... ∨ φ(tₙ). More generally\, it gives a redu
 ction of first-order validity to propositional validity\, by understanding
  the structure of the assignment of first-order terms to existential quant
 ifiers\, and the causal dependency between quantifiers.\n\nIn this talk\, 
 I will show that Herbrand's theorem in its general form\ncan be elegantly 
 stated as a theorem in the framework of concurrent\ngames. The causal stru
 cture of concurrent strategies\, paired with\nannotations by first-order t
 erms\, is used to specify the dependency\nbetween quantifiers. Furthermore
  concurrent strategies can be composed\,\nyielding a compositional proof o
 f Herbrand's theorem\, simply by interpreting classical sequent proofs in 
 a well-chosen denotational\nmodel. I assume no prior knowledge of Herbrand
 's theorem or concurrent\ngames.\n\nThis is joint work with Aurore Alcolei
 \, Martin Hyland and Glynn Winskel.
LOCATION:SS03
END:VEVENT
END:VCALENDAR