PL Seminar: Software Foundations I
- ÕIS data: MTAT.03.271, 3 ECTS
- Time: Tuesdays, 10:15. (Starting February 12)
- Place: J. Liivi 2-512.
- Teachers: Vesal Vojdani, Kalmer Apinis (kalmera@ut.ee)
Wouldn't it be nice if we could prove that our programs are correct, or that some program terminates in linear time, or even that an optimized algorithm A is equivalent to a unoptimized but easy-to-read algorithm B. Although difficult, it is already possible (and sometimes practical) to produce machine-checkable proofs of such properties with the help of proof assistants such as Coq.
This seminar will lay the groundwork for writing proofs about programs. We will follow the first volume of the Software Foundations book by Benjamin C. Pierce et al. to learn what it takes to reason about algorithms.
The lecturers will cover the core but leave some topics for student presentations. The course is mainly intended for graduate students, but highly motivated undergraduate students can also do well. Familiarity with functional programming is useful but not essential.
About the Seminars
The programming language research seminars are a series of independent courses/seminars that focus on different topics in programming languages. While the study information system presents this as a 12 ECTS course with 4 parts, the parts are not generally dependent on each other. This term's seminar, however, is important for the following ones.
- Types and Programming Languages (Fall 2018)
- Software Foundations I: Logical Foundations (Spring 2019)
- Software Foundations II: Programming Language Foundations (Fall 2019)
- Software Foundations II or III. (Fall 2020)
The type theory seminar is useful, but not necessary to understand Software Foundations. It will, however, be more difficult to take the seminar next term if you do not participate in this term's seminar!