Encoding Generic Judgments
Dale Armin Miller · Electronic Notes in Theoretical Computer Science · 2001
Operational semantics is often presented in a rather syntactic fashion using relations specified by inference rules or equivalently by clauses in a suitable logic programming language. As it is well known, various syntactic details of specifications involving bound variables can be greatly simplified if that logic programming language has term-level abstractions (λ-abstraction) and proof-level abstractions (eigenvariables) and the specification encodes object-level binders using λ-terms and universal quantification. We shall attempt to extend this specification setting to include the problem of specifying not only relations capturing operational semantics, such as one-step evaluation, but also properties and relations about the semantics, such as simulation. Central to our approach is the encoding of generic object-level judgments (universally quantified formulas) as suitable atomic meta-level judgments. We shall encode both the one-step transition semantics and simulation of (finite) π-calculus to illustrate our approach.