# User:Pengo/comp

Peter Halasz (talk) ?

Subpages: /dia | /missing | /org | /pages | /photo | /quotes

Ideas: /rants | /ite | /R | /teletaxo

Subjects: /bot | /comp | /ee | /eco | /fringe | /micro | /sd | /zoo

Incubator: /ownimg | /teletaxotest | /self

Computer science and related topics

## Types and Programming Languages

### The Untyped Lambda-calculus

Alternatives:

Lambda calculus grammmar:

```t ::=            terms:
x         variable
λx.t      abstraction or lambda-abstraction
t t       application
```

Language levels:

Capture:

Free variables:

• FV(t) is the set of free variables of term t.
• FV(x) = {x}
• FV(λx.t1) = FV(t1)\{x}
• FV(t1 t2) = FV(t1) ∪ FV(t2)

### Nameless representation of types

Capture (cont):

Explicit substitution:

### Typed Arithmetic Expressions

Safety = Progress + Preservation

### Simply typed lambda-calculus

symbols:

• Γ ⊢ t:T "the closed term t has type T under the empty set of assumptions."
• (not from book)inference, reduces to. x ⊢ y means y is derived from x
• Table of mathematical symbols
• Γ ⊢ x : R, then x:R ∈ Γ (the type assumed for x in Γ is R)
• dom(Γ) gives the set of variables bound by Γ

context:

• Γ is context
• Γ is the set of assumptions about the types of the free variables in t.
• Γ ⊢ ... "using the context Γ ..."
• typing context or type environment
```T ::=            types:
T→T       type of functions

Γ ::=            contexts:
∅        empty context
Γ,x:T     term variable binding
```

more lemmas:

Curry-Howard Correspondence:

Logic Programming languages
propositions types
proposition P ⊃ Q type P → Q
proposition P ∧ Q type P × Q
proof of proposition P term t of type P
proposition P is provable type P is inhabited (by some term)

Thorough discussions of this correspondence:

• Girard, Lafont, and Laylot (1989)
• Gallier (1993)
• Sørensen and Urzyczyn (1998)
• Pfenning (2001)
• Goubault-Larrecq and Mackie (1997)
• Simmons (2000)

Erasure and Typability

### Simple extensions

e.g.

```Addr = <physical:PhysicalAddr, virtual:VirtualAddr>;
```OptionalNat = <none:Unit, some:Nat>;
```EuroAmount = <euros:Float>;