University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > Formalizing General Calculi with Binders in Rewriting Logic

Formalizing General Calculi with Binders in Rewriting Logic

Add to your list(s) Download to your calendar using vCal

  • UserJose Meseguer, University of Illinois at Urbana-Champaign and Leverhulme Visiting Professor at King's College London
  • ClockFriday 16 June 2023, 14:00-15:00
  • HouseSS03, Computer Laboratory.

If you have a question about this talk, please contact Jamie Vicary.

General calculi with binders are useful in many areas such as, e.g., mathematical logic, programming languages, and concurrency. Their meta-levels are often left implicit by suggesting that they are similar to that of the lambda calculus. But the devil is in the details; and their formalization is needed, both to support formal reasoning, and to achieve correct implementations. Two approaches used to formalize the meta-level of a calculus with binders are higher-order abstract syntax and nominal logic. In this talk I will propose a third alternative to formalize calculi with binders, namely, the use of rewriting logic. Rewriting logic is a simple, yet quite expressive, computational logic that has demonstrated good capabilities both as a general semantic framework for computation, including concurrent computation, and as a logical framework in which many logics can be naturally represented and mechanized. The Maude language is a high-performance implementation of rewriting logic. The talk will present a general approach to the rewriting logic representation of calculi with binders, and to a seamless derivation from high-level formalizations to executable versions of calculi with binders that can be directly executed in Maude.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity