BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Symmetries in Reversible Programming - Vikraman Choudhury\, Univer
 sity of Indiana
DTSTART:20220527T130000Z
DTEND:20220527T140000Z
UID:TALK174857@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:Reversible computing is a model of computation\, motivated by 
 physical principles\, where computation happens in an information-preservi
 ng way. Reversible programs are usually expressed as reversible boolean fu
 nctions\, 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 calculus for reversible programming\, S
 abry and his collaborators formulated the Pi family of reversible programm
 ing languages\, which are typed high-level languages for writing total rev
 ersible programs. In this talk\, I will discuss the semantics foundations 
 of this family of languages\, using groupoids.\n\nThe Pi language has cons
 tructs for expressing reversible programs on finite number of bits\, and t
 heir equivalences. The syntactic groupoid of this languages presents the f
 ree symmetric rig groupoid on zero generators\, which is shown to be equiv
 alent to the groupoid of finite sets and bijections. This leads to a fully
 -abstract and fully-complete denotational semantics for the language. The 
 proof uses various tools and techniques from presentations of symmetric mo
 noidal categories\, coherence theorems\, presentations of symmetric groups
 \, permutation codes\, and ideas from normalisation-by-evaluation in progr
 amming language theory.\n\nFinally\, there are some applications of this s
 emantics to reversible boolean circuits\, motivated by examples from quant
 um computing. I will show how to perform normalisation-by-evaluation\, ver
 ification\, and synthesis of reversible boolean gates\, and how to reason 
 about and transfer theorems between different representations of reversibl
 e circuits.
LOCATION:SS03
END:VEVENT
END:VCALENDAR