𝕋he pure \(\lambda\)-calculus contains only functions as values. It is not exactly easy to write large or interesting programs in the pure \(\lambda\)-calculus. We can however encode objects, such as … Read More →

𝕎e have now seen two operational models for programming languages: small-step and large-step. In this nnote, we consider a different semantic model, called denotational semantics. The idea in … Read More →

𝕋he small-step and large-step semantics are equivalent as captured by the following theorem. Theorem. For all commands $c$ and stores $\sigma$ and $\sigma'$ we have […] The proof is left as an … Read More →

𝕎e will now consider a more realistic programming language, one where we can assign values to variables and execute control constructs such as if and while. The syntax for this imperative language, … Read More →

𝕀n the last lecture we defined a semantics for our language of arithmetic expressions using a small-step evaluation relation $\rightarrow \subseteq \mathbf{Config}\times \mathbf{Config}$ (and its … Read More →

𝕀n this note, we will use the semantics of our simple language of arithmetic expressions, […] to express useful program properties, and we will prove these properties by induction. […] … Read More →

𝕎hat is the meaning of a program? When we write a program, we represent it using sequences of characters. But these strings are just concrete syntax—they do not tell us what the program actually … Read More →