From Wikipedia, the free encyclopedia
Jump to: navigation, search
Flag of Earth 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



from the paper Codata and Comonads in Haskell [1] (pdf)

Computer theory[edit]

Automata theory[edit]

Pushdown automata theory[edit]

Turing theory[edit]

Types and Programming Languages[edit]

Not covered[edit]


Untyped arithmetic expressions[edit]

Definition styles[edit]

Symantics styles[edit]

ML example (ch4)[edit]

The Untyped Lambda-calculus[edit]


Free variables and bound variables:

Evaluation strategies:

Lambda calculus grammmar:

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

Language levels:


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[edit]

Capture (cont):

Nicholas de Bruijn:

Explicit substitution:

Typed Arithmetic Expressions[edit]

Safety = Progress + Preservation

Simply typed lambda-calculus[edit]

Type assignment system:


  • Γ ⊢ 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 Γ


  • Γ 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[edit]


Addr = <physical:PhysicalAddr, virtual:VirtualAddr>;
a = <physical:pa> as Addr;

also for null-able types:

OptionalNat = <none:Unit, some:Nat>;


EuroAmount = <euros:Float>;