CS 4110: Programming Languages and Logics

How would we add concurrent composition to IMP? For example, if $\sigma(x) = \sigma(y) = 0$ and $$x := y + 1 ; y := y + 1 \ || \ y := y + 1,$$ then what is $\sigma^\prime$? If we use big-step semantics, it kind of defeats the point of concurrency, where we want multiple computations to be interleaved. For small-step rules, we might say $$\frac{\langle \sigma, c_1 \rangle \to \langle \sigma^\prime, c_1^\prime\rangle}{\sigma, c_1 \ || c_2 \rangle \to \langle \sigma^\prime, c_1^\prime \ || \ c_2 \rangle}$$ ...

This lecture is taught by Dexter Kozen and is about a simple imperative language called IMP. It has arithmetic expressions: $a \in \text{Aexp} \quad a ::= x | n | a_1 + a_2 | a_1 \times a_2$. Boolean expressions: $b \in \text{Bexp} \quad b::= \text{true} | \text{false} | a_1 < a_2$. commands: $c \in \text{Com} \quad c::= \text{skip} | x := a | c_1 ; c_2 | \text{if } b \text{ then } c_1 \text{ else } c_2 | \text{while } b \text{ do } c$. This is the syntax of the language. To describe the (small-step) semantics, we can define three relations, which tell us which store and arithmetic expression pairs can step to which store and arithmetic expression pair, and the same for boolean expression and commands. ...

We can write a grammar for OCaml-style lists: $$\begin{aligned} e ::&= n \\ |& \ [ \ ] \\ |& \ e_1 :: e_2 \\ |& \ e_1 @ e_2 \\ |& \ \text{rev } e \\ |& \ \text{len } e \end{aligned}$$ along with $\ell ::= [ \ ] \ | \ n :: \ell$ and $v ::= n \ | \ \ell$. Now, we can define the big-step semantics using the notation $e \Downarrow v$. We need a reflexive rule and a nil rule, but the cons rule looks like this: ...

Progress Recall the progress property that we discussed last lecture that helps us prove that any well-formed configuration eventually steps to some integer. We want to prove that for all$e \in \text{Exp}$, $P(e)$ holds, where $$P(e):= \forall \sigma \in \text{Store} \ . \ \text{wf}(\sigma, e) \implies C(\sigma, e),$$ where $$C(\sigma, e) := e \in \text{Int} \lor \exists \sigma^\prime \in \text{Store}, e^\prime \in \text{Exp} \ . \ \langle \sigma, e\rangle \to \langle \sigma^\prime, e^\prime\rangle.$$ ...

Inference Rules Suppose that $\sigma$ is some store that maps foo to 4. Consider $\langle \sigma, (\texttt{foo} + 2) \times (\texttt{bar} + 1)\rangle$. In this case, the only inference rule that applies here is the one that allows the left side of the product to take a step. Doing this repeatedly results in a proof tree which shows how we can go from the original configuration to the “final” configuration: ...

What is the meaning of a program? We could execute the program or consult a manual, but these are not satisfactory approaches because the program could execution could not work and manuals are not speciic. A simple language we could look at is that of arithmetic expressions with assignment. First we establish some metavariables. We can establish $x, y, z \in \text{Var}$ (variables), let $n, m \in \text{Int}$ (integers), and let $e \in \text{Exp}$ (expressions). ...

This lecture serves as theater, e.g. to show why studying programming languages might be cool. Programming Language Quirk Examples One cool example of programming languages being weird is how [] + [], [] + {}, {} + [], and {} + {} all evaluate to different things in JavaScript. If we run a = [1], 2 and then a[0] += [3], you might think we would have a = [1, 3], 2, but in Python, tuples are not mutable, so we get an error. However, after the error, a still evaluates as ([1, 3], 2). Why does this happen? At the source level, it might look like if the += line threw an error, then its side effects wouldn’t happen. But, if we look at the bytecode representation (by using the dis module), we see that is actually not the case. ...