Formalizing General Calculi with Binders in Rewriting Logic

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

• Jose Meseguer, University of Illinois at Urbana-Champaign and Leverhulme Visiting Professor at King's College London
• Friday 16 June 2023, 14:00-15:00
• SS03, 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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• SS03, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• tcw57’s list
• yk373's list

Note that ex-directory lists are not shown.