Written by Luka Kerr on November 11, 2018


Programming languages are formal languages which allows us to:

Stages of a Compiler



Semantic Analysis


Code Generation

Backus-Naur Form

Natural Deduction




Hypothetical Derivations

Rule Induction

The process of using existing inference rules to prove a property in the language. The assumptions are called inductive hypotheses.

In general, given a set of rules $R$, we may prove a property $P$ inductively for all judgements that can be inferred with $R$ by showing, for each rule of the form $\frac{J_1 \quad J_1 \quad \dots{} \quad J_n}{J}$ that if $P$ holds for each of $J_1 . . J_n$, then $P$ holds for $J$

The base cases of induction are axioms, all other rules are inductive cases and the premises of each rule give rise to inductive hypotheses

Mathematical Induction Steps (revision)



Concrete syntax is described by judgements on strings, which describe the actual text input by the programmer. It is ambiguous and not suitable for compiler implementation and proofs

Abstract syntax is a representation of a program where extraneous information and ambiguity is removed. It is usually represented as a tree, known as an abstract syntax tree



A program usually has variables, and where these variables are declared is known as the binding occurance of the variable. The scope of the variable is wherever the variable has a value and is defined. For example:

let x = 5 in     -- binding occurance of x
  let y = 2 in   -- scope of x
    x + y        -- usage occurance of x
  end            -- end scope of x

The process of finding the binding occurance of each used variable is called scope resolution.




Variable Capture

First Order Abstract Syntax

De Bruijn Indices

Higher Order Abstract Syntax

Higher order abstract syntax relies on the meta language to facilitate binding of variables. Because of this, many problems such as malformed syntax, capture and $\alpha$-equivalence is solved since it is handled by the meta language

For example, a term language $t$ can be defined as

t ::= Symbol    -- symbols
     | x        -- variables
     | t1 t2    -- application
     | x. t     -- binding or abstraction


Lambda calculus is a system using mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution

The term language $t$ above can be slightly changed:

t ::= Symbol    -- symbols
     | x        -- variables
     | t1 t2    -- application
     | λx. t    -- lambda abstraction






Static Semantics

Dynamic Semantics

Evaluation Strategies


Functional Programming

A programming language derived from or inspired by the $\lambda$-calculus, or derived from or inspired by another functional programming language

Purely Functional

Cost Models

Operational Cost Models

Control Flow

To define an abstract machine where all the rules are axions, we use a stack.


\[\begin{array}{l} \dfrac{}{\circ \ \textbf{Stack}} \quad \dfrac{f \ \textbf{Frame} \quad s \ \textbf{Stack}}{f \triangleright s \ \textbf{Stack}} \end{array}\]


\[\begin{array}{ll} & \circ \succ (\text{Plus (Plus (Num 2) (Num 3)) (Num 4)}) \\ \mapsto & \text{(Plus} \ \square \ \text{(Num 4))} \triangleright \circ \succ \text{(Plus (Num 2) (Num 3))} \\ \mapsto & \text{(Plus} \ \square \ \text{(Num 3))} \triangleright \text{(Plus} \ \square \ \text{(Num 4))} \triangleright \circ \succ \text{(Num 2)} \\ \mapsto & \text{(Plus} \ \square \ \text{(Num 3))} \triangleright \text{(Plus} \ \square \ \text{(Num 4))} \triangleright \circ \prec 2 \\ \mapsto & \text{(Plus 2} \ \square \ \text{)} \triangleright \text{(Plus} \ \square \ \text{(Num 4))} \triangleright \circ \succ \text{(Num 3)} \\ \mapsto & \text{(Plus 2} \ \square \ \text{)} \triangleright \text{(Plus} \ \square \ \text{(Num 4))} \triangleright \circ \prec 3 \\ \mapsto & \text{(Plus} \ \square \ \text{(Num 4))} \triangleright \circ \prec 5 \\ \mapsto & \text{(Plus 5} \ \square \ \text{)} \triangleright \circ \succ \text{(Num 4)} \\ \mapsto & \text{(Plus 5} \ \square \ \text{)} \triangleright \circ \prec 4 \\ \mapsto & \circ \prec 9 \\ \end{array}\]


Safety and Liveness


A safety property states that something bad does not happen. For example:

I will never run out of money


A liveness property states that something good will happen. For example

If I start saving money now, eventually I will be rich

Type Safety

A property that states that well-typed programs do not go wrong

Progress and Preservation

To prove that a well-typed program either goes on forever or reaches a final state, we use the following two lemmas

For example:

\[e_1 : \tau \mapsto \underbrace{e_2: \tau}_{\text{preservation}} \overbrace{\mapsto e_3 }^{\text{progress}} : \tau \mapsto \dots{} \\\]

Composite Data Types

Unit Types - $()$

A type that has just one value - $\textbf{1}$

Product Types - $\tau_1 \times \tau_2$

Data that is stored in one value as a pair. “$\tau_1$ and $\tau_2$”

\[\dfrac{e : \tau_1 \times \tau_2}{\text{fst} \ e : \tau_1} \quad \dfrac{e : \tau_1 \times \tau_2}{\text{snd} \ e : \tau_2}\]

Sum Types - $\tau_1 + \tau_2$

Data that may be one of two forms. “$\tau_1$ or $\tau_2$”

\[\dfrac{e : \tau_1}{\text{InL} \ e : \tau_1 + \tau_2} \quad \dfrac{e : \tau_2}{\text{InR} \ e : \tau_1 + \tau_2} \quad \dfrac{e : \tau_1 + \tau_2 \qquad x : \tau_1, e_1 : \tau \qquad y : \tau_2, e_2 : \tau}{\textbf{case} \text{ e } \textbf{of} \text{ InL x} \to e_1; \text{InR y} \to e_2}\]

Empty Type - $0$

A type that cannot be constructed, and will never be evaluated

Recursive Types - $\textbf{rec} \ t. \tau$

A type that allows reference to the entire type recursively

\[\dfrac{e : \tau [t := \textbf{rec} \ t. \tau]}{\text{roll} \ e : \textbf{rec} \ t. \tau} \quad \dfrac{e : \textbf{rec} \ t. \tau}{\text{unroll} \ e : \tau [t := \textbf{rec} \ t. \tau]}\]

Curry-Howard Correspondence

\[\begin{array}{ll} \times & \land \\ \text{+} & \lor \\ \to & \implies \\ 1 & \top \\ 0 & \bot \\ \forall & \forall \end{array}\]


A way to specify that we don’t care what data type is used (also known as generics)

Type Abstraction

The ability to define functions regardless of specific types.

swap = type a. type b.
         recfun swap :: (a, b) -> (b, a) x = (snd x, fst x)

Type Application

The ability to instantiate polymorphic functions to specific types.

swap@Int@Bool (3, True)



Template Instantiation

Automatically generate a monomorphic copy of each polymorphic function based on the types applied to it.

For example for a type application like swap@Int@Bool

swap = type a. type b.
         recfun swap :: (a, b) -> (b, a) x = (snd x, fst x)

would be replaced statically by

swap = recfun swap :: (Int, Bool) -> (Bool, Int) x = (snd x, fst x)
Advantages Disadvantages
Little to no run-time cost Large binary size if many instantiations are used
Easy to implement Can lead to long compilation times


All data types are represented as a pointer to a data structure on the heap, where all pointers are exactly 32 or 64 bits large.


The principle of parametricity states that the result of polymorphic functions cannot depend on values of an abstracted type.

More formally, given a polymorphic function $g$ that takes a type parameter, if the function $f : \tau \to \tau$ was run on some values of type $\tau$, then run on $g\text{@} \tau$ on the result, that will give the same results as running $g\text{@} \tau$ first, then $f$.


head :: [a] -> a
-- parametric example
f (head list) = head (map f list)

concat :: [[a]] -> [a]
-- parametric example
map f (concat list) = concat (map (map f) list)


A substitution $S$ to unification variables is a unifier of two types $\tau$ and $\rho$ if $S_\tau = S_\rho$.

Furthermore, it is the most general unifier of $\tau$ and $\rho$ if there is no other unifier $S’$ where $S_\tau \sqsubseteq S’ \tau$.

We write $\tau \stackrel{U}{\sim} \rho$ if $U$ is the most general unifier of $\tau$ and $\rho$.


\[\begin{array}{lll} 1) & \alpha \times (\alpha \times \alpha) \sim \beta \times \gamma & \alpha = \beta, \gamma = (\alpha \times \alpha) \\ & \alpha \times (\alpha \times \alpha) \sim \alpha \times (\alpha \times \alpha) \\ \\ 2) & (\alpha \times \alpha) \times \beta \sim \beta \times \gamma & \beta = (\alpha \times \alpha), \gamma = \beta \\ & (\alpha \times \alpha) \times (\alpha \times \alpha) \sim (\alpha \times \alpha) \times (\alpha \times \alpha) \\ \\ 3) & \text{Int} + \alpha \sim \alpha + \text{Bool} \\ & \text{TypeError} \\ \\ 4) & (\alpha \times \alpha) \times \alpha \sim \alpha \times (\alpha \times \alpha) \\ & \text{No Unifier} \\ \end{array}\]

Linear Types

$A \multimap B \quad$ $A$ can be transformed into $B$

$A \otimes B \quad$ You’ve got both $A$ and $B$

$A \oplus B \quad$ You’ve got either $A$ or $B$

$A \text{ \& } B \quad$ You can pick from $A$ or $B$

$!A \qquad$ You’ve got an unlimited amount of $A$

Abstract Data Types

A type defined not by its internal representation, but by the operations that can be performed on it.

Existential Types

$\forall a. \tau$ $\exists a . \tau$
When producing a value, $a$ is an arbitrary, unknown type. When consuming a value, $a$ may be instantiated to any desired type. When consuming a value, $a$ is an arbitrary, unknown type. When producing a value, $a$ may be instantiated to any desired type.

Bag ADT Example


Type Classes

Dictionaries and Resolution


To add subtyping to a language, we define a partial order on types $\tau \le \rho$ and a rule of subsumption

\[\dfrac{e : \tau \qquad \tau \le \rho}{e : \rho}\]

What this partial order means is up to the language. There are two main approaches

Product Types

$\dfrac{\tau_1 \le \rho_1 \qquad \tau_2 \le \rho_2}{(\tau_1 \times \tau_2) \le (\rho_1 \times \rho_2)}$

Example: $(\text{Int} \times \text{Int}) \le (\text{Float} \times \text{Int})$

Sum Types

$\dfrac{\tau_1 \le \rho_1 \qquad \tau_2 \le \rho_2}{(\tau_1 + \tau_2) \le (\rho_1 + \rho_2)}$

Example: $(\text{Int} + \text{Float}) \le (\text{Float} + \text{Float})$


$\dfrac{\rho_1 \le \tau_1 \qquad \tau_2 \le \rho_2}{(\tau_1 \to \tau_2) \le (\rho_1 \to \rho_2)}$

Example: $(\text{Float} \to \text{Int}) \le (\text{Int} \to \text{Float})$



Parallelism is the simultaneous execution of code on multiple processors or cores for the purposes of improved performance. E.g. simulations, neural networks.

Concurrency is an abstraction for the programmer, allowing programs to be structured as multiple threads of control, called processes. E.g. servers, GUI applications, kernels.


Cost Models

Critical Sections

A critical section is a group of multiple steps, grouped into one single atomic step.

We want to ensure two main properties:


A lock is a common mean of concurrency control. It is typically abstracted into two operations

Software Transactional Memory

Each transaction is executed optimistically, rather than pessimistically (i.e. locks).

Each transaction has an associated log, which contains

First the log is validated, and, if validation succeeds, changes are comitted. Validation and commit are one atomic step. If validation fails, the transaction is re-run.


withdraw :: Account -> Int -> STM ()
withdraw acc amt = do
  balance <- readTVar amt
  if amt > 0 && amt > balance then
    writeTVar acc (balance - amt)


Database Guarantees