Is lambda calculus suitable for expressing semantics of non-functional languages?

Question

Would it be convenient to express semantics of imperative languages (e.g. C) and object-oriented languages (e.g. Java) with $\lambda$-calculus?

Or in the other words: is $\lambda$-calculus a suitable candidate for expressing semantics of all context-sensitive languages?

Answer 1

There are two main approaches to giving the semantics of a language that I'm aware of. $\lambda$-calculus is a suitable candidate for expressing semantics in either approach. (Note that my knowledge of programming language semantics is restricted to a single course that I took in the mid-1990s, so I may be missing significant developments from the past 20 years.)

The first approach is operational semantics. According to David Schmidt's Denotational Semantics, Allyn&Bacon, 1986, page 2, operational semantics "uses an interpreter to define a language." In this sense writing a syntax-directed translator or attribute grammar as an extension of your parser gives an operational semantics to the language. Somewhat more abstractly, you might define a small-step operational semantics (like those on the Wikipedia page) where you define the meaning of each syntactic expression with respect to the actions it takes to transform a formally defined state or environment. The imperative programming language Scheme (which is notable for having "first-class" functions and continuations and as being the progenitor of JavaScript) has switched to an operational semantics in their most recent standard.

The other approach is denotational semantics. In denotational semantics you define a domain of program outcomes, and then for every syntactic structure in the program its meaning is a function that maps from an environment (a map from variable names to values) to the outcome domain. Scheme Revision⁵ and earlier have denotational semantics. The semantics of set! (Scheme's imperative construct) are given towards the end of Page 41.

I would guess that language semantics are largely used to prove the correctness of implementations, and in particular to clarify what optimizations are legal and under what circumstances those optimizations are legal. But my only experience in this domain is with respect to compiler optimizations and the memory semantics of C++11, which does not have a formal semantics.