BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//wp-events-plugin.com//7.2.3.1//EN
TZID:Europe/Paris
X-WR-TIMEZONE:Europe/Paris
BEGIN:VEVENT
UID:7288@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20180614T110000
DTEND;TZID=Europe/Paris:20180614T123000
DTSTAMP:20241120T203900Z
URL:https://www.i2m.univ-amu.fr/evenements/the-true-concurrency-of-herbran
 d-s-theorem/
SUMMARY:Pierre Clairambault (LIP\, CNRS\, ENS Lyon): The true concurrency o
 f Herbrand's theorem
DESCRIPTION:Pierre Clairambault: Herbrand's theorem\, widely regarded as a 
 cornerstone of proof theory\, exposes some of the constructive content of 
 classical logic. In its simplest form\, it reduces the validity of a first
 -order purely existential formula to that of a finite disjunction. In the 
 general case\, it reduces first-order validity to propositional validity\,
  by understanding the structure of the assignment of first-order terms to 
 existential quantifiers\, and the causal dependency between quantifiers.\n
 In this paper\, we show that Herbrand's theorem in its general form can be
  elegantly stated and proved as a theorem in the framework of concurrent g
 ames\, a denotational semantics designed to faithfully represent causality
  and independence in concurrent systems\, thereby exposing the concurrency
  underlying the computational content of classical proofs. The causal stru
 cture of concurrent strategies\, paired with annotations by first-order te
 rms\, is used to specify the dependency between quantifiers implicit in pr
 oofs. Furthermore concurrent strategies can be composed\, yielding a compo
 sitional proof of Herbrand's theorem\, simply by interpreting classical se
 quent proofs in a well-chosen denotational model.\nThis is joint work with
  Aurore Alcolei\, Martin Hyland\, and Glynn Winskel.\n\n\n
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 020/01/Pierre_Clairambault.jpg
CATEGORIES:Séminaire,Logique et Interactions
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
DTSTART:20180325T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
END:DAYLIGHT
END:VTIMEZONE
END:VCALENDAR