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:7888@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20160225T110000
DTEND;TZID=Europe/Paris:20160225T120000
DTSTAMP:20241120T205559Z
URL:https://www.i2m.univ-amu.fr/evenements/open-call-by-value/
SUMMARY:Giulio Guerrieri (PPS\, Université Paris-Diderot): Open Call-by-Va
 lue
DESCRIPTION:Giulio Guerrieri: The elegant theory of the call-by-value lambd
 a-calculus relies on weak evaluation and closed terms\, that are natural h
 ypotheses in the study of programming languages. To model proof assistants
 \, however\, strong evaluation and open terms are required\, and it is wel
 l known that the operational semantics of call-by-value becomes problemati
 c in this case\, as first pointed out by Paolini and Ronchi della Rocca. H
 ere we study the intermediate setting—that we call Open Call-by-Value—
 of weak evaluation with open terms\, on top of which Grégoire and Leroy d
 esigned the abstract machine of Coq. Various calculi for Open Call-by-Valu
 e already exist\, coming from logical\, semantical\, or implementative poi
 nts of view\, each one with its pros and cons. This paper presents a detai
 led comparative study of their operational semantics. First\, we show that
  all calculi are equivalent from a termination point of view\, justifying 
 the slogan Open Call-by-Value. Second\, we compare their equational theori
 es. Third\, we present a detailed quantitative analysis of the time cost m
 odel. Four\, we introduce a new simple abstract machine\, and prove it a r
 easonable implementation of Open Call-by-Value with respect to its cost mo
 del. Along the way\, there emerges a sharp deconstruction of call-by-value
  evaluation and of the complexity of its implementations.\nJoint work with
  Beniamino Accattoli.\n\nhttp://www.pps.univ-paris-diderot.fr/~giuliog/
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 020/01/Giulio_Guerrieri.jpg
CATEGORIES:Séminaire,Logique et Interactions
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:STANDARD
DTSTART:20151025T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
END:VTIMEZONE
END:VCALENDAR