Abstract. 
Mikrokosmos is an educational untyped and simply typed lambda-calculus interpreter. For students, it is a tool to learn lambda-calculus and intuitionistic logic by coding. For educators, it is a didactic resource, grounded in the theoretical implementation of a functional programming language, so that they can integrate it with other learning materials.