Declarative Programming and (Co)Induction 2014
Indice degli argomenti
-
Teachers:
Davide Ancona (davide.ancona@unige.it), DIBRIS Univ. Genova
Elena Zucca (elena.zucca@unige.it), DIBRIS Univ. Genova
Period: 23 June - 27 June
Location: DIBRIS, via Dodecaneso 35
Format: one week (20 h) course including theory and practical (lab) session
Because of the compressed format, the course may be of interest for PhD students of other universities.
Summary: 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.
Exam: either a small project, or a seminar on the subject of the course.
-
-
Schedule (tentative): every day, from Monday through Friday: 11-13 and 14.30-16.30.
The course is split into two modules, of 10 hours each. The former will cover mainly functional programming and programming languages foundations, while the latter will cover inductive/co-inductive systems and the issue of dealing with infinite objects.
- 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