BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Shoggoth: A Formal Foundation for Strategic Rewriting - Xueying Qi
 n\, University of Edinbunrgh
DTSTART:20240521T100000Z
DTEND:20240521T110000Z
UID:TALK217009@talks.cam.ac.uk
CONTACT:Siddharth Bhat
DESCRIPTION:Rewriting is a versatile and powerful technique used in many d
 omains. Strategic rewriting allows programmers to control the application 
 of rewrite rules by composing individual rewrite rules into complex rewrit
 e strategies. These strategies are semantically complex\, as they may be n
 ondeterministic\, they may raise errors that trigger backtracking\, and th
 ey may not terminate.\n\nGiven such semantic complexity\, it is necessary 
 to establish a formal understanding of rewrite strategies and to enable re
 asoning about them in order to answer questions like: How do we know that 
 a rewrite strategy terminates? How do we know that a rewrite strategy does
  not fail because we compose two incompatible rewrites? How do we know tha
 t a desired property holds after applying a rewrite strategy?\n\nTo answer
  these questions\, we introduce Shoggoth: a formal foundation for understa
 nding\, analysing and reasoning about strategic rewriting that is capable 
 of answering these questions. We provide a denotational semantics of Syste
 m S\, a core language for strategic rewriting\, and prove its equivalence 
 to our big-step operational semantics\, which extends existing work by exp
 licitly accounting for divergence. We further define a location-based weak
 est precondition calculus to enable formal reasoning about rewriting strat
 egies\, and we prove this calculus sound with respect to the denotational 
 semantics. We show how this calculus can be used in practice to reason abo
 ut properties of rewriting strategies\, including termination\, that they 
 are well-composed\, and that desired postconditions hold. The semantics an
 d calculus are formalised in Isabelle/HOL and all proofs are mechanised.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR