Drafts from my bachelor's thesis. Suggestions or corrections in grammar and spelling are welcome.
- [1] Untyped lambda calculus
- [2] Simply typed lambda calculus
- [3] The Curry-Howard correspondence
- [5] Mikrokosmos: a lambda interpreter. Implementation of lambda expressions
- [6] Mikrokosmos: user interaction
- [7] Mikrokosmos: usage
- [8] Mikrokosmos: programming environment
- [9] Programming in the untyped lambda calculus
- [10] Programming in the simply typed lambda calculus
- [11] Category theory
- [15] Adjoints, monads, algebras
- [16] Lawvere theories
- [22] Martin-Löf type theory
- [23] Programming in Martin-Löf type theory
[Bonus] I am taking notes on the homotopy type theory book. They were not meant to be published and MathJax is not working properly because of the use of latex macros. I will update them when I finish the bachelor's thesis.