Formal Semantics of Programs

The need for formal semantics traditional approaches to language semantics for programming were informal, with disastrous results (e.g., inconsistent behavior of compilers)

Formal Semantics of Programs

	The need for formal semantics
	Strachey's Denotational Semantics in the 1960s and 70s, Strachey showed how lambda calculus can be used to give formal, mathematical meanings to programming language constructs

Formal Semantics of Programs

	The need for formal semantics
	Strachey's Denotational Semantics
	Compositionality of meaning the style of denotational semantics follows mathematical logic/model theory; we present: • a term structure (usually via CFG); • a type system (to reflect context-sensitive aspects); • a semantic domain (built in a known math. meta-language); • and a meaning function (compositional mapping on language constructs).

Formal Semantics of Programs

	The need for formal semantics
	Strachey's Denotational Semantics
	Compositionality of meaning
	Scott's Domain Theory Dana Scott established lambda calculus as an appropriate mathematical meta-language by giving it a semantics in terms of lattices and continuous functions (especially to model recursion, self-reference)

Formal Semantics of Programs

	The need for formal semantics
	Strachey's Denotational Semantics
	Compositionality of meaning
	Scott's Domain Theory
	Other formal semantics of programs other approaches to formal semantics have also been explored (operational, algebraic, abstract machines, etc.); they vary in levels of abstraction (e.g., how overtly they specify computational steps) (interestingly, they are often not viewed as competitive alternatives, but as opportunities for perspective, via coherence results)