The core of a functional language The core as a formal system: type-free l-calculus Computation as rewriting 1 Computation as rewriting 2 Computation is deterministic The power of type-free l-calculus Types for terms The power of typed l-calculus Increasing the power of typed l-calculus Typed l-calculus and logical proofs The Curry - Howard isomorphism 1 The Curry - Howard isomorphism 2 Normalisation Second order logic Expressiveness of second order l-calculus From second to higher order: Fw Dependent types: LF Propositions-as-types Summing up Putting all together
