Declarative Programming and (Co)Induction
|
Instructors:
|
|
Where and When:
|
DISI
Università degli Studi di Genova
Via Dodecaneso 35
16146 Genova, Italy
How to reach the department
Length: 20 hours
The course will take place on the week 13-17 June 2011.
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 the first of May 2011.
Lessons in room 710
Labs in SW1
|
Description:
|
The course is a self-contained introduction to functional and logic
programming;
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 split into two modules, of 10 hours each. The
former will cover mainly functional programming and programming language
foundations, while the latter will cover inductive/co-inductive systems
and the issues of dealing with infinite objects.
|
Outline:
|
- Induction: inductive definitions and proofs by induction
- Small step and big step semantics, lambda calculus, inductive type system, soundness
- Functional programming in Haskell
- Lab: exercises in Haskell
- Lab: implementation of the inductive type system in Haskell
- Induction and coinduction: lowest and greatest fixed points, proofs by induction and by coinduction
- Abstract and operational semantics of Prolog and coProlog
- Programming in Prolog and coProlog
- Lab: exercises in Prolog and coProlog
- Lab: implementation of the inductive and coinductive type system in Prolog/coProlog
|
Course material (in progress...)
|
|
Some useful links:
|
|
Exam:
|
To be chosen by students, between the development of a small project, to a seminar on the subject of the course
|