Implementazione ottimale dei linguaggi funzionali
(Simone Martini, Stefano Guerrini)

Sharing graphs are a new technique for efficient implementationof functional languages. The goal is avoiding any duplication of work during reduction, optimizing sharing.
The interest of this technique is both practical andtheoretical.
The study of optimal reduction has provided important insights andconnections between linear logic, control structures, context semantics and the geometry of interaction, intensional semantics, withhope of applying its ideas as well in the area of full ab straction.
Moreover, recent complexity results seem to open interestingresearch perspectives on the definition of a good "intrinsic" complexity measure for the reduction cost of functional expressions.

Il Corso:

• Docenti: Simone Martini (Responsabile), Stefano Guerrini.

  ---

• Periodo: 2-25 Giugno.

  ---

• Ore di lezione: 27.

  ---

• Calendario Lezioni:

      Mar.    16:00-18:00
      Mer.    11:00-13:00
      Gio.    11:00-13:00
  
      Mer.    11:00-13:00
  
      Gio.    11:00-13:00
      Ven.    11:00-13:00
  
      Lun     11:00-13:00     14:30-16:30
      Mar      9:15-11:15     13:30-15:30
      Mer     10:00-12:00     14:00-16:00
      Gio      9:30-12:30 (Sala Multimediale)
  
  

  ---

• Luogo: Sala Riunioni, Dip. di Matematica e Informatica, Univ. di Udine.

  ---

• Credito: Una unità.

  ---

• Main topics of the course:
  • Introductory part
    • Basic definitions of lambda-calculus.
    • Basic definitions of proof-nets and linear logic.
    • Rewriting of nets and lambda-terms: cut-elimination and beta-reduction.
    • Labeled calculus and optimal reduction (sketch).
    • Definition of sharing graphs.
    • Lamping's algorithm.
  • Advanced part
    • Pragmatic of optimal implementations: BOHM.
    • Implementation of general functional programming primitives.
    • Optimal reductions and actual complexity, with a comparison of the cost of structural and logicalrules.

  ---

• Prerequisites:
  Some familiarity with formal systems (e.g., with some logical formalism for proofs like sequent calculus or natural deduction) and rewriting systems.

  ---

• References:
  Barendregt - The Lambda Calculus (North Holland)
  Girard, Lafont, Taylor - Proof and Types (Cambridge University Press)
  Asperti, Guerrini - The Optimal Implementation of Functional Programming Languages (Cambridge University Press, to appear)