NPRG085: Theory of Programming Languages
Properties of a small imperative language
Tomáš Petříček and Vít Šefl
petricek@d3s.mff.cuni.cz | sefl@ksvi.mff.cuni.cz
@tomasp.net | https://tomasp.net
Properties
Programming language theories
Scala and Java
are unsound
Unexpected interaction between subtyping and implicit nulls.
Sound in isolation!
Why bother with properties?
Understanding subtle cases
- What relates to what
- Corner cases worth checking
- Basis for larger proofs
What we want to know
- Language evaluation is deterministic
- Type system is sound
- Type inference is decidable
Language evaluation is deterministic
Theorem (Determinacy)
If \(\langle e, s \rangle \rightarrow \langle e', s'\rangle\) and
also \(\langle e, s \rangle \rightarrow \langle e'', s''\rangle\)
then \(e'=e''\) and \(s'=s''\).
Property of evaluation
- No mention of types - just reduction relation
- Not necessarily through the same reduction!
- Does not hold for some languages (e.g., concurrency)
Well-typed programs do not get stuck
Theorem (Safety)
If \(\Gamma \vdash e : \tau\) and \(dom(\Gamma)\subseteq dom(s)\) and
\(\langle e, s \rangle \rightarrow^{*} \langle e', s'\rangle\)
then either
\(e'\) is a value or there exist \(e'', s''\) such
that \(\langle e', s' \rangle \rightarrow \langle e'', s''\rangle\).
Combination of two properties
- Progress - a well-typed program is a value or can reduce
- Preservation - reduction preserves the type of a program
Induction
Proof technique
Three forms of induction
Induction over natural numbers
\(\forall x\in\mathbb{N}.\Phi(x)\) if \(\Phi(0)\) and \(\Phi(x)\Rightarrow\Phi(x+1)\)
Induction over structure of a term
Show that \(\forall e\in\mathbb{E}.\Phi(e)\) by showing \(\Phi(e)\) holds for
leaves and \(\Phi(e_1),\ldots,\Phi(e_n) \Rightarrow \Phi(\texttt{op}(e_1, \ldots, e_n))\)
Induction over a relation
Show that \(\forall x.R(x) \Rightarrow \Phi(x)\) by showing \(\Phi(J)\) holds for axioms (no assumptions) and \(\Phi(x)\) follows from assumptions \(\Phi(x_1), \ldots, \Phi(x_n)\) for each rule \(\dfrac{x_1, \ldots, x_n}{x}\).
Induction
Three properties
- Determinacy - induction over term structure
- Progress - induction over \(\vdash\) relation
- Preservation - induction over \(\rightarrow\) relation
- Safety - induction over \(\rightarrow^{*}\) relation
Determinacy
Property of evaluation
Determinacy
Induction over the structure of expressions
Determinacy
See details (PDF)
Remarks
Values do not reduce
Careful treatment of what rules could have been used
Soundness
Progress and preservation
Progress
Induction over the derivation of \(\vdash\)
Progress
See details (PDF)
Remarks
Inversion lemma to know what values can have a given type
Preservation
Induction over the derivation of \(\rightarrow\)
Progress
See details (PDF)
Remarks
Induction over reduction relation, assuming any
context \(\Gamma\) and type \(\tau\)
Well-typed programs do not get stuck
Theorem (Safety)
If \(\Gamma \vdash e : \tau\) and \(dom(\Gamma)\subseteq dom(s)\) and
\(\langle e, s \rangle \rightarrow^{*} \langle e', s'\rangle\)
then either
\(e'\) is a value or there exist \(e'', s''\) such
that \(\langle e', s' \rangle \rightarrow \langle e'', s''\rangle\).
Proof by induction
Induction over \(\rightarrow^{*}\). Reduction preserves type (preservation) and thus becomes value or can continue further (progress).
Conclusions
Properties of a small imperative language
Conclusions
- Phew, proving this is really hard!
- Same structure for verified proofs in Rocq/Lean
- Induction over terms or relations is useful!
- Progress and preservation is a good framing