Declarative Programming and (Co)Induction
PhD Course at DIBRIS
Instructors
Davide Ancona, DIBRIS (davide.ancona@unige.it)
Elena Zucca, DIBRIS (elena.zucca@unige.it)
Where: DIBRIS - Università degli Studi di Genova - via Dodecaneso, 35.
Length: 20 hours
The course will take place on 23 June - 27 June. Because of the compressed format, the course may be of interest for PhD students of other universities. The (free) registration is mandatory and requires sending an email to instructors before June 16.
Description
The course is a self-contained introduction to functional programming, logic programming, and the use of induction and coinduction.
We will cover both foundational (inference systems, induction and co-induction, lambda calculus, type system and semantics) and practice/implementation (languages Haskell and Prolog) aspects in dealing with finite and infinite objects.
The course is organized in two modules.
- First module 10 hours: inductive definitions and proofs by induction, small step and big step semantics, lambda calculus, inductive type, system, soundness. Functional programming in Haskell.
- Second module 10 hours: induction and coinduction, lowest and greatest fixed points, proofs by induction and coinduction, abstract and operational semantics of Prolog and coProlog. Programming in Prolog and coProlog.
Exam
Either a small project, or a seminar on the subject of the course.Tentative schedule
- [Monday 10.30-13 Room 711] Induction: inductive definitions and proofs by induction
- [Monday 14.30-17 Room 711 + SW2] Functional programming in Haskell + Lab: simple programs in Haskell
- [Tuesday] NO LECTURE since university is closed
- [Wednesday 10.30-13 Room 711] Small step and big step semantics, lambda calculus type system, soundness
- [Wednesday 14.30-17 Room 711 + SW2] Lab: programs in Haskell
- [Thursday 10.30-13 Room 711] Recursive definitions and fixed points. Logic programs as inference systems
- [Thursday 14.30-17 Room 711+SW2] Lab: simple programs in Prolog and coProlog with ground queries
- [Friday 10.30-13 Room 711] SLD and coSLD resolution
- [Friday 14.30-17 Room 711+SW2] Lab: programs in Prolog and coProlog
Aulaweb If you owe an UnigePass account, you can access the Aulaweb module of the course.
Course material
Module 1: First lab on Haskell
Module 1: Slides on Small Step Semantics, Lambda Calculus and Type Systems
Module 1: Slides on Haskell, continued
Module 1: Second lab on Haskell
The course is part of the activities of the SEPL research program.