BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formalizing General Calculi with Binders in Rewriting Logic - Jose
  Meseguer\, University of Illinois at Urbana-Champaign and Leverhulme Visi
 ting Professor at King's College London
DTSTART:20230616T130000Z
DTEND:20230616T140000Z
UID:TALK202246@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:General calculi with binders are useful in many areas such as\
 , e.g.\,\nmathematical logic\, programming languages\, and concurrency.  T
 heir\nmeta-levels are often left implicit by suggesting that they are\nsim
 ilar to that of the lambda calculus.  But the devil is in the\ndetails\; a
 nd their formalization is needed\, both to support formal\nreasoning\, and
  to achieve correct implementations.  Two approaches\nused to formalize th
 e meta-level of a calculus with binders are\nhigher-order abstract syntax 
 and nominal logic.  In this talk I will\npropose a third alternative to fo
 rmalize calculi with binders\, namely\,\nthe use of rewriting logic.  Rewr
 iting logic is a simple\, yet quite\nexpressive\, computational logic that
  has demonstrated good\ncapabilities both as a general semantic framework 
 for computation\,\nincluding concurrent computation\, and as a logical fra
 mework in which\nmany logics can be naturally represented and mechanized. 
  The Maude\nlanguage is a high-performance implementation of rewriting log
 ic.\nThe talk will present a general approach to the rewriting logic\nrepr
 esentation of calculi with binders\, and to a seamless derivation\nfrom hi
 gh-level formalizations to executable versions of calculi with\nbinders th
 at can be directly executed in Maude.
LOCATION:SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR