CSE 605 - Fall 2016 - Advanced Concepts in Programming Languages

Location: Davis 338A
Time: Friday 4:00 - 6:40
Instructor: Marco Gaboardi
e-mail: gaboardi@buffalo.edu

Credits: 3
Office Hours: Friday 10:30am or by appointment
Discussion forum: Piazza


Book: Software Foundations
Software: Coq proof assistant


This will be a graduate level course introducing techniques for formal reasoning about programs and specifications. These techniques are fundamental to ensure that programs are correct and reliable. Bugs and insecurities in software have a huge societal cost, but ensuring programs correctness and reliability in practice is difficult. To assist programmers with this task, researcher in programming languages and software engineering have developed tools based on formal logic. The rigor of formal logic is useful to provide a formal specification for the program behaviour and to check, assisted by a machine, that the program meets this formal specification.
To introduce students to formal reasoning about programs and the basic techniques behind it we will use the Coq proof assistant and we will follow the approach developed in the online book Software Foundations. The precise schedule of the different classes will appear below.

Course description

The course is offered as a 3 credits class. This will be a graduate level course where each student is required to submit weekly assignment. There will be a midterm and a final. Students will also be invited to engage on one project and to present the results at the end of the course. The project is optional. Discussion about all the aspects of the course will also take place on Piazza.


The grading will be based on assignments, participation in class, and midterm and final exam.
The final grade will be composed as:

  • 50% Assignments,
  • 20% Participation,
  • 15% midterm,
  • 15% final exam.

  • Students who are interested in a project to fulfill their curriculum requirement can replace the work on the project for the midterm and final exam. The project will then count for the 30% of the final grade. Students interested in this option should communicate with the instructor before the end of the third class. The assignment are mandatory for everybody.


    Every week at the end of the class the instructor will give the assignment for the week. The assignments must be submitted by the following Thursday at 6pm. The modality for submitting the assignments will appear here. Students can work on assignments in groups of two people. The components of the group have to be communicated to the instructor before the first assignment is due and must remain a group for the duration of the entire course.


    Projects can take different forms depending on the interest of each student and can be discussed directly with the instructor. Students interested in this option should communicate with the instructor before the end of the third class. Some examples of what would constitute a good project are: implementation and proof of correctness of a non-trivial algorithm, formalization of programming language meta-theory, etc.


    Date Topic Software Foundations Assignment
    8/29 Introduction to the course
    9/09 Functional programming in Coq Basics.v
    9/16 Proof by Induction Induction.v
    9/23 Working with Structured Data Lists.v
    09/30 Polymorphism and Higher-order Functions Poly.v
    10/07 More basic tactics Tactics.v
    10/14 Logic in coq Logics.v
    10/21 Inductively Defined Propositions IndProp.v
    10/28 Total and Partial Maps Maps
    11/04 Simple Imperative Programs Imp.v
    11/11 Program Equivalence Equiv.v
    11/18 Hoare Logic (Part I) Hoare1.v
    11/25 Fall Break - no class
    12/2 Hoare Logic (Part II) Hoare2.v
    12/9 Small Step Operational Semantics Smallstep.v
    12/16 Final