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:20161030T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=10
TZNAME:CET
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTAMP:20260429T024209Z
UID:585bf14ac7f5b914140820@ist.ac.at
DTSTART:20170126T094500
DTEND:20170126T104500
DESCRIPTION:Speaker: Justin Hsu\nAbstract: Since the inception of computer 
 science\, rigorous mathematical proofs have played a major role in analyzi
 ng and understanding computation. Fields like algorithms\, datastructures\
 , and complexity theory---commonly known as "Theory A" or simply "Theory"-
 --seek to understand how efficiently problems can be solved by a computer\
 , if they can be solved at all. In contrast\, disciplines like programming
  languages\, denotational semantics\, and verification---commonly known as
  "Theory B" or simply "Formal Methods"---explore how to represent computat
 ion\, and how to reason about its correctness.\n\nWhile these two broad ar
 eas share a theoretical perspective on computer science\, in recent years 
 they have diverged substantially. In this talk\, I will present a confluen
 ce of ideas from the two theories. First\, I will show how coupling proofs
 \, used to analyze random walks and Markov chains\, correspond to proofs i
 n the program logic pRHL. This connection enables formal verification of n
 ovel probabilistic properties\, and provides an structured understanding o
 f proofs by coupling. Then\, I will show how an approximate version of pRH
 L\, called apRHL\, points to a new\, approximate version of couplings clos
 ely related to differential privacy\, and a new kind of proof by approxima
 te coupling. This proof technique enables cleaner proofs of differential p
 rivacy\, both for humans and for formal verification. Finally\, I will dis
 cuss some potential directions towards a possible "Theory AB"\, blending i
 deas from both worlds.
LOCATION:Mondi Seminar Room 2\, Central Building\, ISTA
ORGANIZER:pdelreal@ist.ac.at
SUMMARY:Justin Hsu: Towards Theory AB
URL:https://talks-calendar.ista.ac.at/events/72
END:VEVENT
END:VCALENDAR