BEGIN:VCALENDAR
VERSION:2.0
PRODID:icalendar-ruby
CALSCALE:GREGORIAN
METHOD:PUBLISH
BEGIN:VTIMEZONE
TZID:Europe/Vienna
BEGIN:DAYLIGHT
DTSTART:20170326T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=3
TZNAME:CEST
END:DAYLIGHT
BEGIN:STANDARD
DTSTART:20171029T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=10
TZNAME:CET
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTAMP:20260427T115807Z
UID:59958700ad338255213207@ist.ac.at
DTSTART:20170906T170000
DTEND:20170906T180000
DESCRIPTION:Speaker: Johannes Kloos\nhosted by Tom Henzinger\nAbstract: Asy
 nchronous concurrency is a model of concurrency based on the concept of ta
 sks. It executes tasks one-at-a-time\, choosing the next task to run from 
 a set called the task buffer\, adding tasks to the buffer using a "post" p
 rimitive\, and scheduling a new task only when the currently running task 
 gives up control. Task can depend on each other using explicit "wait" oper
 ations. This model and its variants are used widely in languages such as J
 avaScript\, C# (the async and await primitives)\, or the monadic concurren
 cy libraries of Haskell and OCaml. The more restricted scheduling separate
 s it from the more commonly considered multi-threaded programming model.\n
 \nIn this talk\, I will address talk about two projects. The first project
  deals with the question how we can reason about asynchronous programs. We
  present a program logic and a corresponding type system that allow us to 
 reason locally about programs with asynchronous concurrency and mutable st
 ate\; we instantiate this model for OCaml using the Lwt library. The key i
 nnovation is to introduce the concept of a "wait permission"\, which descr
 ibes the resources that a given task will yield on termination. An earlier
  version of this work was published at ECOOP '15. The second project deals
  with the question how we can perform a kind of "asynchronous parallelizat
 ion" optimization\, where we are given a (more-or-less) sequential program
  and rewrite it to make use of asynchronous concurrency. We use a set of p
 rogram rewriting rules\, most notably replacing synchronous I/O operations
  with asynchronous counterparts in a safe way\, and pushing wait statement
 s as far back as possible. As it turns out\, proving the soundness of thes
 e rewriting rules is surprisingly tricky\; I will sketch a reasoning appro
 ach that allows us to show refinement\, in the the following sense: Let $e
 $ be a program\, and $e'$ the result of rewriting $e$ using the given rule
 s. For every terminating execution of $e'$\, there is a corresponding term
 inating execution of $e$ that ends in an equivalent state.
LOCATION:Mondi Seminar Room 3\, Central Building\, ISTA
ORGANIZER:pnovotny@ist.ac.at
SUMMARY:Johannes Kloos: Heap-based reasoning about asynchronous programs
URL:https://talks-calendar.ista.ac.at/events/801
END:VEVENT
END:VCALENDAR