BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic and Semantics Seminar (Computer Laboratory)
SUMMARY:Symmetries in Reversible Programming - Vikraman Ch
oudhury\, University of Indiana
DTSTART;TZID=Europe/London:20220527T140000
DTEND;TZID=Europe/London:20220527T150000
UID:TALK174857AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/174857
DESCRIPTION:Reversible computing is a model of computation\, m
otivated by physical principles\, where computatio
n happens in an information-preserving way. Revers
ible programs are usually expressed as reversible
boolean functions\, reversible boolean gates\, or
sequences of reversible operations on bits\, which
can be run forwards or backwards on a reversible
computer.\n\nTowards building a high-level calculu
s for reversible programming\, Sabry and his colla
borators formulated the Pi family of reversible pr
ogramming languages\, which are typed high-level l
anguages for writing total reversible programs. In
this talk\, I will discuss the semantics foundati
ons of this family of languages\, using groupoids.
\n\nThe Pi language has constructs for expressing
reversible programs on finite number of bits\, and
their equivalences. The syntactic groupoid of thi
s languages presents the free symmetric rig groupo
id on zero generators\, which is shown to be equiv
alent to the groupoid of finite sets and bijection
s. This leads to a fully-abstract and fully-comple
te denotational semantics for the language. The pr
oof uses various tools and techniques from present
ations of symmetric monoidal categories\, coherenc
e theorems\, presentations of symmetric groups\, p
ermutation codes\, and ideas from normalisation-by
-evaluation in programming language theory.\n\nFin
ally\, there are some applications of this semanti
cs to reversible boolean circuits\, motivated by e
xamples from quantum computing. I will show how to
perform normalisation-by-evaluation\, verificatio
n\, and synthesis of reversible boolean gates\, an
d how to reason about and transfer theorems betwee
n different representations of reversible circuits
.
LOCATION:SS03
CONTACT:Jamie Vicary
END:VEVENT
END:VCALENDAR