Home | Search | Help  
Home Page UniversitÓ di Genova
DISI -> People -> Faculty -> Giovanni Lagorio -> Declarative Programming and (Co)Induction

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