Semantics of Programming Languages
One of the most effective ways to define a programming language or paradigm is as an executable formal specification. This has at least two advantages:
- (1) one can execute programs, and
- (2) one can formally reason about programs and programming languages.
Additionally, if the executable specification language is based on a simple and efficiently implementable computational paradigm, one can obtain quite efficient implementations of programming languages (intepreters or even compilers) which are correct by construction. Moreover, if the definitional framework comes equipped with a suitable notion of a model, then one obtains a built-in denotational semantics for the specified language or lambda calculus.
For achieving the above goal, we are currently using two logical systems: Rewriting Logic and a new logic called Generic First-Order Logic (GFOL). On top of the former logic, introduced by Jose Meseguer in the early nineties as a unified model for concurrency, we have developed a continuation-based technique and notation called K, that allows the language specifier to directly and conveniently focus on the desired aspects of the language. The latter logic, GFOL, is essentially a first-order logic that makes no commitment to the particular structure of terms, so long as they come with a suitable notion of substitution. Lambda Calculi definitions can be conveniently expressed in GFOL, in such a way that the GFOL built-in semantics provides meaningful models for the specified calculus. We believe that combining Rewriting Logic (and in particular K) with GFOL via some back and forth mappings between logical systems would provide a powerful operational, proof-theoretical, and model-theoretical setting for defining, prototyping, and reasoning about programming languages and calculi.
Rewriting Logic Semantics unifies (algebraic) denotational and operational semantics: by regarding a rewrite logic language definition from a "designated model" point of view one obtains a denotational semantics, while by executing that same definition one obtains an operational semantics. Additionally, general purpose analysis techniques for rewrite logic specifications translate into corresponding analysis techniques for the defined languages. We are currently using Maude as a rewrite logic framework and thus, from a Maude formal language or system definition, we currently obtain for free the following: a parser for that language, an interpreter, a search engine for safety property violations, and a model checker. Rewrite logic semantics is being used in several courses taught at UIUC and has been used to formally define several (large fragments of) programming languages, including: Java, Scheme, Haskell, LISP, Beta, Smalltalk, Pict, Python, etc. We aim at modular design of programming language concepts, so that, once defined, features can be used across different programming languages. Also, one can easily modify or extend a programming language rewrite logic definition, so one can rapidly prototype and experiment with new languages and paradigms, as well as with program analysis and/or transformation techniques.
Built upon a (first-order) continuation-based technique and a series of notational conventions, K is a programming language definitional framework which allows for more compact and modular language definitions than plain rewriting logic. K definitions can be mechanically translated into rewriting logic and in particular into Maude to obtain program analysis tools or interpreters based on term rewriting, or into C to obtain more efficient interpreters. K is not an alternative to rewrite logic semantics, but rather a programming language specific shell for it.
GFOL is a logic whose formulae are built using the traditional first-order connectives and quantifiers, but whose terms are generic, in the sense that no particular syntax is assumed for them. Terms are only required to constitute a term syntax, i.e., to have free variables and substitution that obey some natural axioms. Classical first-order terms, as well as any type of terms involving bindings, fall into this category. GFOL models are simply required to interpret terms in their carrier sets in a way that is consistent with substitution. Classical first-order models, as well as various forms of Henkin models for typed and untyped calculi, are particular cases of GFOL models. It turns out that many classical-FOL constructions and results, including completeness and the existence of initial models, can be performed at the GFOL generic level. And moreover, many lambda calculi can be viewed as (and not merely encoded as) theories in GFOL. These have an important methodological consequence for our calculi- and programming-languages- specification goals: the "general purpose" GFOL semantics offers, in a uniform way, meaningful semantics for each particular specified calculus.