read all of Enderton

typeset and read and understand my Feferman notes

read and understand all Pratt's course notes (universal algebra, category theory, chu spaces)

proof theory

## How does "intuition" help proops? Also, intuitionistic logic and intermediate logics

http://en.wikipedia.org/wiki/Intermediate_logic

"Classical logic is the only coatom in the lattice of superintuitionistic logics; the lattice of intermediate logics also has a unique coatom, namely SmL?."

"Smetanich's logic (SmL?): IPC + (¬q → p) → (((p → q) → p) → p)" note: (((p → q) → p) → p) is Pierce's law

curry-howard isomorphism

http://en.wikipedia.org/wiki/Realizability

http://en.wikipedia.org/wiki/Heyting_arithmetic

http://en.wikipedia.org/wiki/Markov%27s_principle

## computation

### computation and types

curry-howard isomorphism

http://en.wikipedia.org/wiki/Lambda_cube

http://en.wikipedia.org/wiki/Pure_type_system

http://en.wikipedia.org/wiki/Lambda-mu_calculus