Drafts from my bachelor's thesis. Suggestions or corrections in grammar and spelling are welcome.
-  Untyped lambda calculus
-  Simply typed lambda calculus
-  The Curry-Howard correspondence
-  Mikrokosmos: a lambda interpreter. Implementation of lambda expressions
-  Mikrokosmos: user interaction
-  Mikrokosmos: usage
-  Mikrokosmos: programming environment
-  Programming in the untyped lambda calculus
-  Programming in the simply typed lambda calculus
-  Category theory
-  Adjoints, monads, algebras
-  Lawvere theories
-  Martin-Löf type theory
-  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.