type theory and well-founded sets

Program Verification

Proving certain properties about programs—perhaps types, but not just types.

Program verification proofs are usually written manually, but uses a proof assistant which…

proof assistant

Helps with proof, by:

1. checking the proof for correctness (uses type theory)
2. helps automate the easy parts

Agda

A whirlwind tour through Agda

Agda whitespace rules

Agda allows UNICODE! IN! VARIABLES! so:

i:Int is! not! i : Int

• the first thing is an indentifier of type i:Int
• the second thing is an i of type Int

Dependent Type Theories with Agda

booleans

Consider two empty declarations:

data False : Set where

this is a type with nothing in it!

record True : Set where

this is a type with exactly one thing in it!

False has no elements in it, and True has exactly one element in it.

Today’s lambda calculus

why static typing?

• find type errors when the program is written
• …which makes guarantees for all possible executions
• …which can leads to a faster execution because you don’t have to do runtime type checks (this is actually non-trivial!)

why (not) static typing

• you can detect type errors during execution—so it can be sound as well
• this is not untyped: you can still have types (untyped is raw bits)

implementation

every value has a “tag” — for instance, integers vs. functions

more Combinator Calculus and confluence

Lambda Calculus

Like SKI Calculus, its a language of functions; unlike SKI Calculus, there are variables.

\begin{equation} e\to x \mid \lambda x.e \mid ee \mid (e) \end{equation}

meaning, we have:

• a variable \(x\)
• an abstraction \(\lambda x . e\) (a function definition)
• an application \(e_1 e_2\)

we call \((\lambda x . e)e’\) (a function and its argument, ready for reduction) a redex.

abstraction

def f(x) = e

can be written as:

\begin{equation} \lambda x.e \end{equation}