Seminar: Foundations for Programming Languages

This is the web page for a seminar on the foundations for programming languages. We study the book Foundations for Programming Languages by John C. Mitchell and formalize the definitions, theorems and exercises in this book by using Abella and Coq.

Prerequisites

You need to get familiar with the following tools:

• Lambda Prolog: We shall use this meta-language to formalize the object languages in the book.
  • Software: Download the Teyjus implementation of Lambda Prolog.
  • Tutorial: https://sites.google.com/site/lambdaprologvideotutorial/home/
  • Book: https://sites.google.com/site/proghol/
  • Installation: Consult the instructions at here.
    There is also an emacs mode coming with the source code. See the "emacs" directory.
• Abella: We shall use this proof assistant to prove the meta-properties about the object languages.
  • Software: Download the prover at https://github.com/abella-prover/abella
  • Tutorial: https://jfr.unibo.it/article/view/4650
  • Installation: Consult the instructions at here.
    There is also a version of proof general supporting Abella. Download it at here.
• Coq: We shall use this proof assistant to investigate the denotational semantics of object languages.
  • Software: Download the prover at https://coq.inria.fr/
  • Book: Software Foundations

Tentative Schedule

• Chapter 1: Introduction. Hosted by Jinhua Wu. Sep 25th, 2021.

  Exercise: Formalize the Church-Rosser theorem of the untyped lambda calculus in Abella.

• Chapter 2.1-2.4: PCF. Hosted by Wanting Li. Oct 9th, 2021.
• Chapter 2.5-2.6: PCF. Hosted by Siyu Liu. Oct 23th, 2021.
• Chapter 3.1-3.4: Algebraic Data Types. Hosted by Litao Zhou. Nov 6th, 2021.
• Chapter 3.5-3.7: Algebraic Data Type. Hosted by Zilong Zhong. Nov 20th, 2021.
• Chapter 4.1-4.4: Simply-Typed Lambda Calculus. Hosted by Ling Zhang. Dec 4th, 2021.