The course aims to introduce formal computer science methods using tools based on type theory, especially AGDA. Lectures will
concern the grounds of type theory, namely intuitionistic logic and
lambda calculus, eventually focussing on dependent types and Martin-Loef
intuitionistic type theory, of which AGDA is an implementation.
- Teacher: Ugo De' Liguoro