Abstract
In the first seminar, the speaker shared his experience of using demonstration assistants to teach the foundations of programming languages. Initially, he used Software Foundations, the interactive Coq lecture by Benjamin Pierce and co-authors. Dissatisfied with the presentation of demonstrations, he developed his own lecture, Programming Language Foundations in Agda, which formalizes the simply typed lambda-calculus with intrinsically typed syntax and explicit demonstrations in the form of executable functions. Thus, the proof of the progression property directly provides an evaluator for the language. An extension of the approach to the F system is currently being developed within the framework of the Plutus smart contracts language.
