Foundations of software

CS-452

Media

This file is part of the content downloaded from Foundations of software.
Course summary


Introduction

Software foundations (or theory of programming languages) is the mathematical study of the meaning of programs. Students will learn ways to describe program behaviors, and mathematical tools to formalize and check interesting properties of programs. This course concentrates on  lambda calculus, operational techniques and type systems.

Teaching team

Lecturers

Martin Odersky  martin.odersky@epfl.ch

Thomas Bourgeat thomas.bourgeat@epfl.ch

Assistants

Martina Camaioni martina.camaioni@epfl.ch

Yichen Xu yichen.xu@epfl.ch

Cao Nguyen Pham nguyen.pham@epfl.ch


Grading rubric

Final course grade will be computed as follows:

  • Homework: 20%
  • Projects: 20%
  • Final exam: 60%

Over the course of the semester, we will post five assignments that will require you to code up or do proofs about five moderately complex Lean4 applications (one per each assignment) that highlight certain theoretical aspects of the course.

Every assignment will become available on Moodle at due time (usually after the deadline of the previous assignment). The procedure to submit assignments will be specified later.


Class Material


The material for the class will be made available on this Moodle every monday. Part of the lectures will involve live programming, the lean4 file corresponding will be shared on gitlab.


Continuous Evaluation


Every two to three weeks, a short lab/project will be due. Each student will have to come to the Tuesday session (Between 10am and 12pm) or Wednesday between (2pm and 4pm)  and show their homework (code + paper) to the TA.

There will be one  paper homework, serving a similar purpose to a midterm: train the students for the final exam. This homework will be on paper (not on machine), and will be similar in content as for the final exam.

Office Hour

Wednesdays 5-7pm in BC145 (Except Wednesday 30th of April cancelled and moved to Tuesday 29th 5-7pm).

Final Exam


Final exam will be during the exam period, on paper.



Resources about Lean4

https://leanprover-community.github.io/learn.html

Useful resources to find theorems and lemmas:
https://loogle.lean-lang.org/
https://leanprover-community.github.io/mathlib4_docs/index.html