Systems and
Formalisms Lab

CS-428: Interactive Theorem Proving

Course team

Clément Pit-Claudel, Aurèle Barrière
Simon Guilloud, Yawen Guan, Shardul Chiplunkar
Dario Halilovic

Contact email

itp-staff@groupes.epfl.ch

Meeting times

Tuesdays 8AM-11AM (lectures + exercises, ELD 020 INF 119)
Thursdays 1PM-3PM (labs, INM 202)

Course links
Coq resources
Final grade breakdown

  • Labs 40% (drop lowest)

  • Project 60%

Deadlines and late submissions

Deadlines on Fridays at 6PM
No-penalty extension until midnight
Beyond that: -15% for up to 24h; -30% up to 48h; 0 beyond 48h.

Labs

Rubric

Tests, implementation quality, checkoffs

Submission

On Moodle (for labs, submit only the Implementation.v file)

Collaboration

OK to whiteboard together, but final submission must be your own code / text

Detailed instructions

Your automated grade is the sum of the point values of the individual theorems that you solved, as documented in the specification file. There is no partial credit for partially proven theorems except where explicitly specified.

Checkoffs are in-person oral examinations on labs 1 and 3. Checkoffs last approximately 8-10 minutes, during which you present your lab solution and explain your proofs. We ask that you follow roughly the following template:

  • 1 minute overview of your solution (scroll through with the TA giving you the check-off)

  • 7 minutes deep dive into one or two interesting theorems of your choice:

    • 3 minutes on the proof plan / big idea / key lemmas, without looking at code and without Coq jargon (no “tactics”, “destruct”, “repeat”, …). Pretend you're talking to a computer scientist who knows nothing about Coq.

    • 4 minutes on the code, showing how it follows the logic of your proof plan.

Grading scheme

Code submissions

75%, automatically graded (pass/fail per definition or theorem)

In person checkoffs (labs 1 and 3)

25% (of which 20% for lab 1 and 80% for lab 3), manually graded on the following criteria (10pts per checkoff):

  • Implementation is clean and readable: 5pts
    Code: no redundant code, no useless definitions
    Proofs: no useless tactics, no excessive repetition, no unnecessary proof steps

  • Proof plan is clear, complete, succinct, and well understood: 4pts
    Explained in English (not code); complete

  • Code and proofs are kept private: 1pt

Projects

Rubric

Check-in, report, implementation, presentation

Collaboration

Projects in teams of 2
All forms of collaboration allowed, but make sure to give credit

Project ideas

  • Update the Warblre JS Regex spec to the latest ECMAScript standard.

  • Implement, document, and verify a 2-3-tree-based finite map, and prepare it for submission to Coq standard's library (FMap), or one of the more recent map interfaces (mmap, stdpp).

  • Formalize part of an open language standard, technical standard, or RFC, and prove some properties of the associated algorithms: XPath, CSS, Dart, RFC 9485, GNU Make.

  • Formalize parts of an existing language, type system, or algorithm, either from your research or from a recently published paper.

  • Specify and verify a pass of your CS420 Advanced Compiler Construction compiler (aim for higher complexity than the example passes from lab 5).

  • Formalize and verify algorithms from one of your bachelor classes (Computer Networks, Algorithms I, Computer Systems, Parallelism and Concurrency); either purely functional using plain Coq or imperative using a separation-logic framework.

  • Port (a subset of) labs and exercises from another EPFL class to Coq.

Timeline

Projects will happen over the last 8 weeks of the class:

Week 8

Project proposal (one-page extended abstract), submitted on Moodle.

Week 11

In-person check-in (code walk-through), graded by a TA in lab session.

Week 14

Oral project presentation, given to the class.

EOS

Final report, submitted on Moodle.

Detailed instructions

Project proposals

Aim for one printed page, and assume an informed (but not expert) reader. Submit your proposal as PDF. A good project proposal should follow the format of an “extended abstract”, with the following parts (roughly):

Introduction / problem statement (1/4 page)

State what the problem is (a good example helps a lot) and (ideally) why it matters. Keep it short and to the point: give enough context to understand, but not more. It should be clear from the introduction what it means to solve the problem.

Proposal (1/2 page)

Summarize what you plan to do: how will you approach the problem? What deliverables (artifacts, proofs, ...) will you produce? What interesting challenges do you foresee?

Timeline and responsibilities (1/4 page)

Break down you project into small components and milestones, then estimate how they depend on each other and how long each will take. Organize the milestones on a timeline. Clarify who will do what, and how you will organize the work of your group.

Code walk-throughs

Prepare two slides to recap what the project is about, what progress you have made, and who did what (about 2-3 minutes), then a code demo (about 8-10 minutes), and be ready for 3-5 minutes worth of questions and interruptions. All team members should contribute equally to the presentation.

Presentation

Aim for 10 minutes, plus 5 minutes of questions / interruptions. The structure of the talk should be similar to that of the final report (below), skipping the timeline and related work parts.

Final report

Aim for four to six printed pages, and assume an informed (but not expert) reader. Submit your report as PDF. The structure is similar to that of a tech report:

Abstract (1 paragraph)

A one-paragraph condensed version of the motivation and results.

Introduction / Motivation (1/2 page)

This should be an expanded version of the proposal.

Approach (2 pages)

Summarize how you solved the problem. Aim to present the general approach and the most challenging aspects in enough detail that someone else could reproduce your approach, and try to justify non-trivial design choices.

Results (1/2 pages)

Clarify exactly what you achieved and what the limitations are.

Reflections on the timeline (1/2 page)

Compare the actual development of the project to your original timeline. Highlight the main divergences. Clarify who did what.

Related work, future work, conclusion (1/2 page)

Highlight related efforts, put your project in perspective, and suggest interesting continuations of your work.

Grading scheme

In principle, team members will receive the same grade, unless there are pronounced differences in contributions to a project.

Project proposal

5%, graded on the following criteria:

  • Project goals are clear: 40%

  • Deliverables are adequate: 20%

  • Proposed approach is reasonable: 20%

  • Timeline and individual responsibilities are realistic: 20%

Code walk through

25%, graded on the following criteria:

  • Intro is clear and complete: 15%

  • Code is clean and readable: 10%

  • Walkthrough is easy to follow: 20%

  • Questions are answered satisfactorily: 20%

  • Design decisions are motivated during walkthrough: 10%

  • Project is on track for completion: 20%[1]

  • Contributions of each team member are clearly identified: 5%

Project presentation

30%, graded on the following criteria:

  • Presentation is clear and structured: 25%

  • Motivation is convincing: 10%

  • Approach and design are adequate and motivated: 10%

  • Results are presented completely and accurately: 5%[2]

  • Demo / highlight is compelling: 25%

  • Questions are answered correctly and completely: 15%

  • Time is used judiciously: 10%

Final report & implementation

40%, graded on the following criteria:

  • Writing is clear and structured: 25%

  • Motivation is convincing: 10%

  • Approach and design are adequate and motivated: 10%

  • Results are presented completely and accurately: 5%[2]

  • Deliverables are functional and sufficiently complete: 25%

  • Code is clean and readable: 15%

  • Limitations and Related work are adequately discussed: 10%

Calendar

Week 1 (Feb 18 & 20)

Topics

Intro to Coq, inductive types, fixpoints, tactics, proofs by induction

Course materials
Lab 1 materials
Optional readings and exercises

Week 2 (Feb 25 & 27)

Topics

Polymorphism, data abtractions

Course materials

Clément’s livecoding transcripts:

Lab 2 materials
Optional readings and exercises
Deadlines

Lab 1 due

Lab 1 checkoff due

Week 3 (Mar 4 & 6)

Topics

Interpreters, automation

Course materials
Lab 3 materials
Optional readings and exercises
Deadlines

Lab 2 due

Week 4 (Mar 11 & 13)

No class on March 11th: IC Boost day. Lecture moved to March 13th (Thursday) in replacement of lab session.

Topics

Inductively defined propositions, rule induction

Course materials

Clément’s livecoding transcript: Inductive propositions and proofs
[Coq source file]
[Video: Part 1, Part 2]

Exercise materials

(On gitlab: Regex from SF)

Optional readings and exercises

Week 5 (Mar 18 & 20)

Topics

Big-step semantics, logic programming

Course materials

Clément’s livecoding transcripts:

Lab 4 materials

Hints

Deadlines

Lab 3 due

Lab 3 checkoff

Week 6 (Mar 25 & 27)

Topics

Small-step semantics

Course materials

Aurèle’s livecoding transcript: Small-step semantics (adapted from FRAP’s OperationalSemantics.v)
[Coq source file]
[Video]

Lab 5 materials
Deadlines

Lab 4 due

Week 7 (Apr 1 & 3)

Topics

Simply-typed lambda calculus

Course materials

Aurèle’s transcript
[Coq source file]
[Video]

Deadlines

Project teams

Optional readings and exercises

Software foundations: Simply-typed Lambda Calculus

Week 8 (Apr 8 & 10)

Guest lecture: Samuel Grütter, Live Verification

Deadlines

Lab 5 due

Week 9 (Apr 15 & 17)

Topics

Simple dependent types

Deadlines

Project proposals

Course materials

Transcript
[Coq source file]
[Video]

Easter break (Apr 22 & 24)

No class: EPFL holidays!

Week 10 (Apr 29 & May 1)

Lecture / Labs swapped. Lecture moved to March May 1st (Thursday); labs on April 29th (Tuesday).

Topics

Hoare logic

Course materials

Aurèle’s transcript
[Coq source file]
[Video]

Week 11 (May 6 & 8)

Topics

Dependent inductive types

Course materials

Clément’s transcript

Deadlines

May 8: Project check-in with staff

Week 12 (May 13 & 15)

Topics

Separation logic
Proofs by reflection

Course materials

Aurèle’s transcript?
Clément’s transcript

Week 13 (May 20 & 22)

Topics

Real-world Rocq: Regular expressions, Orthologic

Week 14 (May 27 & 29)

No lab session on May 29 (federal holiday!)

Deadlines

May 27 & 30: project presentations
June 13: final report due