The course is aimed to introduce formal methods in computer science by means of 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.
Applications to foundations of programming languages, program verification and language-based security are illustrated.
- Teacher: Ugo De' Liguoro