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 1317 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 selfcontained introduction to functional and logic
programming;
we will cover both foundational (inference systems, induction and
coinduction, lambda calculus, typesystem 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/coinductive 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
