Updates
- 19 Apr 2024:
added the live-proving session from today’s lecture
in Chapter A continuation-based interpreter
in Week 13
- 14 Apr 2024:
added Chapter Curry and uncurry
in Week 12
- 14 Apr 2024:
added two interludes in Chapter Polymorphism in Gallina
in Week 01
- 14 Apr 2024:
split Chapter Life after the midterm project into two
and created Chapter Functional equality
in Week 07
- 12 Apr 2024:
added the term project
- 12 Apr 2024:
added the material for Week 13
- 12 Apr 2024:
added the material for Week 12
- 05 Apr 2024:
added the material for Week 11
- 04 Apr 2024:
added the material for Week 10
- 28 Mar 2024:
added a section about the unit type in Chapter Induction and induction proofs: a recapitulation
in Week 05
- 24 Mar 2024:
added the exercises for Week 09
- 22 Mar 2024:
added the material for Week 09
- 21 Mar 2024:
extracted Chapter Two more goodies to go
out of Chapter Structuring programs, structuring proofs,
and expanded Chapter Structuring programs, structuring proofs
in Week 05
- 21 Mar 2024:
added a postlude about vacuous specifications
and two exercises
in Chapter The exists tactic, revisited
in Week 06
- 21 Mar 2024:
split the chapter about miscellanies into two
(Chapter About unfolding calls and Chapter The exists tactic, revisited)
in Week 06
- 21 Mar 2024:
added Exercise 02
in Week 08
- 15 Mar 2024:
added the live-proving session from today’s lecture
in Chapter More tactics
in Week 08
- 15 Mar 2024:
added the material for Week 08
- 08 Mar 2024:
added the material for Week 07
- 22 Feb 2024:
added the midterm project
- 22 Feb 2024:
added the material for Week 06
- 16 Feb 2024:
added the material for Week 05
- 14 Feb 2024:
added an executive summary about when to use the induction tactic
in Chapter Reasoning equationally about recursive functions using fold-unfold lemmas
in Week 04
- 09 Feb 2024:
added the songbook
- 09 Feb 2024:
added the material for Week 04
- 06 Feb 2024:
added the executive summary
after Halcyon’s dream
in Chapter Specifications
in Week 03
- 03 Feb 2024:
added the exercises for Week 03
- 02 Feb 2024:
added the live-proving sessions from today’s lecture
in Chapter Specifications
in Week 03
- 02 Feb 2024:
added most of the material for Week 03
- 30 Jan 2024:
added a hint for the exercise about types
in Week 02
- 30 Jan 2024:
pointed out that when solving Exercise 05 in Week 02,
all the arguments should be supplied to all the lemmas that are applied
- 28 Jan 2024:
added hints for
Exercise 15,
Exercise 16,
and
Exercise 17
in Chapter Proving logical properties with the Coq Proof Assistant
in Week 02
- 28 Jan 2024:
added Section Using the revert tactic with several arguments
in Chapter The revert tactic
in Week 02
- 27 Jan 2024:
added the exercises for Week 02
- 26 Jan 2024:
fixed a typo in the specifications of the addition function
in Chapter Formalizing a proof with the Coq Proof Assistant
in Week 02
- 25 Jan 2024:
added most of the material for Week 02
- 25 Jan 2024:
added a warning about submitting handins as a group, not as an individual, on Canvas
in the Exercises for Week 01
- 21 Jan 2024:
rewrote the Interlude about implementing a function that returns the smallest of two natural numbers
in Chapter Exercises for Week 01
in Week 01
- 20 Jan 2024:
added the exercises for Week 01
- 20 Jan 2024:
added a partial solution for Exercise 01
in Chapter Functional programming in Gallina
in Week 01;
this partial solution contains more explanations about lambda-lifting and lambda-dropping
- 19 Jan 2024:
fixed a couple of typos
and
added the live-coding session from today’s lecture
in Chapter Functional programming in Gallina
in Week 01
- 19 Jan 2024:
added a section about generative AI
and a postlude
in Chapter The events leading to the term project and the oral exams
in Week 01
- 19 Jan 2024:
polished Chapter Functional programming in Gallina
and its accompanying .v file
in Week 01
- 18 Jan 2024:
added most of the material for Week 01
- 15 Jan 2024:
created