Re

τ := bool
   | τ₁ → τ₂

---

V⟦τ⟧: Values of type τ which don't get stuck

V⟦bool⟧ = {true, false}
V⟦τ₁ → τ₂⟧ =
  {λx:τ₁. e
   | ∀v ∈ V[τ₁],
     e[v/x] ∈ E[τ₂]}

---

E⟦τ⟧: Expressions which will end up being of type τ

E⟦τ⟧ =
  {e | ∀e',
       e ↦* e' ∧ irred(e') ∧ e' ∈ V[τ]}

---

G: Substitution for assignments
G⟦⋅⟧ = {∅}

Γ

γ

D1

STLC

• no recursive functions
• no recursive types

Logical relations

• Very general
• Eg:
  • Termination of STLC (unary)
  • type safety/soundness (unary)
  • Program equivalence (a relational, binary property. Not unary property which is a property about a single program)
    • That two given programs do the same thing
    • Binary logical relations: Programs in even two different languages. As in source to target language. Low-high level equiv.
    • Useful to prove compiler correctness
  • Representation independence.
    • Data structure itself doesn't matter for correctness. Only interface does.
    • Existential type. Interfaces are like that??
  • Parametricity.
    • Polymorphism

Observational equiv. Output program of the compiler is related to the input program.

• Unary logical relations
• Useful to verify FFIs

–

STLC that we consider:

• only bools

τ := bool | τ1 → τ2
e := x
   | true | false
   | if e then e1 else e2
   | λx:τ. e
   | e1 e2
v := true | false
   | λx:τ. e

Remark: λ comes in e and v. e is specified, then we say what are the vals. and λ is a val. Choice of values are important when designing lang. Eg: (e1, e2) itself could be considered val. But we could also have said only (v1,v2) can be a value.

Value lambda is an e suspended computations. Cannot be run till applied.

Operational semantics (call-by-value, left-to-right evaluation):

Evaluation context.

• Which one to evaluate next
• Allows for unique parsing
• Tells where to go next

E := [⋅]
   | if E then e1 else e2
   | E e2      (Evaluate left first)
   | v1 E      (Evaluate right only after left)

Reduction rules:

• The real deal

# e ↦ e'

if true then e1 else e2 ↦ e1

if false then e1 else e2 ↦ e2

(λx:τ. e) v  ↦  e[v/x]

  e ↦ e'
────────────
E[e] ↦ E[e']

Context Γ:

• Unordered list which associates each variable with a type

Γ := ⋅         (empty)
   | Γ, x:τ    (cons)

Shape of typing judgement ??

# Γ ⊢ e: τ

Γ(x) = τ
─────────
 Γ ⊢ x:τ


──────────────    ───────────────
Γ ⊢ true: bool    Γ ⊢ false: bool



   Γ, x:τ1 ⊢ e:τ2          Γ ⊢ e1:τ1→τ2    Γ ⊢ e2:τ1    
─────────────────────      ─────────────────────────        
Γ ⊢ (λx:τ1. e): τ1→τ2          Γ ⊢ (e1 e2): τ2              



 Γ ⊢ e:bool   Γ ⊢ e1:τ    Γ ⊢ e2:τ
───────────────────────────────────
   Γ ⊢ (if e then e1 else e2): τ

–

Features defining a language:

• Syntax
• Static semantics
  • aka Typing rules
  • How to assign types to terms
• Dynamic semantics
  • How to run the program
  • In our case, operational semantics

How to prove type soundness.

Type soundness

• not just progress and preservation. That's just a technique to show type soundness. Not type soundness itself.
• Well typed programs don't go wrong - Milner
  • If we can type check a program, ie, build a typing derivation for it, it is a well-typed program. Type safety.
  • Going wrong: Getting stuck without arriving at a value
    • Not a value, but still cannot go another step => not well typed

Milner's slogan.

Type soundness: (à la Milner's slogan):

∀e', e ↦* e' then either
 val(e') or       (ie, already a value)
 ∃e'', e' ↦ e''   (ie, one more step possible)

What if e'' is a stuck term? That scenario is ruled out because the base condition says it should end up being a value.

• Progress: If you have a well-typed program, then it is either a value or it is possible to take another step
  • if ⊢ e:τ, then val(e) or ∃e', e ↦ e'
• Preservation: Type is preserved. Same term always has the same type
  • if ⊢ e:τ and e ↦ e', then e': τ

DBT: For subtypes the above two need to be generalized.

For the type soundness proof, we can ping-pong between these two lemmas.

• If it's a value, it is well typed (Progress)
• If it's not a value, it can take a step (Progress)
• If it takes a step, its type is preserved (Preservation)

This is a syntactic way of proving type soundness.

Progress and preservation is just one technique, although the most popular one, to prove type soundness.

This lecture series will show how to prove type soundness semantically. Using logical relations.

—

DBT: From 80s till mid 2000s everyone used progress and preservation for type soundness proofs. What happened then?

In the 1980s, people used to prove type soundness using denotational semantics.

1990s, Andrew Wright and Matthias Felleisen[1]. Beginning of a proof method to prove soundness without using denotational semantics.

Denosem => give a mathematical interpreation to program and make sure everything is consistent.

80s: deno sem. math interp to progs 94: Andrew wright.

• Progress lemma: Either val or can take a step

  ⊢e:τ, then eigher val(e) or ∃e', e↦e'

• Preservation lemma: take a step and type doesn't change

  ⊢e:τ and ⊢e ↦ e', then ⊢e':τ

This is synatically proving type correctenss. This lecture series about proving this semantically. Using logrels.

—

Logical relations

Setting up relations that let us prove some property of interest.

We will be looking at type soundness of STLC. That means showing absence of stuck terms.

Pₜ(e)

• P: Property of interest
• e: term
• t: type

Set of programs indexed by the different types of the language.

STLC that we consider => types are just bool and functions. Unary relations. More types => more relations

For binary relations, it would be like: Rₜ(e1, e2)

–

Unary relation:

• A collection/family of elements having some property
• Eg: Set of left-handed people

Binary relation:

• Eg: equality

—

Our type soundness theorem for STLC:

⋅⊢e: τ then safe(e)

ie, if e has a type τ, then e is type safe

where safe is defined as

safe(e) ≝ ∀e', if e↦*e' then val(e') or ∃e'', e'↦e''

—

Now to define the relations.

We could define relations on expressions. But let's try a more common style.

DBT: Why is the other style more common?

2 parts:

• Relation on values saying when they belong to the relation. ie, when are values safe.
  • Values are closed values.
• Then, we say when are expressions safe.
  • Expression can have free variables. ie, an environment need to be considered.

— Value relation: What are all the sets of values v such that v behaves like something of type τ and doesn't get stuck.

V⟦τ⟧: set of all values which can be of type τ and don't get stuck
 = {v | .. }

V⟦bool⟧ = {true, false}

V⟦τ1→τ2⟧ = {λx.τ1. e | ... }
  ∀v ∈ V⟦τ1⟧
  e[v/x] ∈ E⟦τ2⟧

This has to behave like a τ1→τ2 even when we put it in a different program. So just checking if it's a value isn't enough.

Amal gave this example: λx:bool. x true

Also, λ is already a value. Could've stopped here, but that would mean getting stuck.

Logical relations give a stronger induction principle.

We got to eliminate stuff like true false which isn't even a proper function application??.

irreducible: cannot take another redn.

• either stuck or a value

Note that V⟦τ1→τ2⟧ doesn't ask for a typing derivation. It only asks whether it behaves as expected.

—

Expression type

E[τ] is a relation indicating the family of expressions which behave like a τ.

E[τ] = {e | ∀e', e ↦* e' ∧ irred(e') ∧ e' ∈ V⟦τ⟧}

where

irred(e) ≝ ∄e', e ↦* e'

irred(e) means e cannot take another step. Which means it's either stuck or is a value.

Question: what if e diverges?

• For STLC, it's okay. Because every well typed term terminates.
  • Once we add recursive types, I guess some modifications are due.
• STLC cannot type check the Ω combinator.

Omega combinator: The famous divergent term

• Ω = (λx. x x)(λx. x x)

Question: Example of a term which is not syntactically well-typed but still belongs to the relation?

• Consider rust code marked unsafe.
  • Programmer say, I know what I'm doing. A too rich type system would only annoy the programmer.
• Syntactically not possible, but can be safe.
• Safe at boundaries, but internally not sound as per type checker
• Standard library uses unsafe code too.

Semantic type sounndess using logrel stuff method doesn't need the program to finish running. Doesn't need a complete derivation tree ??

Can't limit ourselves to proofs about closed terms. We need open progs as well ∵ of the λ typing rule

Semantics type soundness theorem: ⋅⊢ e:τ then safe(e)

⊢ : syntactically well-typed ⊨ : semantically well-typed

For open progs, G = Substitution for assignments

G[⋅] = {∅} G[Γ,x:τ] = { γ[x↦v] | γ ∈ G[Γ] ∧ v ∈ V[τ]}

γ is value assignments to variables. Eg: γ = {x1↦v1, x2↦v2, …}

Γ ⊨ e:τ =def ∀γ∈G[Γ], γ(e) ∈ E[τ]

Logrel: If you give me input of desired relation, I'll give you output of desired relation

Fundamental property of logical relations

• aka basic lemma

Adequacy of a logrel

—

A) ⋅↦e:τ => ⋅ ⊨ e:τ A) ⋅↦e:τ => e ∈ E[τ]

B) ⋅⊨

B should be trivial if the logrel was built properly

Case 1: ¬irred(e)

Then

—

FP Γ⊢e:τ => Γ⊨e:τ

Induction of typing derivation.

Case: Γ⊢true:bool To prove: Γ⊨true:bool

Suppose γ∈G[Γ]

TAPL: Logical realtions section in Normalization

D2

• V: Value
• E: Expression
• G: Ctxt instance ??
• γ: plug in some value ??
• Γ: ctxt

• FP: Fundamental property
  • If a term is syntactically well-typed then it is semantically well-typed

behaviour: what happens when we run it? compositionality building blocks

Granularity of type ??

Add new types -> we will have new typing rules (intro, elim), then got to show that those rules are sound too.

logrel comes into play after a type system is already there.

FP:

Γ,x:τ implicitly means x ∈¬ Γ (TAPL)

HW: Application case (lambda was done in class)

The lang as it is now is terminating.

• not Turing complete

Let's allow non-terminating progs => Add recursive types

unit type useful for stuff like repring nil of lists and leaf of tree

type tree = Leaf
          | Node of int * tree * tree

tree = 1 + (int * tree * tree)

type itself shows up in definition

many possible 'views' (ie, unrollings??)

Fixpoint: x is fixpoint of f if x = f(x)

F := λα:type. 1 + (int * α * α)

We need a fixpoint builder. General.

<skip>

fold and unfold of a recursive type.

Examples of recursive types:

tree = μα. 1 + (int * α * α)
intlist = μα. 1 + (int * α)

where α is the type argument.

τ := bool 
   | τ → τ
   | 1
   | α
   | μα. τ

View shifters.

• fold e
• unfold e

Let's try to type check the Ω-combinator.

Ω = (λx. x x) (λx. x x)

Without rectypes, x could be τ1 → τ2 or τ.

self application part (x x): (unfold x) x rectype in neg pos!

We have type rules. Now need eval rules??

V := fold V
   | ...
   | ...

E := fold E
   | ...

Redex rule:

unfold (fold v) = v

V[μα. τ] = {fold v | }

smeantic breacket eval arrow big 1 , 0

Andrew Pitts ATAPL last exercise

• used to be an open problem. Not any more ??

mutable refs: still unsovled ??

• ∵ of cycles in heap

Step-indexing Logrel indexed by a natural number

Now induction is done on step count instead of the structure of type.

gas is similar concept but for synactic-oriented stuff

—

Vₖ

Each redn step of the opsem = 1 step Kinda like possible worlds model. monotonicity

D3

Step indexing paper (proof carrying code): 2001 TOPLAS Appel + McCallester 2004: Ahmed PhD on mutable refs

iris: step indexing fold case of fundamental property from last day:

Reminder: Γ⊢e:τ => Γ⊨e:τ

Γ⊢e: τ[μα.τ/α]

HW: Same for step-indexed λ

—

monotonicity: if a val behaves like some type τ for k steps, then it has to behave like τ itself for <k steps too.

• aka downward closed
• v ∈ Vₖ[τ] => ∀j≤k. v ∈ Vⱼ[τ]

Got to prove monotonicity for all types

monotonicity and contravariance in funs

k steps = k steps to interact with it. ie, to use it.

syntactic correctness -> semantic correctness

• by means of invariants while running the prog

memory location info not needed for prog-preservation approach for type safety, but not here ???

Mutable references.

STLC with allocation and stuff: type of reference/pointer to a value of τ read/write from refs

τ := 1 | bool | τ1→τ2
   | ref τ    (type of ref to some mem loc which has a value of type τ)

e := () | ...  
   | new e      (create a new ref)
   | !e         (dereference/read)
   | e1 := e2   (assignment. overwrite if needed)

v := true | false | () | λx. ?
   |  l         (location)

Opsem:

One of: s(tore), m(emory), h(eap)

S: Loc -> Closed val l ↦ v ∈ S

Old rules has S, but unchanging

(S,e) -> (S',e')
────────────────────────────────────────────── 
(S, new v) -> (S[l↦v], l) where l ∈¬ dom(S)


(S, !l) -> (S, v) where l↦v ∈ S

(S, l:=v) -> (S[l↦v], ())  ie, update S, return unit

Eval context: call by val

E := new E
   | !E
   | E := e2
   | v := E

—

f(x: ref bool, y: ref bool) { free x; !y }

Aliasing problem. 2 ptrs pointing to same location. Freeing one would cause problem for others. What can type system do to prevent this?

Reason why once allocated, type can't be changed.

rust handles aliasing nicely ??

This lang is non-terminating. Loops possible. Eg:

let x: (unit -> unit) ref := new (λz. z)
let f = λz:unit. (!x) z
x := f
f tt

Named Landin's knot.

Infinite loop.

ie, STLC + refs => inf loop possible.

f = λz.

Type preserving updates. aka strong updates. GC is like refreshing mem so that it can be used for other types afterwards.

Review of what seen so far:

• Day1: Type = {I ∈ P(Closed vals)}
• Day2: Type = {I ∈ nat -> P(Closed vals)}

Possible world semantics. Meaning with respect to current world.

Typing rules with refs:

Γ ⊢ e:τ
----------------
Γ ⊢ new e: ref τ


Γ ⊢ e: ref τ
----------------
Γ ⊢ !e: τ


Γ ⊢ e1: ref τ       Γ⊢e2:τ
---------------------------
Γ ⊢ e1:=e2: 1

ie, 2 elim rules for ref

ψ location to type mappings New locations can come in, but their type shouldn't change => type preserving updates

D4

ψ = mapping from locations to semantic types (not syntactic types) = {l1↦V[τ1], l2↦V[τ2], ..} = store typing

S = mapping from locations to vals

Type world circularity Stratification to avoid circularity

—

For functions where there is mutref.

accessibility relation

V(k,ψ)[τ1→τ2] = {

possible worlds model is same as kripke models ??

D5

if true then 5 else false

semantically well-defined E⟦int⟧

but not syntactically

Our logrel was unary??? Binary also possible.

Re

References

[1]: Wright, A.K. and Felleisen, M., 1994. A syntactic approach to type soundness. Information and computation, 115(1), pp.38-94.ʰ