Schema della sezione

  • 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