Abstract

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.