PhD in Computer Science

Type theory at work: introduction to Agda

Type theory at work: introduction to Agda

Academic year 2023/2024

Sommario del corso

• Course objectives
• Program
• Suggested readings and bibliography
• Teaching tools
• Course card

Course objectives

Type theory, shortly TT, is a branch of logic providing both a foundation of constructive mathematics and of programming languages. Among other logical frameworks and proof assistants inspired to TT, Agda is one of the tools that are most directly connected to the theory and at the same time it is a quite powerful programming language, where types are expressive enough to implement functional verification of programs via type inference.

In this course we introduce the basics of TT and use Agda as a tool to explore the theory and, at the same time, to look to its applications as well as to its most recent developments in quite active research fileds.

Program

• The untyped λ-calculus and definability of recursive functionals
• The simply typed λ-calculus and its extensions in logic and functional programming foundations
• Intuitionistic logic, natural deduction systems and the Curry-Howard correspondence
• Dependent types: type theory at work
• Introduction to Agda: data types, equational reasoning and induction
• Π and Σ-types in Agda, formalizing higher-order intuitionistic logic
• Representing the λ-calculus within Agda
• Proving properties of functional programs with Agda
• Formalizing procedural programming languages in Agda

• Girard Lafont Taylor - Proofs and Types
• Sørensen Urzyczyn - Lectures on the Curry-Howard Isomorphism
• Thompson - Type Theory and Functional Programming
• Nordstrom Peterson Smith - Programming in Martin-Löf Type Theory
• Wadler - Programming Language Foundations in Agda
• Agda - Documentation
• A List of Tutorials
• The Agda WiKi

• Teaching material
• Exams and finals
• Class schedule
• Go to Moodle
• Register for the course
• Enrolled students
• Invia email agli studenti registrati
• Export table