COMP3610/6361
Principles of Programming Languages
Peter Ho¨fner
Aug 16, 2023
1
Section 0
Admin
2
Lecturer
• A/Prof. Peter Ho¨fner
CSIT, Room N234 (Building 108)
Peter.Hoefner@anu.edu.au
+61 2 6125 0159
Consultation
Thursday 12pm – 1pm, or by appointment
3
CoLecturer and Tutors
• Dr Fabian Muelboeck
Fabian.Muehlboeck@anu.edu.au
• Abhaas Goyal
Abhaas.Goyal@anu.edu.au
• Weiyou Wang
Weiyou.Wang@anu.edu.au
4
Lectures
• Wednesday, 3 pm – 5 pm
Thursday, 11 am – 12 pm
• Rm 5.02 Marie Reay, Bldg 155
• Q/A session in Week 12
• Etiquette
▶ engage
▶ feel free to ask questions
▶ we reject behaviour that strays into harassment,
no matter how mild
5
Tutorials
• join one of the 2 tutorials
• Thursday, 3pm – 5pm (Rm 5.03 Marie Reay)
Friday, 1pm – 2pm (Rm 5.03 Marie Reay)
• from Week 2 onwards
• Summary
▶ your chance to discuss problems
▶ discuss home work
▶ discuss additional exercises
6
Plan/Schedule I
Resources
web: https://cs.anu.edu.au/courses/comp3610/
wattle: https://wattlecourses.anu.edu.au/course/view.php?id=41142
edstem: https://edstem.org/
(you will be registered at the end of the week)
Workload
The average student workload is 130 hours for a six unit course.
That is roughly 11 hours/week.
https://policies.anu.edu.au/ppl/document/ANUP_000691
7
Plan/Schedule II
Assessment criteria
• Quizz: 0% (for feedback only)
• Assignments: 35%, 4 assignments (35marks)
• Oral exam: 65% (65 marks) [hurdle]
• hurdle: minimum of 40% in the final exam
Assessments (tentative)
No Hand Out Hand In Marks
0 31/07 03/08 0
1 02/08 10/08 5
2 16/08 31/08 10
3 20/09 12/10 10
4 18/10 02/11 10
8
About the Course I
This course is an introduction to
the theory and design of programming languages.
9
About the Course II
Topics (tentative)
The following schedule is tentative and likely to change.
Topic
0 Admin
1 introduction
2 IMP and its Operational Semantics
3 Types
4 Derivation and Proofs
5 Functions, Call-by-Value, Call-by-Name
6 Typing for Call-By-Value
7 Data Types and Subtyping
8 Denotational Semantics
9 Axiomatic Semantics
10 Concurrency
11 Formal Verification
10
About the Course IV
Disclaimer
This is has been redesigned fairly recently.
The material in these notes has been drawn from several different
sources, including the books and similar courses at some other
universities. Any errors are of course all the author’s own work.
As it is a newly designed course, changes in timetabling are quite likely.
Feedback (oral, email, survey, . . . ) is highly appreciated.
11
Academic Integrity
• never misrepresent the work of others as your own
• if you take ideas from elsewhere
you must say so with utmost clarity
12
Reading Material
• Glynn Winskel. The Formal Semantics of Programming Languages
– An Introduction. MIT Press, 1993. ISBN 978-0-262-73103-4
• Robert Harper. Practical Foundations for Programming Languages.
Cambridge University Press, 2016. ISBN 978-1-107-15030-0
• Shriram Krishnamurthi. Programming Languages: Application and
Interpretation (2nd edition) Open Textbook Library, 2017
• additional reading material can be found online
13
Section 1
Introduction
14
Foundational Knowledge of Disciplines
Mechanical Engineering
Students learn about torque
d(r × ω)
dt
= r × dω
dt
+
dr
dt
× ω
Figure: Sydney Harbour Bridge under construction [NMA]
15
Foundational Knowledge of Disciplines
Electrical Engineering / Astro Physics
Students learn about complex impedance
ejωt = cos(ωt) + j sin(ωt)
Figure: Geomagnetic Storm alters Earth’s Magnetic field [Wikipedia]
16
Foundational Knowledge of Disciplines
Civil Engineering / Surveying
Students learn about trigonometry
sin(θ + ϕ) = sin θ cosϕ+ cos θ sinϕ
Figure: Surveying Swan River, WA [Wikipedia]
17
Foundational Knowledge of Disciplines
Software Engineering / Computer Science
Students learn about ???
Figure: First Ariane 5 Flight, 1996 [ESA] Figure: Heartbleed, 2014 [Wikipedia]
18
Programming Languages
Programming Languages: basic tools of computing
• what are programming languages?
• do they provide basic laws of software engineering?
• do they allow formal reasoning in the sense of above laws?
19
Constituents
• the syntax of programs:
the alphabet of symbols and a description of the well-formed
expressions, phrases, programs, etc.
• the semantics:
the meaning of programs, or how they behave
• often also the pragmatics:
description and examples of how the various features of the
language are intended to be used
20
Use of Semantics
• understand a particular language
what you can depend on as a programmer;
what you must provide as a compiler writer
• as a tool for language design:
▶ clear language design
▶ express design choices, understand language features and interaction
▶ for proving properties of a language, eg type safety, decidability of type
inference.
• prove properties of particular programs
21
Style of Description (Syntax and Semantics)
• natural language
• definition ‘by’ compiler behaviour
• mathematically
22
Introductory Examples: C
In C, if initially x has value 3, what is the value of the following?
x++ + x++ + x++ + x++
Is it different to the following?
x++ + x++ + ++x + ++x
23
Introductory Examples: C♯
In C♯, what is the output of the following?
delegate i n t IntThunk ( ) ;
c lass C {
p u b l i c s t a t i c vo id Main ( ) {
IntThunk [ ] funcs = new IntThunk [ 1 1 ] ;
f o r ( i n t i = 0 ; i <= 10; i ++)
{
funcs [ i ] = delegate ( ) { r e t u r n i ; } ;
}
foreach ( IntThunk f i n funcs )
{
System . Console . Wr i teL ine ( f ( ) ) ;
}
}
}
24
Introductory Examples: JavaScript
f u n c t i o n bar ( x ) {
r e t u r n f u n c t i o n ( ) {
var x = x ;
r e t u r n x ;
} ;
}
var f = bar ( 2 0 0 ) ;
f ( )
25
About This Course
• background: mathematical description of syntax by means of formal
grammars, e.g. BNF (see COMP1600)
clear, concise and precise
• aim I: mathematical definitions of semantics/behaviour
• aim II: understand principles of program design
(for a toy language)
• aim III: reasoning about programs
26
Use of formal, mathematical semantics
Implementation issues
Machine-independent specification of behaviour. Correctness of program
analyses and optimisations.
Language design
Can bring to light ambiguities and unforeseen subtleties in programming
language constructs. Mathematical tools used for semantics can suggest
useful new programming styles. (E.g. influence of Church’s lambda
calculus (circa 1934) on functional programming).
Verification
Basis of methods for reasoning about program properties and program
specifications.
27
Styles of semantics
Operational
Meanings for program phrases defined in terms of the steps of
computation they can take during program execution.
Denotational
Meanings for program phrases defined abstractly as elements of some
suitable mathematical structure.
Axiomatic
Meanings for program phrases defined indirectly via the axioms and
rules of some logic of program properties.
28
Section 2
IMP
and its Operational Semantics
29
‘Toy’ languages
• real programming languages are large
many features, redundant constructs
• focus on particular aspects and abstract from others (scale up later)
• even small languages can involve delicate design choices.
30
Design choices, from Micro to Macro
• basic values
• evaluation order
• what is guaranteed at compile-time and run-time
• how effects are controlled
• how concurrency is supported
• how information hiding is enforceable
• how large-scale development and re-use are supported
• . . .
31
IMP1– Introductory Example
IMP is an imperative language with store locations, conditionals and
while loop.
For example
l2 := 0 ;
while !l1 ≥ 1 do (
l2 := !l2 + !l1 ;
l1 := !l1 + −1
)
with initial store {l1 7→ 3, l2 7→ 0}.
1Basically the same as in Winskel 1993 (IMP) and in Hennessy 1990 (WhileL)
32
IMP – Syntax
Booleans b ∈ B = {true, false}
Integers (Values) n ∈ Z = {. . . ,−1, 0, 1, . . . }
Locations l ∈ L = {l, l0, l1, l2, . . . }
Operations op ::= + | ≥
Expressions
E ::= n | b | E op E |
l := E | !l |
skip | E ; E |
if E then E else E
while E do E
33
Transition systems
A transition system consists of
• a set Config of configurations (or states), and
• a binary relation −→⊆ Config× Config.
The relation −→ is called the transition or reduction relation:
c −→ c′ reads as ‘state c can make a transition to state c′’.
(see DFA/NFA)
34
IMP Semantics (1 of 4) – Configurations
Stores are (finite) partial functions L⇀ Z.
For example, {l1 7→ 3, l3 7→ 42}
Configurations are pairs ⟨E , s⟩ of an expression E and a store s.
For example, ⟨l := 2 + !l , {l 7→ 3}⟩.
Transitions have the form ⟨E , s⟩ −→ ⟨E′ , s′⟩.
For example, ⟨l := 2 + !l , {l 7→ 3}⟩ −→ ⟨l := 2 + 3 , {l 7→ 3}⟩
35
Transitions – Examples
Transitions are single computation steps.
For example
⟨l := 2 + !l , {l 7→ 3}⟩
−→ ⟨l := 2 + 3 , {l 7→ 3}⟩
−→ ⟨l := 5 , {l 7→ 3}⟩
−→ ⟨skip , {l 7→ 5}⟩
−̸→
Keep going until reaching a value v, an expression in V = B∪Z∪{skip}.
A configuration ⟨E , s⟩ is stuck if E is not a value and ⟨E , s⟩ −̸→.
36
IMP Semantics (2 of 4) – Rules (basic operations)
(op+) ⟨n1 + n2 , s⟩ −→ ⟨n , s⟩ if n = n1 + n2
(op≥) ⟨n1 ≥ n2 , s⟩ −→ ⟨b , s⟩ if b = (n1 ≥ n2)
(op1)
⟨E1 , s⟩ −→ ⟨E′1 , s′⟩
⟨E1 op E2 , s⟩ −→ ⟨E′1 op E2 , s′⟩
(op2)
⟨E2 , s⟩ −→ ⟨E′2 , s′⟩
⟨v op E2 , s⟩ −→ ⟨v op E′2 , s′⟩
37
Rules (basic operations) – Examples
Find the possible sequences of transitions for
⟨(2 + 3) + (4 + 5) , ∅⟩
The answer is 14 – but how do we show this formally?
38
IMP Semantics (3 of 4) – Store and Sequencing
(deref) ⟨ !l , s⟩ −→ ⟨n , s⟩ if l ∈ dom(s) and s(l) = n
(assign1) ⟨l := n , s⟩ −→ ⟨skip , s + {l 7→ n}⟩
(assign2)
⟨E , s⟩ −→ ⟨E′ , s′⟩
⟨l := E , s⟩ −→ ⟨l := E′ , s′⟩
(seq1) ⟨skip;E2 , s⟩ −→ ⟨E2 , s⟩
(seq2)
⟨E1 , s⟩ −→ ⟨E′1 , s′⟩
⟨E1;E2 , s⟩ −→ ⟨E′1;E2 , s′⟩
39
Store and Sequencing – Examples
⟨l := 3 ; !l , {l 7→ 0}}⟩ −→ ⟨skip ; !l , {l 7→ 3}⟩
−→ ⟨ !l , {l 7→ 3}⟩
−→ ⟨3 , {l 7→ 3}⟩
40
Store and Sequencing – Examples
⟨l := 3 ; l := !l , {l 7→ 0}⟩ −→ ?
⟨42 + !l , ∅⟩ −→ ?
41
IMP Semantics (4 of 4) – Conditionals and While
(if1) ⟨if true then E2 else E3 , s⟩ −→ ⟨E2 , s⟩
(if2) ⟨if false then E2 else E3 , s⟩ −→ ⟨E3 , s⟩
(if3)
⟨E1 , s⟩ −→ ⟨E′1 , s′⟩
⟨if E1 then E2 else E3 , s⟩ −→ ⟨if E′1 then E2 else E3 , s′⟩
(while)
⟨while E1 do E2 , s⟩ −→ ⟨if E1 then (E2 ; while E1 do E2) else skip , s⟩
42
IMP – Examples
If
E =
(
l2 := 0 ; while !l1 ≥ 1 do (l2 := !l2 + !l1 ; l1 := !l1 + −1)
)
s = {l1 7→ 3, l2 7→ 0}
then
⟨E , s⟩ −→∗ ?
43
Determinacy
Theorem (Determinacy)
If ⟨E , s⟩ −→ ⟨E1 , s1⟩ and ⟨E , s⟩ −→ ⟨E2 , s2⟩
then ⟨E1 , s1⟩ = ⟨E2 , s2⟩.
Proof.
later
44
Reminder
• basic and simple imperative while-language
• with formal semantics
• given in the format structural operational semantics
• rules usually have the form
A B
C
(special rule is C, which we often write as C)
• derivation tree
(R1)
(R3)
A
(R4)
B1
(R5)
B2
B
(R2)
C
45
Language design I
Order of Evaluation
IMP uses left-to-right evaluation. For example
⟨(l := 1 ; 0) + (l := 2 ; 0) , {l 7→ 0}⟩ −→5 ⟨0 , {l 7→ 2}⟩
For right-to-left we could use
(op1’)
⟨E2 , s⟩ −→ ⟨E′2 , s′⟩
⟨E1 op E2 , s⟩ −→ ⟨E1 op E′2 , s′⟩
(op2’)
⟨E1 , s⟩ −→ ⟨E′1 , s′⟩
⟨E1 op v , s⟩ −→ ⟨E′1 op v , s′⟩
In this language
⟨(l := 1 ; 0) + (l := 2 ; 0) , {l 7→ 0}⟩ −→5 ⟨0 , {l 7→ 1}⟩
46
Language design II
Assignment results
Recall
(assign1) ⟨l := n , s⟩ −→ ⟨skip , s + {l 7→ n}⟩ if l ∈ dom(s)
(seq1) ⟨skip ; E2 , s⟩ −→ ⟨E2 , s⟩
We have chosen to map an assignment to skip, and e1 ; e2 to progress
iff e1 = skip.
Instead we could have chosen the following.
(assign1’) ⟨l := n , s⟩ −→ ⟨n , s + {l 7→ n}⟩ if l ∈ dom(s)
(seq1’) ⟨v ; E2 , s⟩ −→ ⟨E2 , s⟩
47
Language design III
Store initialisation
Recall
(deref) ⟨ !l , s⟩ −→ ⟨n , s⟩ if l ∈ dom(s) and s(l) = n
Assumes l ∈ dom(s).
Instead we could have
• initialise all locations to 0, or
• allow assignments to an l ̸∈ dom(s).
48
Language design IV
Storable values
• our language only allows integer values (store: L⇀ Z)
• could we store any value? Could we store locations, or even
programs?
• store is global and cannot create new locations
49
Language design V
Operators and Basic values
• Booleans are different from integers (unlike in C)
• Implementation is (probably) different to semantics
Exercise: fix the semantics to match 32-bit integers
50
Expressiveness
Is our language expressive enough to write ‘interesting’ programs?
• yes: it is Turing-powerful
Exercise: try to encode an arbitrary Turing machine in IMP
• no: no support for standard feature, such as functions, lists, trees,
objects, modules, . . .
Is the language too expressive?
• yes: we would like to exclude programs such as 3 + true
clearly 3 and true are of different type
51
Section 3
Types
52
Type systems
• describe when programs make sense
• prevent certain kinds of errors
• structure programs
• guide language design
Ideally, well-typed programs do not get stuck.
53
Run-time errors
Trapped errors
Cause execution to halt immediately.
Examples: jumping to an illegal address, raising a top-level exception.
Innocuous?
Untrapped errors
May go unnoticed for a while and later cause arbitrary behaviour.
Examples: accessing data past the end of an array, security loopholes in
Java abstract machines.
Insidious!
Given a precise definition of what constitutes an untrapped run-time
error, then a language is safe if all its syntactically legal programs cannot
cause such errors. Usually, safety is desirable. Moreover, we’d like as
few trapped errors as possible.
54
Formal type systems
We define a ternary relation Γ ⊢ E :T
expression E has type T , under assumptions Γ on the types of locations
that may occur in E.
For example (according to the definition coming up):
• {} ⊢ if true then 2 else 3 + 4 : int
• l1 : intref ⊢ if !l1 ≥ 3 then !l1 else 3 : int
• {} ⊬ 3 + true : T for any type T
• {} ⊬ if true then 3 else true : int
55
Types of IMP
Types of expressions
T ::= int | bool | unit
Types of locations
Tloc ::= intref
We write T and Tloc for the sets of all terms of these grammars.
• Γ ranges over TypeEnv, the finite partial function from L⇀ Z
• notation: write l1 : intref, . . . , lk : intref instead of
{l1 7→ intref, . . . , lk 7→ intref}
56
Type Judgement (1 of 3)
(int) Γ ⊢ n : int if n ∈ Z
(bool) Γ ⊢ b :bool if b ∈ B = {true, false}
(op+)
Γ ⊢ E1 : int Γ ⊢ E2 : int
Γ ⊢ E1 + E2 : int
(op≥) Γ ⊢ E1 : int Γ ⊢ E2 : int
Γ ⊢ E1 ≥ E2 :bool
(if)
Γ ⊢ E1 :bool Γ ⊢ E2 :T Γ ⊢ E3 :T
Γ ⊢ if E1 then E2 else E3 :T
57
Type Judgement – Example
Prove that {} ⊢ if false then 2 else 3 + 4 : int.
{} ⊢ false :bool (BOOL) {} ⊢ 2 : int (INT)
(INT) {} ⊢ 3 : int {} ⊢ 4 : int (INT)
{} ⊢ 3 + 4 : int (OP+)
{} ⊢ if false then 2 else 3 + 4 : int (IF)
58
Type Judgement (2 of 3)
(assign)
Γ(l) = intref Γ ⊢ E : int
Γ ⊢ l := E :unit
(deref)
Γ(l) = intref
Γ ⊢ !l : int
Here, (for the moment) Γ(l) = intref means l ∈ dom(Γ)
59
Type Judgement (3 of 3)
(skip) Γ ⊢ skip :unit
(seq)
Γ ⊢ E1 :unit Γ ⊢ E2 :T
Γ ⊢ E1 ; E2 :T
(while)
Γ ⊢ E1 :bool Γ ⊢ E2 :unit
Γ ⊢ while E1 do E2 :unit
60
Type Judgement – Properties
Theorem (Progress)
If Γ ⊢ E :T and dom(Γ) ⊆ dom(s) then either E is a value or there exist
E′ and s′ such that ⟨E , s⟩ −→ ⟨E′ , s′⟩.
Theorem (Type Preservation)
If Γ ⊢ E :T , dom(Γ) ⊆ dom(s) and ⟨E , s⟩ −→ ⟨E′ , s′⟩ then Γ ⊢ E′ :T
and dom(Γ) ⊆ dom(s′).
61
Type Safety
Main result: Well-typed programs do not get stuck.
Theorem (Type Safety)
If Γ ⊢ E :T , dom(Γ) ⊆ dom(s), and ⟨E , s⟩ −→∗ ⟨E′ , s′⟩ then either E′ is
a value with Γ ⊢ E′ :T , or there exist E′′, s′′ such that
⟨E′ , s′⟩ −→ ⟨E′′ , s′′⟩, Γ ⊢ E′′ :T and dom(Γ) ⊆ dom(s′′).
Here, −→∗ means arbitrary many steps in the transition system.
62
Type checking, typeability, and type inference
Type checking problem for a type system:
given Γ, E and T , is Γ ⊢ E :T derivable?
Type inference problem:
given Γ and E, find a type T such that Γ ⊢ E :T is derivable, or show
there is none.
Type inference is usually harder than type checking, for a type T needs
to be computed.
For our type system, though, both are easy.
63
Properties
Theorem (Type inference)
Given Γ and E , one can find T such that Γ ⊢ E :T , or show that there is
none.
Theorem (Decidability of type checking)
Given Γ, E and T , one can decide whether Γ ⊢ E :T holds.
Moreover
Theorem (Uniqueness of typing)
If Γ ⊢ E :T and Γ ⊢ E :T ′ then T = T ′.
64
Section 4
Proofs (Structural Induction)
65
Why Proofs
• how do we know that the stated theorems are actually true?
intuition is often wrong – we need proof
• proofs strengthen intuition about language features
• examines all the various cases
• can guarantee items such as type safety
• most of our definitions are inductive; we use structural induction
66
(Mathematical) Induction
Mathematical induction proves that we can climb as high as we
like on a ladder, by proving that we can climb onto the bottom
rung (the basis) and that from each rung we can climb up to the
next one (the step).
[Concrete Mathematics (1994), R. Graham]
67
Natural Induction I
A proof by (natural) induction consists of two cases.
The base case proves the statement for n = 0 without assuming any
knowledge of other cases.
The induction step proves that if the statement holds for any given case
n = k, then it must also hold for the next case n = k + 1.
68
Natural Induction II
Theorem
∀n ∈ IN .Φ(n).
Proof.
Base case: show Φ(0)
Induction step: ∀k. Φ(k) =⇒ Φ(k + 1)
For that we fix an arbitrary k.
Assume Φ(k) derive Φ(k + 1).
Example: 0 + 1 + 2 + · · ·+ n = n·(n+1)2 .
69
Natural Induction III
Theorem
∀n ∈ IN .Φ(n).
Proof.
Base case: show Φ(0)
Induction step: ∀i, k.0 ≤ i ≤ k. Φ(i) =⇒ Φ(k + 1)
For that we fix an arbitrary k.
Assume ϕ(i) for all i ≤ k derive ϕ(k + 1).
Example: Fn = φ
n−ψn
φ−ψ ,
with Fn is the n-th Fibonacci number, φ = 1+
√
5
2 (the golden ratio) and
ψ = 1−
√
5
2 .
70
Structural Induction I
• generalisation of natural induction
• prove that some proposition Φ(x) holds for all x of some sort of
recursively defined structure
• requires well-founded partial order
Examples: lists, formulas, trees
71
Structural Induction II
Determinacy structural induction for E
Progress rule induction for Γ ⊢ E :T
(induction over the height of derivation tree)
Type Preservation rule induction for ⟨E , s⟩ −→ ⟨E′ , s′⟩
Safety mathematical induction on −→n
Uniqueness of typing . . .
Decidability of typability exhibiting an algorithm
Decidability of type checking corollary of other results
72
Structural Induction over Expressions
Prove facts about all expressions, e.g. Determinacy?
Theorem (Determinacy)
If ⟨E , s⟩ −→ ⟨E1 , s1⟩ and ⟨E , s⟩ −→ ⟨E2 , s2⟩
then ⟨E1 , s1⟩ = ⟨E2 , s2⟩.
Do not forget the elided universal quantifiers.
Theorem (Determinacy)
For all E, s, E1, s1, E2 and s2,
if ⟨E , s⟩ −→ ⟨E1 , s1⟩ and ⟨E , s⟩ −→ ⟨E2 , s2⟩
then ⟨E1 , s1⟩ = ⟨E2 , s2⟩.
73
Abstract Syntax
Remember the definition of expressions:
E ::= n | b | E op E |
l := E | !l |
if E then E else E |
skip | E ; E |
while E do E
This defines an (infinite) set of expressions.
74
Abstract Syntax Tree I
Example: if !l ≥ 0 then skip else (skip ; l := 0)
if then else
≥
!l 0
skip ;
skip l :=
0
75
Abstract Syntax Tree II
• equivalent expressions are not the same, e.g., 2 + 2 ̸= 4
+
2 2 4
• ambiguity, e.g., (1 + 2) + 3 ̸= 1 + (2 + 3)
+
+
1 2
3
+
1 +
2 3
Parentheses are only used for disambiguation – they are not part of
the grammar
76
Structural Induction (for abstract syntax)
Theorem
∀E ∈ IMP. Φ(E)
Proof.
Base case(s): show Φ(E) for each unary tree constructor (leaf)
Induction step(s): show it for the remaining constructors
∀c. ∀E1, . . . Ek. (Φ(E1) ∧ · · · ∧ Φ(Ek)) =⇒ Φ(c(E1, . . . , Ek))
77
Structural Induction (syntax IMP)
To show ∀E ∈ IMP. Φ(E).
base cases
nullary: Φ(skip)
∀b ∈ B. Φ(b)
∀n ∈ Z. Φ(n)
∀l ∈ L. Φ( !l)
steps
unary: ∀l ∈ L. ∀E. Φ(E) =⇒ Φ(l := E)
binary: ∀op. ∀E1, E2. (Φ(E1) ∧ Φ(E2)) =⇒ Φ(E1 op E2)
∀E1, E2. (Φ(E1) ∧ Φ(E2)) =⇒ Φ(E1 ; E2)
∀E1, E2. (Φ(E1) ∧ Φ(E2)) =⇒ Φ(while E1 do E2)
ternary: ∀E1, E2, E3. (Φ(E1) ∧ Φ(E2) ∧ Φ(E3))
=⇒ Φ(if E1 then E2 else E3)
78
Proving Determinacy – Outline
Theorem (Determinacy)
For all E, s, E1, s1, E2 and s2,
if ⟨E , s⟩ −→ ⟨E1 , s1⟩ and ⟨E , s⟩ −→ ⟨E2 , s2⟩
then ⟨E1 , s1⟩ = ⟨E2 , s2⟩.
Proof.
Choose
Φ(E)
def
= ∀s, E′, s′, E′′, s′′.
(⟨E , s⟩ −→ ⟨E′ , s′⟩ ∧ ⟨E , s⟩ −→ ⟨E′′ , s′′⟩)
=⇒ ⟨E′ , s′⟩ = ⟨E′′ , s′′⟩
and show Φ(E) by structural induction over E.
79
Proving Determinacy – Sketch
Some cases on whiteboard
80
Proving Determinacy – auxiliary lemma
Values do not reduce.
Lemma
For all E ∈ IMP, if E is a value then
∀s. ¬(∃E′, s′. ⟨E , s⟩ −→ ⟨E′ , s′⟩).
Proof.
• E is a value iff it is of the form n, b, skip
• By examination of the rules . . .
there is no rule with conclusion of the form ⟨E , s⟩ −→ ⟨E′ , s′⟩ for E
a value
81
Inversion I
In proofs involving inductive definitions. one often needs an inversion
property.
Given a tuple in one inductively defined relation, gives you a case
analysis of the possible “last rule” used.
Lemma (Inversion for −→)
If ⟨E , s⟩ −→ ⟨Eˆ , sˆ⟩ then either
1. (op+): there exists n1, n2 and n such that E = n1 op n2, Eˆ = n,
sˆ = s and n = n1 + n2,
(Note: +s have different meanings in this statements), or
2. (op1): there exists E1, E2, op and E′1 such that E = E1 op E2,
Eˆ = E′1 op E2 and ⟨E1 , s⟩ −→ ⟨E′1 , s′⟩, or
3. . . .
82
Inversion II
Lemma (Inversion for ⊢)
If Γ ⊢ E :T then either
• . . .
83
Determinacy – Intuition
The intuition behind structural induction over expressions. Consider
( !l + 2) + 3. How can we see that Φ(( !l + 2) + 3) holds?
+
+
!l 2
3
84
Rule Induction
How to prove the following theorems?
Theorem (Progress)
If Γ ⊢ E :T and dom(Γ) ⊆ dom(s) then either E is a value or there exist
E′ and s′ such that ⟨E , s⟩ −→ ⟨E′ , s′⟩.
Theorem (Type Preservation)
If Γ ⊢ E :T , dom(Γ) ⊆ dom(s) and ⟨E , s⟩ −→ ⟨E′ , s′⟩ then Γ ⊢ E′ :T
and dom(Γ) ⊆ dom(s′).
85
Inductive Definition of −→
What does ⟨E , s⟩ −→ ⟨E′ , s′⟩ actually mean?
We defined the transition relation by providing some rules, such as
(op+) ⟨n1 + n2 , s⟩ −→ ⟨n , s⟩ if n = n1 + n2
(op1)
⟨E1 , s⟩ −→ ⟨E′1 , s′⟩
⟨E1 op E2 , s⟩ −→ ⟨E′1 op E2 , s′⟩
These rules (their concrete instances) inductively/recursively define a set
of derivation trees. The last step in the derivation tree defines a step in
the transition system.
We define the (infinite) set of all finite derivation trees
86
Derivation Tree (Transition Relation) – Example
⟨2 + 2 , {}⟩ −→ ⟨4 , {}⟩ (OP+)
⟨(2 + 2) + 3 , {}⟩ −→ ⟨4 + 3 , {}⟩ (OP1)
⟨(2 + 2) + 3 ≥ 5 , {}⟩ −→ ⟨4 + 3 ≥ 5 , {}⟩ (OP1)
87
Derivation Tree (Typing Judgement) – Example
Γ(l) = intref
Γ ⊢!l : int (DERREF) Γ ⊢ 2 : int (INT)
Γ ⊢ !l + 2 : int (OP+) Γ ⊢ 3 : int (INT)
Γ ⊢ ( !l + 2) + 3 : int (OP+)
88
Principle of Rule Induction I
For any property Φ(a) of elements a of A, and any set of rules which
define a subset SR of A, to prove
∀a ∈ SR. Φ(a)
it is enough to prove that {a | Φ(a)} is closed under the rules,
i.e., for each
h1 . . . hk
c
if Φ(h1) ∧ · · · ∧ Φ(hk) then Φ(c).
89
Principle of Rule Induction II
For any property Φ(a) of elements a of A, and any set of rules which
define a subset SR of A, to prove
∀a ∈ SR. Φ(a)
it is enough to prove that for each
h1 . . . hk
c
if Φ(h1) ∧ · · · ∧ Φ(hk) then Φ(c).
90
Proving Progress I
Theorem (Progress)
If Γ ⊢ E :T and dom(Γ) ⊆ dom(s) then either E is a value or there exist
E′ and s′ such that ⟨E , s⟩ −→ ⟨E′ , s′⟩.
Proof.
Choose
Φ(Γ, E, T ) = ∀s. dom(Γ) ⊆ dom(s)
=⇒ value(E) ∨ (∃E′, s′. ⟨E , s⟩ −→ ⟨E′ , s′⟩)
We show that for all Γ, E, T , if Γ ⊢ E :T then Φ(Γ, E, T ), by rule
induction on the definition of ⊢.
91
Proving Progress II
Rule induction for our typing rules means:
(int) ∀Γ, n. Φ(Γ, n, int)
(deref) ∀Γ, l. Γ(l) = intref =⇒ Φ(Γ, !l, int)
(op+) ∀Γ, E1, E2.
(
Φ(Γ, E1, int) ∧ Φ(Γ, E2, int) ∧ Γ ⊢ E1 : int ∧ Γ ⊢ E2 : int
)
=⇒ Φ(Γ, E1 + E2, int)
(seq) ∀Γ, E1, E2.
(
Φ(Γ, E1,unit) ∧ Φ(Γ, E2, T ) ∧ Γ ⊢ E1 :unit ∧ Γ ⊢ E2 :T
)
=⇒ Φ(Γ, E1;E2, int)
. . . [10 rules in total]
92
Proving Progress III
Φ(Γ, E, T ) = ∀s. dom(Γ) ⊆ dom(s)
=⇒ value(E) ∨ (∃E′, s′. ⟨E , s⟩ −→ ⟨E′ , s′⟩)
Case (op+):
(op+)
Γ ⊢ E1 : int Γ ⊢ E2 : int
Γ ⊢ E1 + E2 : int
• assume Φ(Γ, E1, int), Φ(Γ, E2, int), Γ ⊢ E1 : int and Γ ⊢ E2 : int
• we have to show Φ(Γ, E1 + E2, int)
• assume an arbitrary but fixed s, and dom(Γ) ⊆ dom(s)
• E1 + E2 is not a value; hence we have to show
∃E′, s′. ⟨E1 + E2 , s⟩ −→ ⟨E′ , s′⟩
93
Proving Progress IV
Case (op+) (cont’d):
• we have to show
∃E′, s′. ⟨E1 + E2 , s⟩ −→ ⟨E′ , s′⟩
• Using Φ(Γ, E1, int) and Φ(Γ, E2, int) we have
case E1 reduces. Then E1 + E2 does, by (op1).
case E1 is a value and E2 reduces. Then E1 + E2 does, by (op2).
case E1 and E2 are values; we want to use
(op+) ⟨n1 + n2 , s⟩ −→ ⟨n , s⟩ if n = n1 + n2
we assumed Γ ⊢ E1 : int and Γ ⊢ E2 : int we need E1 = n1 and
E2 = n2; then E1 + E2 reduces, by (op+).
94
Proving Progress V
Lemma
For all Γ, E, T , if Γ ⊢ E :T is a value with T = int
then there exists n ∈ Z with E = n.
95
Derivation Tree (Typing Judgement) – Example
Γ(l) = intref
Γ ⊢ !l : int (DEREF) Γ ⊢ 2 : int (INT)
Γ ⊢ !l + 2 : int (OP+) Γ ⊢ 3 : int (INT)
Γ ⊢ ( !l + 2) + 3 : int (OP+)
96
Which Induction Principle to Use?
• matter of convenience (all equivalent)
• use an induction principle that matches the definitions
97
Structural Induction (Repetition)
Determinacy structural induction for E
Progress rule induction for Γ ⊢ E :T
(induction over the height of derivation tree)
Type Preservation rule induction for ⟨E , s⟩ −→ ⟨E′ , s′⟩
Safety mathematical induction on −→n
Uniqueness of typing . . .
Decidability of typability exhibiting an algorithm
Decidability of type checking corollary of other results
98
Why care about Proofs?
1. sometimes it seems hard or pointless to prove things because they
are ‘obvious’, . . .
(in particular with our language)
2. proofs illustrate (and explain) why ‘things are obvious’
3. sometimes the obvious facts are false . . .
4. sometimes the obvious facts are not obvious at all
(in particular for ‘real’ languages)
5. sometimes a proof contains or suggests an algorithm that you need
(proofs that type inference is decidable (for fancier type systems))
6. force a clean language design
99
Section 5
Functions
100
Functions, Methods, Procedures, . . .
• so far IMP was really minimalistic
• the most important ‘add-on’ are functions
• this requires variables and other concepts
101
Examples
add one : : I n t −> I n t
add one n = n + 1
p u b l i c i n t add one ( i n t x ) {
r e t u r n ( x +1) ;
}

f u n c t i o n addone ( x )
addone = x+1
end f u n c t i o n

102
Introductory Examples: C♯
In C♯, what is the output of the following?
delegate i n t IntThunk ( ) ;
c lass C {
p u b l i c s t a t i c vo id Main ( ) {
IntThunk [ ] funcs = new IntThunk [ 1 1 ] ;
f o r ( i n t i = 0 ; i <= 10; i ++)
{
funcs [ i ] = delegate ( ) { r e t u r n i ; } ;
}
foreach ( IntThunk f i n funcs )
{
System . Console . Wr i teL ine ( f ( ) ) ;
}
}
}
In my opinion, the design was wrong.
103
Functions – Examples
We want include the following expressions:
(fn x : int ⇒ x + 1)
(fn x : int ⇒ x + 1) 7
(fn y : int ⇒ (fn x : int ⇒ x + y))
(fn y : int ⇒ (fn x : int ⇒ x + y)) 1
(fn x : int → int ⇒ (fn y : int ⇒ x (x y)))
(fn x : int → int ⇒ (fn y : int ⇒ x (x y))) (fn x : int ⇒ x + 1)(
(fn x : int → int ⇒ (fn y : int ⇒ x (x y))) (fn z : int ⇒ z + 1)) 7
104
Functions – Syntax
We extend our syntax:
Variables x ∈ X for a set X = {x, y, z, . . . } (countable)
Expressions
E ::= . . . | (fn x : T ⇒ E) | E E | x
Types
T ::= int | bool | unit | T → T
Tloc ::= intref
105
Variable Shadowing
(fn x : int ⇒ (fn x : int ⇒ x + 1))
106
Alpha conversion
In expressions (fn x : T ⇒ E), variable x is a binder
• inside E, any x (not being a binder themselves and not inside
another (fn x : T ′ ⇒ . . . )) mean the same
• it is the formal parameter of this function
• outside (fn x : T ⇒ E), it does not matter which variable we use – in
fact, we should not be able to tell
For example, (fn x : int ⇒ x + 2) should be the same as
(fn y : int ⇒ y + 2)
Binders are known from many areas of mathematics/logics.
107
Alpha conversion: free and bound variables
An occurrence x in an expression E is free if it is not inside any
(fn x : T ⇒ . . .).
For example:
17
x + y
(fn x : int ⇒ x + 2)
(fn x : int ⇒ x + z)
if y then 2 + x else ((fn x : int ⇒ x + 2) z)
108
Alpha Conversion – Binding Examples
(fn x : int ⇒ x + 2)
(fn x : int ⇒ x + z)
(fn y : int ⇒ y + z)
(fn z : int ⇒ z + z)
(fn x : int ⇒ (fn x : int ⇒ x + 2))
109
Alpha Conversion – Convention
• we want to allow to replace binder x (and all occurrences of x bound
by that x) by another binder y
• if it does not change the binding graph
For example
(fn x : int ⇒ x + z) = (fn y : int ⇒ y + z) ̸= (fn z : int ⇒ z + z)
• called ‘working up to alpha conversion’
• extend abstract syntax trees by pointers
110
Syntax Trees up to Alpha Conversion
(fn x : int ⇒ x + z) = (fn y : int ⇒ y + z) ̸= (fn z : int ⇒ z + z)
Standard abstract syntax trees
(fn x : int ⇒ )
+
x z
(fn y : int ⇒ )
+
y z
(fn z : int ⇒ )
+
z z
111
Syntax Trees up to Alpha Conversion II
(fn x : int ⇒ x + z) = (fn y : int ⇒ y + z) ̸= (fn z : int ⇒ z + z)
Add pointers
(fn • : int ⇒ )
+
• z
(fn • : int ⇒ )
+
• z
(fn • : int ⇒ )
+
• •
112
Syntax Trees up to Alpha Conversion III
(fn x : int ⇒ (fn x : int ⇒ x + 2))
= (fn y : int ⇒ (fn z : int ⇒ z + 2)) ̸= (fn z : int ⇒ (fn y : int ⇒ z + 2))
(fn • : int ⇒ )
(fn • : int ⇒ )
+
• z
(fn • : int ⇒ )
(fn • : int ⇒ )
+
• z
113
Syntax Trees up to Alpha Conversion IV
Application and function type
(fn x : int ⇒ x) 7 (fn z : int → int → int ⇒ (fn y : int ⇒ z y y))
@
(fn • : int ⇒ )
•
7
(fn • : int → int → int ⇒ )
(fn • : int ⇒ )
@
@
• •
•
114
De Bruijn indices
• these pointers are known as De Bruijn indices
• each occurrence of a bound variable is represented by the number
of fn-nodes you have to pass
(fn • : int ⇒ (fn • : int ⇒ v0 + 2)) ̸= (fn • : int ⇒ (fn • : int ⇒ v1 + 2))
(fn • : int ⇒ )
(fn • : int ⇒ )
+
• 2
(fn • : int ⇒ )
(fn • : int ⇒ )
+
• 2
115
Free Variables
• free variables of an expression E are the set of variables for which
there is an occurrence of x free in E
fv(x) = {x}
fv(E1 op E2) = fv(E1) ∪ fv(E2)
fv((fn x : T ⇒ E)) = fv(E)− {x}
• an expression E is closed if fv(E) = ∅
• For a set E of expressions fv(E) =
⋃
E∈E fv(E)
• these definitions are alpha-invariant
(all forthcoming definitions should be)
116
Substitution – Examples
• semantics of functions will involve substitution (replacement)
• {E/x}E′ denotes the expression E′ where all free occurrences of x
are substituted by E
Examples
{3/x} (x ≥ x) = (3 ≥ 3)
{3/x} ((fn x : int ⇒ x + y) x) = (fn x : int ⇒ x + y) 3
{y + 2/x} (fn y : int ⇒ x + y) = (fn z : int ⇒ (y + 2) + z)
117
Substitution
Definition
{E/z}x def=
{
E if x = z
x otherwise
{E/z} (fn x : T ⇒ E1) def= (fn x : T ⇒ ({E/z}E1)) if x ̸= z and x ̸∈ fv(E)(∗)
{E/z} (E1 E2) def= ({E/z}E1) ({E/z}E2)
. . .
if (∗) is false, apply alpha conversion to generate a variant of (fn x : T ⇒ E1) to
make (∗) true
118
Substitution – Example
Substitution – Example Again
{y + 2/x} (fn y : int ⇒ x + y)
= {y + 2/x} (fn z : int ⇒ x + z)
= (fn z : int ⇒ {y + 2/x} (x + z))
= (fn z : int ⇒ {y + 2/x}x + {y + 2/x} z)
= (fn z : int ⇒ (y + 2) + z)
119
Simultaneous Substitution
• a substitution σ is a finite partial function from variables to
expressions
• notation: {E1/x1, . . . , Ek/xk} instead of {x1 7→ E1, . . . , xk 7→ Ek}
• the formal definition is straight forward
120
Definition Substitution [for completeness]
Let σ be {E1/x1, . . . , Ek/xk}.
Moreover, dom(σ) = {x1, . . . , xk} and ran(σ) = {E1, . . . , Ek}.
σ x =
{
Ei if x = xi (and xi ∈ dom(σ)
x otherwise
σ (fn x : T ⇒ E) = (fn x : T ⇒ (σ E)) if x ̸∈ dom(σ) and x ̸∈ fv(ran(σ)) (∗)
σ (E1 E2) = (σ E1) (σ E2)
σ n = n
σ (E1 op E2) = (σ E1) op (σ E2)
σ (if E1 then E2 else E3) = if (σ E1) then (σ E2) else (σ E3)
σ b = b
σ skip = skip
σ (l := E) = l := (σ E)
σ ( !l) = !l
σ (E1 ; E2) = (σ E1) ; (σ E2)
σ (while E1 do E2) = while (σ E1) do (σ E2)
121
Function Behaviour
• we are now ready to define the semantics of functions
• there are some choices to be made
▶ call-by-value
▶ call-by-name
▶ call-by-need
122
Function Behaviour
Consider the expression
E = (fn x : unit ⇒ (l := 1) ; x) (l := 2)
What is the transition relation
⟨E , {l 7→ 0}⟩ −→∗ ⟨skip , {l 7→ ???}⟩
123
Choice 1: Call-by-Value
Idea: reduce left-hand-side of application to an fn-term;
then reduce argument to a value;
then replace all occurrences of the formal parameter in the fn-term by
that value.
E = (fn x : unit ⇒ (l := 1) ; x) (l := 2)
⟨E , {l 7→ 0}⟩
−→ ⟨(fn x : unit ⇒ (l := 1) ; x) skip , {l 7→ 2}⟩
−→ ⟨(l := 1) ; skip , {l 7→ 2}⟩
−→ ⟨skip ; skip , {l 7→ 1}⟩
−→ ⟨skip , {l 7→ 1}⟩
124
Call-by-Value – Semantics
Values
v ::= b | n | skip | (fn x : T ⇒ E)
SOS rules
all sos rules we used so far, plus the following
(app1)
⟨E1 , s⟩ −→ ⟨E′1 , s′⟩
⟨E1 E2 , s⟩ −→ ⟨E′1 E2 , s′⟩
(app2)
⟨E2 , s⟩ −→ ⟨E′2 , s′⟩
⟨v E2 , s⟩ −→ ⟨v E′2 , s′⟩
(fn) ⟨(fn x : T ⇒ E) v , s⟩ −→ ⟨{v/x}E , s⟩
125
Call-by-Value – Example I
⟨(fn x : int ⇒ (fn y : int ⇒ x + y)) (3 + 4) 5 , s⟩
= ⟨((fn x : int ⇒ (fn y : int ⇒ x + y)) (3 + 4)) 5 , s⟩
−→ ⟨((fn x : int ⇒ (fn y : int ⇒ x+ y)) 7) 5 , s⟩
−→ ⟨({7/x} (fn y : int ⇒ x+ y)) 5 , s⟩
= ⟨(fn y : int ⇒ 7 + y) 5 , s⟩
−→ ⟨{5/y} 7 + y , s⟩
= ⟨7 + 5 , s⟩
−→ ⟨12 , s⟩
126
Call-by-Value – Example II
(fn f : int → int ⇒ f 3) (fn x : int ⇒ (1 + 2) + x) −→∗ ???
127
Choice 2: Call-by-Name
Idea: reduce left-hand-side of application to an fn-term;
then replace all occurrences of the formal parameter in the fn-term by
that argument.
E = (fn x : unit ⇒ (l := 1) ; x) (l := 2)
⟨E , {l 7→ 0}⟩
−→ ⟨(l := 1) ; (l := 2) , {l 7→ 0}⟩
−→ ⟨skip ; (l := 2) , {l 7→ 1}⟩
−→ ⟨l := 2 , {l 7→ 1}⟩
−→ ⟨skip , {l 7→ 2}⟩
128
Call-by-Name – Semantics
SOS rules
(CBN-app)
⟨E1 , s⟩ −→ ⟨E′1 , s′⟩
⟨E1 E2 , s⟩ −→ ⟨E′1 E2 , s′⟩
(CBN-fn) ⟨(fn x : T ⇒ E1) E2 , s⟩ −→ ⟨{E2/x}E1 , s⟩
No evaluation unless needed
⟨(fn x : unit ⇒ skip) (l := 2) , {l 7→ 0}⟩
−→ ⟨{l := 2/x}skip , {l 7→ 0}⟩
= ⟨skip , {l 7→ 0}⟩
but if it is needed, repeated evaluation possible.
129
Choice 3: Full Beta
Idea: allow reductions on left-hand-side and right-hand-side;
any time if left-hand-side is an fn-term;
replace all occurrences of the formal parameter in the fn-term by that
argument; allow reductions inside functions
⟨(fn x : int ⇒ 2 + 2) , s⟩ −→ ⟨(fn x : int ⇒ 4) , s⟩
130
Full Beta – Semantics
Values
v ::= b | n | skip | (fn x : T ⇒ E)
SOS rules
(beta-app1)
⟨E1 , s⟩ −→ ⟨E′1 , s′⟩
⟨E1 E2 , s⟩ −→ ⟨E′1 E2 , s′⟩
(beta-app2)
⟨E2 , s⟩ −→ ⟨E′2 , s′⟩
⟨E1 E2 , s⟩ −→ ⟨E1 E′2 , s′⟩
(beta-fn1) ⟨(fn x : T ⇒ E1) E2 , s⟩ −→ ⟨{E2/x}E1 , s⟩
(beta-fn2)
⟨E , s⟩ −→ ⟨E′ , s′⟩
⟨(fn x : T ⇒ E) , s⟩ −→ ⟨(fn x : T ⇒ E′) , s′⟩
131
Full Beta – Example
(fn x : int ⇒ x + x) (2 + 2)
(fn x : int ⇒ x + x) 4 (2 + 2) + (2 + 2)
4 + (2 + 2)
4 + 4
8
(2 + 2) + 4
132
Choice 4: Normal-Order Reduction
Idea: leftmost, outermost variant of full beta.
133
Section 6
Typing for Call-By-Value
134
Typing Functions - TypeEnvironment
• so far Γ ranges over TypeEnv, the finite partial function from
L⇀ Tloc
• with functions, it summarises assumptions on the types of variables
• type environments Γ are now pairs of a Γloc (L⇀ Tloc)
and a Γvar, a partial function from X to T (X⇀ T ).
For example, Γloc = {l1 : intref} and Γvar = {x : int, y : bool → int}.
• dom(Γ) = dom(Γloc) ∪ dom(Γvar).
• notation: if x ̸∈ dom(Γvar), we write Γ, x : T , which adds x : T to
Γvar
135
Typing Functions
(var) Γ ⊢ x :T if Γ(x) = T
(fn)
Γ, x : T ⊢ E :T ′
Γ ⊢ (fn x : T ⇒ E) :T → T ′
(app)
Γ ⊢ E1 :T → T ′ Γ ⊢ E2 :T
Γ ⊢ E1 E2 :T ′
136
Typing Functions – Example I
(FN)
(OP+)
(VAR)
x : int ⊢ x : int x : int ⊢ 2 : int (INT)
x : int ⊢ x + 2 : int
{} ⊢ (fn x : int ⇒ x + 2) : int → int {} ⊢ 2 : int (INT)
{} ⊢ (fn x : int ⇒ x + 2) 2 : int (APP)
137
Typing Functions – Example II
Determine the type of
(fn x : int → int ⇒ x (fn x : int ⇒ x) 3)
138
Properties Typing
We only consider closed programs, with no free variables.
Theorem (Progress)
If E closed, Γ ⊢ E :T and dom(Γ) ⊆ dom(s) then either E is a value or
there exist E′ and s′ such that ⟨E , s⟩ −→ ⟨E′ , s′⟩.
There are more configurations that get stuck, e.g. (3 4).
Theorem (Type Preservation)
If E closed, Γ ⊢ E :T , dom(Γ) ⊆ dom(s) and ⟨E , s⟩ −→ ⟨E′ , s′⟩ then
Γ ⊢ E′ :T and dom(Γ) ⊆ dom(s′).
139
Proving Type Preservation
Theorem (Type Preservation)
If E closed, Γ ⊢ E :T , dom(Γ) ⊆ dom(s) and ⟨E , s⟩ −→ ⟨E′ , s′⟩ then
Γ ⊢ E′ :T and dom(Γ) ⊆ dom(s′).
Proof outline.
Choose
Φ(E, s,E′, s′) = ∀Γ, T. (Γ ⊢ E :T ∧ closed(E) ∧ dom(Γ) ⊆ dom(s)
=⇒ Γ ⊢ E′ :T ∧ closed(E′) ∧ dom(Γ) ⊆ dom(s′))
show ∀E, s,E′, s′. ⟨E , s⟩ −→ ⟨E′ , s′⟩ =⇒ Φ(E, s,E′, s′), by rule
induction
140
Proving Type Preservation – Auxiliary Lemma
Lemma (Substitution)
If E closed, Γ ⊢ E :T and Γ, x : T ⊢ E′ :T ′ with x ̸∈ dom(Γ) then
Γ ⊢ {E/x}E′ :T ′.
141
Type Safety
Main result: Well-typed programs do not get stuck.
Theorem (Type Safety)
If Γ ⊢ E :T , dom(Γ) ⊆ dom(s), and ⟨E , s⟩ −→∗ ⟨E′ , s′⟩ then either E′ is
a value with Γ ⊢ E′ :T , or there exist E′′, s′′ such that
⟨E′ , s′⟩ −→ ⟨E′′ , s′′⟩, Γ ⊢ E′′ :T and dom(Γ) ⊆ dom(s′′).
Here, −→∗ means arbitrary many steps in the transition system.
142
Normalisation
Theorem (Normalisation)
In the sublanguage without while loops, if Γ ⊢ E :T and E closed then
there does not exist an infinite reduction sequence
⟨E , {}⟩ −→ ⟨E1 , {}⟩ −→ ⟨E2 , {}⟩ −→ . . .
Proof.
See B. Pierce, Types and Programming Languages, Chapter 12.
143
Section 7
Recursion
144
Scoping
Name Definitions
restrict the scope of variables
E ::= . . . | let val x : T = E1 in E2 end
• x is a binder for E2
• can be seen as syntactic sugar:
let val x : T = E1 in E2 end ≡ (fn x : T ⇒ E2) E1
145
Derived sos-rules and typing
let val x : T = E1 in E2 end ≡ (fn x : T ⇒ E2) E1
(let)
Γ ⊢ E1 :T Γ, x : T ⊢ E2 :T ′
Γ ⊢ let val x : T = E1 in E2 end :T ′
(let1)
⟨E1 , s⟩ −→ ⟨E′1 , s′⟩
⟨let val x :T = E1 in E2 end , s⟩ −→ ⟨let val x :T = E′1 in E2 end , s′⟩
(let2) ⟨let val x : T = v in E2 end , s⟩ −→ ⟨{v/x}E2 , s⟩
146
Recursion – An Attempt
Consider
r = (fn y : int ⇒ if y ≥ 1 then y + (r(y + −1)) else 0)
where r is the recursive call (variable occurring in itself).
What is the evaluation of r 3?
We could try
E ::= . . . | let val rec x : T = E in E′ end
where x is a binder for both E and E′.
let val rec r : int → int =
(fn y : int ⇒ if y ≥ 1 then y + (r(y + −1)) else 0)
in r 3 end
147
However . . .
• What about let val rec x : T = (x, x) in x end?
• What about let val rec x : int list = 3 :: x in x end?
Does this terminate? and if it does is it equal to
– let val rec x : int list = 3 :: 3 :: x in x end
• Does let val rec x : int list = 3 :: (x+ 1) in x end terminate?
• In Call-by-Name (Call-by-Need) these are reasonable
• In Call-by-Value these would usually be disallowed
148
Recursive Functions
Idea specialise the previous let val rec
• T = T1 → T2 (recursion only at function types)
• E = (fn y : T1 ⇒ E1) (and only for function values)
149
Recursive Functions – Syntax and Typing
E ::= . . . | let val rec x : T1 → T2 = (fn y : T1 ⇒ E1) in E2 end
Here, y binds in E1 and x bind in (fn y : T1 ⇒ E1) and E2
(recT)
Γ, x:T1→T2, y:T1 ⊢ E1 :T2 Γ, x:T1→T2 ⊢ E2 :T
Γ ⊢ let val rec x : T1 → T2 = (fn y : T1 ⇒ E1) in E2 end :T
150
Recursive Functions – Semantics
(rec) ⟨let val rec x:T1→T2=(fn y:T1⇒E1) in E2 end , s⟩
−→
⟨{(fn y:T1⇒ let val rec x:T1→T2=(fn y:T1⇒E1) in E1 end)/x}E2 , s⟩
151
Redundancies?
• Do we need E1 ; E2?
No: E1 ; E2 ≡ (fn y : unit ⇒ E2) E1
• Do we need while E1 do E2?
No:
while E1 do E2 ≡ let val rec w : unit → unit =
(fn y : unit ⇒ if E1 then (E2; (w skip)) else skip)
in
w skip
end
152
Redundancies?
• Do we need recursion?
Yes! Previously, normalisation theorem effectively showed that
while adds expressive power; now, recursion is even more powerful.
153
Side remarks I
• naive implementations (in particular substitutions) are inefficient
(more efficient implementations are shown in courses on compiler
construction)
• more concrete – closer to implementation or machine code – are
possible
• usually refinement to prove compiler to be correct
(e.g. CompCert or CakeML)
154
Side remarks I – CakeML
155
Side remarks II: Big-step Semantics
• we have seen a small-step semantics
⟨E , s⟩ −→ ⟨E′ , s′⟩
• alternatively, we could have looked at a big-step semantics
⟨E , s⟩ ⇓ ⟨E′ , s′⟩
For example
⟨n , s⟩ ⇓ ⟨n , s⟩
⟨E1 , s⟩ ⇓ ⟨n1 , s′⟩ ⟨E2 , s′⟩ ⇓ ⟨n2 , s′′⟩
⟨E1 + E2 , s⟩ ⇓ ⟨n , s′′⟩ (n = n1+n2)
• no major difference for sequential programs
• small-step much better for modelling concurrency and proving type
safety
156
Section 8
Data
157
Recap and Missing Steps
• simple while language
• with functions
• but no data structures
158
Products – Syntax
T ::= . . . | T ∗ T
E ::= . . . | (E,E) | fst E | snd E
159
Products – Typing
(pair)
Γ ⊢ E1 :T1 Γ ⊢ E2 :T2
Γ ⊢ (E1, E2) :T1 ∗ T2
(proj1)
Γ ⊢ E :T1 ∗ T2
Γ ⊢ fst E :T1
(proj2)
Γ ⊢ E :T1 ∗ T2
Γ ⊢ snd E :T2
160
Products – Semantics
Values
v ::= . . . | (v, v)
SOS rules
(pair1)
⟨E1 , s⟩ −→ ⟨E′1 , s′⟩
⟨(E1, E2) , s⟩ −→ ⟨(E′1, E2) , s′⟩
(pair2)
⟨E2 , s⟩ −→ ⟨E′2 , s′⟩
⟨(v,E2) , s⟩ −→ ⟨(v,E′2) , s′⟩
(proj1) ⟨fst (v1, v2) , s⟩ −→ ⟨v1 , s⟩ (proj2) ⟨snd (v1, v2) , s⟩ −→ ⟨v2 , s⟩
(proj3)
⟨E , s⟩ −→ ⟨E′ , s′⟩
⟨fst E , s⟩ −→ ⟨fst E′ , s′⟩ (proj4)
⟨E , s⟩ −→ ⟨E′ , s′⟩
⟨snd E , s⟩ −→ ⟨snd E′ , s′⟩
161
Sums (Variants, Tagged Unions) – Syntax
T ::= . . . | T + T
E ::= . . . | inl E :T | inr E :T |
case E of inl x1 :T1 ⇒ E | inr x2 :T2 ⇒ E
x1 and x2 are binders for E1 and E2, up to alpha-equivalence
162
Sums – Typing I
(inl)
Γ ⊢ E :T1
Γ ⊢ inl E : T1 + T2 :T1 + T2
(inr)
Γ ⊢ E :T2
Γ ⊢ inr E : T1 + T2 :T1 + T2
(case)
Γ ⊢ E :T1 + T2 Γ, x :T1 ⊢ E1 :T Γ, y :T2 ⊢ E2 :T
Γ ⊢ case E of inl x :T1 ⇒ E1 | inr y :T2 ⇒ E2 :T
163
Sums – Typing II
case E of inl x :T1 ⇒ E1 | inr y :T2 ⇒ E2
Why do we need to carry around type annotations?
• maintain the unique typing property
Otherwise inl 3 : could be of type int + int or int + bool
• many programming languages allow type polymorphism
164
Sums – Semantics
Values
v ::= . . . | inl v :T | inr v :T
SOS rules
(inl)
⟨E , s⟩ −→ ⟨E′ , s′⟩
⟨inl E :T , s⟩ −→ ⟨inl E′ :T , s′⟩ (inr)
⟨E , s⟩ −→ ⟨E′ , s′⟩
⟨inr E :T , s⟩ −→ ⟨inr E′ :T , s′⟩
(case1)
⟨E , s⟩ −→ ⟨E′ , s′⟩
⟨case E of inl x :T1 ⇒ E1 | inr y :T2 ⇒ E2 , s⟩
−→ ⟨case E′ of inl x :T1 ⇒ E1 | inr y :T2 ⇒ E2 , s′⟩
(case2) ⟨case inl v :T of inl x :T1 ⇒ E1 | inr y :T2 ⇒ E2 , s⟩
−→ ⟨{v/x}E1 , s⟩
(case3) ⟨case inr v :T of inl x :T1 ⇒ E1 | inr y :T2 ⇒ E2 , s⟩
−→ ⟨{v/y}E2 , s⟩
165
Constructors and Destructors
type constructors destructors
T → T (fn x : T ⇒ ) E
T ∗ T ( , ) fst snd
T + T inl :T inr :T case
bool true false if then else
166
Proofs as Programs
The Curry-Howard correspondence
(var) Γ, x :T ⊢ x :T Γ, P ⊢ P
(fn)
Γ, x :T ⊢ E :T ′
Γ ⊢ (fn x : T ⇒ E) :T → T ′
Γ, P ⊢ P ′
Γ ⊢ P → P ′
(app)
Γ ⊢ E1 :T → T ′ Γ ⊢ E2 :T
Γ ⊢ E1 E2 :T ′
Γ ⊢ P → P ′ Γ ⊢ P
Γ ⊢ P ′ (modus ponens)
. . .
167
Proofs as Programs: The Curry-Howard
correspondence
(var) Γ, x:T ⊢ x :T Γ, P ⊢ P
(fn)
Γ, x:T ⊢ E :T ′
Γ ⊢ (fn x : T ⇒ E) :T → T ′
Γ, P ⊢ P ′
Γ ⊢ P → P ′
(app)
Γ ⊢ E1 :T → T ′ Γ ⊢ E2 :T
Γ ⊢ E1 E2 :T ′
Γ ⊢ P → P ′ Γ ⊢ P
Γ ⊢ P ′ (modus ponens)
(pair)
Γ ⊢ E1 :T1 Γ ⊢ E2 :T2
Γ ⊢ (E1, E2) :T1 ∗ T2
Γ ⊢ P1 Γ ⊢ P2
Γ ⊢ P1 ∧ P2
(proj1)
Γ ⊢ E :T1 ∗ T2
Γ ⊢ fst E :T1 (proj2)
Γ ⊢ E :T1 ∗ T2
Γ ⊢ snd E :T2
Γ ⊢ P1 ∧ P2
Γ ⊢ P1
Γ ⊢ P1 ∧ P2
Γ ⊢ P2
(inl)
Γ ⊢ E :T1
Γ ⊢ inl E :T1 + T2 :T1 + T2 (inr)
Γ ⊢ E :T2
Γ ⊢ inr E :T1 + T2 :T1 + T2
Γ ⊢ P1
Γ ⊢ P1 ∨ P2
Γ ⊢ P2
Γ ⊢ P1 ∨ P2
(case)
Γ ⊢ E :T1 + T2 Γ, x : T1 ⊢ E1 :T Γ, y : T2 ⊢ E2 :T
Γ ⊢ case E of inl x :T1 ⇒ E1 | inr y :T2 ⇒ E2 :T
Γ ⊢ P1 ∨ P2 Γ, P1 ⊢ P Γ, P2 ⊢ P
Γ ⊢ P
(unit), (zero), . . . ; but not (letrec)
168
Curry-Howard correspondence (abstract)
Programming side Logic side
bottom type false formula
unit type true formula
sum type disjunction
product type conjunction
function type implication
generalised sum type (Σ type) existential quantification
generalised product type (Π type) universal quantification
169
Datatypes in Haskell
Datatypes in Haskell generalise both sums and products
data Pa i r = P I n t Double
data E i t h e r = I I n t | D Double
The expression
data Expr = I n t V a l I n t
| BoolVal Bool
| Pai rVa l I n t Bool
is (roughly) like saying
Expr = int + bool + (int ∗ bool)
170
More Datatypes - Records
A generalisation of products.
Labels lab ∈ LAB for a set LAB = {p, q, ...}
T ::= . . . | {lab1 : T1, . . . , labk : Tk}
E ::= . . . | {lab1 = E1, . . . , labk = Ek} | #lab E
(where in each record (type or expression) no lab occurs more than
once)
171
Records – Typing
(record)
Γ ⊢ E1 :T1 . . . Γ ⊢ Ek :Tk
Γ ⊢ {lab1 = E1, . . . , labk = Ek} :{lab1 : T1, . . . , labk : Tk}
(recordproj)
Γ ⊢ E :{lab1 : T1, . . . , labk : Tk}
Γ ⊢ #labi E :Ti
172
Records – Semantics
Values
v ::= . . . | {lab1 = v1, . . . , labk = vk}
SOS rules
(record1)
⟨Ei , s⟩ −→ ⟨E′i , s′⟩
⟨{lab1 = v1, . . . , labi−1 = vi−1, labi = Ei, . . . , labk = Ek} , s⟩
−→ ⟨{lab1 = v1, . . . , labi−1 = vi−1, labi = E′i, . . . , labk = Ek} , s′⟩
(record2) ⟨#labi {lab1 = v1, . . . , labk = vk} , s⟩ −→ ⟨vi , s⟩
(record3)
⟨E , s⟩ −→ ⟨E′ , s′⟩
⟨#labi E , s⟩ −→ ⟨#labi E′ , s′⟩
173
Mutable Store I
Most languages have some kind of mutable store.
Two main choices:
1. our approach
E ::= . . . | l := E | !l | x
▶ locations store mutable values
▶ variables refer to a previously calculated value – immutable
▶ explicit dereferencing and assignment
(fn x : int ⇒ l := (!l) + x)
174
Mutable Store II
Most languages have some kind of mutable store.
Two main choices:
2. languages as C or Java
▶ variables can refer to a previously calculated value
and overwrite that value
▶ implicit dereferencing
▶ some limited type machinery to limit mutability
vo id foo ( x : i n t ) {
l = l + x
. . .
}
175
References
T ::= . . . | T ref
Tloc ::= intref T ref
E ::= · · · | ll := E | !l
| E1 := E2 | !E | ref E | l
176
References – Typing
(ref)
Γ ⊢ E :T
Γ ⊢ ref E :T ref
(assign)
Γ ⊢ E1 :T ref Γ ⊢ E2 :T
Γ ⊢ E1 := E2 :unit
(deref)
Γ ⊢ E :T ref
Γ ⊢ !E :T
(loc)
Γ(l) = T ref
Γ ⊢ l :T ref
177
References – Semantics I
Values
A location is a value v ::= . . . | l
Stores s were finite partial functions L⇀ Z.
We now take them to be finite partial functions from L to all values.
SOS rules
(ref1) ⟨ref v , s⟩ −→ ⟨l , s+ {l 7→ v}⟩ if l ̸∈ dom(s)
(ref2)
⟨E , s⟩ −→ ⟨E′ , s′⟩
⟨ref E , s⟩ −→ ⟨ref E′ , s′⟩
178
References – Semantics II
(deref1) ⟨!l , s⟩ −→ ⟨v , s⟩ if l ∈ dom(s) and s(l) = v
(deref2)
⟨E , s⟩ −→ ⟨E′ , s′⟩
⟨!E , s⟩ −→ ⟨!E′ , s′⟩
(assign1) ⟨l := v , s⟩ −→ ⟨skip , s+ {l 7→ v}⟩ if l ∈ dom(s)
(assign2)
⟨E , s⟩ −→ ⟨E′ , s′⟩
⟨l := E , s⟩ −→ ⟨l := E′ , s′⟩
(assign3)
⟨E , s⟩ −→ ⟨E′ , s′⟩
⟨E := E2 , s⟩ −→ ⟨E′ := E2 , s′⟩
179
Type Checking the Store
• so far we used dom(Γ) ⊆ dom(s) in theorems such as progress and
type preservation
• expressed ‘all locations in Γ exist in store s ’
• we need more
• for each l ∈ dom(s) we require that s(l) is typable
• moreover, s(l) might contain some other locations . . .
180
Type Checking – Example
Example
E = let val x : (int → int) ref = ref (fn z : int ⇒ z) in
(x := (fn z : int ⇒ if z ≥ 1 then z + ((!x) (z +−1)) else 0);
(!x) 3) end
which has reductions
⟨E , {}⟩
−→∗ ⟨E1 , {l1 7→ (fn z : int ⇒ z)⟩
−→∗ ⟨E2 , {l1 7→ (fn z : int ⇒ if z ≥ 1 then z + ((!l1)(z +−1)) else 0)}⟩
−→∗ ⟨6 , . . . ⟩
181
Progress and Type Preservation
Definition (Well-type store)
Let Γ ⊢ s if dom(Γ) = dom(s) and if
∀l ∈ dom(s). Γ(l) = T ref =⇒ Γ ⊢ s(l) :T .
Theorem (Progress)
If E closed, Γ ⊢ E :T and Γ ⊢ s then either E is a value or there exist E′
and s′ such that ⟨E , s⟩ −→ ⟨E′ , s′⟩.
Theorem (Type Preservation)
If E closed, Γ ⊢ E :T , Γ ⊢ s and ⟨E , s⟩ −→ ⟨E′ , s′⟩ then E′ is closed
and for some Γ′ (with disjoint domain to Γ) Γ,Γ′ ⊢ E′ :T and Γ,Γ′ ⊢ s′.
182
Type Safety
Theorem (Type Safety)
If E closed, Γ ⊢ E :T , Γ ⊢ s, and ⟨E , s⟩ −→∗ ⟨E′ , s′⟩ then either E′ is a
value with Γ ⊢ E′ :T , or there exist E′′, s′′ such that
⟨E′ , s′⟩ −→ ⟨E′′ , s′′⟩, and there exists a Γ′ s.t. Γ,Γ′ ⊢ E′′ :T and
Γ,Γ′ ⊢ s′′.
183