Updates
- 11 Jul 2025:
added two tasks
in the mini project about summations that may start above zero
- 08 Jul 2025:
expanded the prelude with a concrete example
in Chapter Integers
in Week 10
- 08 Jul 2025:
added a mini project about yet another mystery function
- 08 Jul 2025:
completed Chapter Induction principles: strong induction
in Week 11
- 03 Jul 2025:
completed Chapter Induction principles: course-of-values induction
in Week 11
- 30 Jun 2025:
aligned the narrative with the resource file more precisely
in the mini project about summations that may start above zero
- 29 Jun 2025:
added a prelude, an interlude, and an executive summary
in Chapter Integers
in Week 10
- 27 Jun 2025:
added Section Divisibility of polynomials
in Chapter Integers
in Week 10
- 22 Jun 2025:
added Section Two identities about absolute values
in Chapter Integers
in Week 10
- 15 Jun 2025:
added a mini project about summations that may start above zero
- 15 Jun 2025:
added an exercise in Binomial coefficients
in Week 08
- 08 Jun 2025:
added a chapter about integers
in Week 10
- 06 Jun 2025:
added a section about the repeat tactic
in Chapter More tactics
in Week 10
- 06 Jun 2025:
added an interlude
in Chapter Ex falso quodlibet
in Week 10
- 06 Jun 2025:
added an exercise
in Chapter More about soundness and completeness
in Week 05
- 05 Jun 2025:
created Chapter Existential declarations, revisited
in Week 07
- 05 Jun 2025:
created Chapter The problem with substracting natural numbers
in Week 10
- 05 Jun 2025:
added exercises in Chapter Reasoning equationally about recursive functions using fold-unfold lemmas
in Week 05
- 05 Jun 2025:
added a dedicated chapter about the ring tactic
- 05 Jun 2025:
added a dedicated chapter about formalizing two-by-two matrices
- 05 Jun 2025:
added a dedicated chapter about formalizing summations
- 04 Jun 2025:
added a mini project about fourth-order induction
- 23 May 2025:
added
a partial solution for Exercise 23
in Chapter A simple problem in Week 07
and
three new exercices as well as a postlude
in Chapter Induction principles: from first-order to higher-order induction in Week 11
- 22 May 2025:
wrote a proper description of the term project
in Chapter Three program processors for arithmetic expressions
- 21 May 2025:
created Chapter Arithmetic expressions with names
as a foundation for Chapter Observational equivalence
in Week 12
- 20 May 2025:
expanded Chapter The case of proofs by cases
in Week 09
- 19 May 2025:
expanded Chapter Proving logical properties with the Coq Proof Assistant
in Week 03
- 20 Apr 2025:
expanded the .v file about formalizing summations
with the content of the oral-exam questions for Audi Prasanto and Sim Ray En Ryan
and
added Towards a solution for Exercise 03
in Chapter Formalizing summations
in Week 10
- 14 Apr 2025:
finalized the term project with more precise types
- 12 Apr 2025:
added a couple of solutions as well as a postlude
in Chapter Observational equivalence
in Week 12
- 11 Apr 2025:
added the live-proving session that took place at the lecture
in Chapter Observational equivalence
in Week 12
- 11 Apr 2025:
added the material for Week 12
- 11 Apr 2025:
added the term project
- 09 Apr 2025:
completed the chapter about Demand-driven computation
and added a chapter about Programming with streams
in Week 11
- 04 Apr 2025:
added a chapter about A Fibonacci structure
in Week 10
- 04 Apr 2025:
added the material for Week 11
- 31 Mar 2025:
added a chapter about Binomial coefficients
in Week 08
- 30 Mar 2025:
added
Section The ring tactic,
an interlude,
and
Section A perspicuous use of the injection tactic
in Chapter More tactics
in Week 10
- 30 Mar 2025:
detailed the solution for
Exercise 01
some more
in Chapter More tactics
in Week 10
- 24 Mar 2025:
clarified the statement of Exercise 06
in Chapter The Euclidean division
in Week 08
- 23 Mar 2025:
fine-tuned
Exercise 02,
Exercise 04,
and
Exercise 06,
provided solutions for
Exercise 02.a,
Exercise 02.b,
and
Exercise 02.c,
and added a postlude
in Chapter In the wake of the midterm project
in Week 09
- 22 Mar 2025:
added the exercises
for Week 09
- 22 Mar 2025:
added Chapter In the wake of the midterm project
in Week 09
- 21 Mar 2025:
expanded the statement of Exercise 33
in Chapter A simple problem
in Week 07,
in an attempt to clarify it
- 21 Mar 2025:
added the .v file about isometries and proofs by cases after the live-proving session
during the last part of the lecture
- 21 Mar 2025:
added the material for Week 09 (minus the exercises)
- 13 Mar 2025:
added the material for Week 08
- 07 Mar 2025:
added a note about Bloom et al.’s hierarchical taxonomy of
student-learning objectives in LPP this semester
- 07 Mar 2025:
changed all occurrences of “to destructure” into “to deconstruct”
- 07 Mar 2025:
added Section Rewriting in all the assumptions
and Section Rewriting both in the goal and in all the assumptions
in Chapter The rewrite tactic
in Week 04
- 07 Mar 2025:
added the material for Week 07
- 22 Feb 2025:
completed Section Help! My recursive function doesn’t espouse my inductive data type!
in Chapter Structuring programs, structuring proofs
in Week 06
- 21 Feb 2025:
added the midterm project
- 21 Feb 2025:
added most of the material for Week 06
- 16 Feb 2025:
reformatted the unit-test functions uniformly in the resource files
in Weeks 01, 02, and 05 by adding an initial (and redundant) true conjunct
- 16 Feb 2025:
fixed a typo in the opening sentence of Exercise 23
in Week 05
- 16 Feb 2025:
added Chapter The clear tactic
in Week 05 (the lecture notes for Week 05 are now complete)
- 15 Feb 2025:
added Chapter Three properties of the Leibniz equality
in Week 05
- 15 Feb 2025:
added Section The Coq Proof Assistant in essence
in Chapter Warmup
in Week 04
- 14 Feb 2025:
nearly completed the material for Week 05
(Chapters Three properties of the Leibniz equality
and The clear tactic are still missing,
and so is the live-proving session from today’s lecture)
- 14 Feb 2025:
streamlined the names of the addition and multiplication functions
in Chapter Reasoning equationally about accumulator-based recursive functions
in Week 05
- 14 Feb 2025:
added missing definitions (?!?)
in the .v file of Chapter Specifications that depend on other specifications
and aligned the content of Chapter Specifications that depend on other specifications
accordingly
in Week 05
- 14 Feb 2025:
added most of the material for Week 05
- 10 Feb 2025:
added Exercise 11.m
and Exercise 11.n
in Week 04
- 08 Feb 2025:
added Exercise 11 from Week 02
in Week 04
- 07 Feb 2025:
completed the material for Week 04
and added the exercises
- 07 Feb 2025:
added most of the material for Week 04
- 04 Feb 2025:
tuned the end of the interlude about formalizing informal specifications
and added the continuation of this interlude
in Chapter Writing logical statements with the Coq Proof Assistant
in Week 02
- 02 Feb 2025:
added a section about a practical use of the Check command
in Chapter Functional programming in Gallina
in Week 01
and a section about the polymorphic option type
in Chapter Polymorphism in Gallina
in Week 02,
to illustrate how to exhibit an expression of a given type
- 02 Feb 2025:
added a postlude about equivalent statements
in Chapter Proving logical properties with the Coq Proof Assistant
in Week 03
- 02 Feb 2025:
added the optional exercises
in Week 03
- 02 Feb 2025:
added the solution for Exercise 03,
Exercise 04, and
Exercise 05
in Chapter Formalizing a proof with the Coq Proof Assistant
in Week 03
- 31 Jan 2025:
completed the material for Week 03
and added most of the exercises
- 31 Jan 2025:
added most of the material for Week 03
- 31 Jan 2025:
renamed the chapter about writing logical statements with tCPA
in Week 02
- 26 Jan 2025:
added an exercise for the overachievers
in Week 02
- 26 Jan 2025:
added a postlude about the food for thought in Week 01
in the chapter about writing logical statements with tCPA
in Week 02
- 25 Jan 2025:
expanded the exchange about the induction step in the interlude
about the equality predicate for polymorphic binary trees
(because sometimes, it pays off to be pedantic)
in the chapter about polymorphism
in Week 02
- 25 Jan 2025:
added explanations about copy_nat_alt and power_alt
in the analysis of what happens at call time and at return time
in the chapter about accumulators
in Week 02
- 25 Jan 2025:
added the exercises for Week 02
- 24 Jan 2025:
renamed the constructors of binary_tree_nat
in the chapter about accumulators
in Week 02
- 24 Jan 2025:
added most of the material for Week 02
- 19 Jan 2025:
added a section about declarations
in the chapter about functional programming in Gallina
in Week 01
- 18 Jan 2025:
expanded the first section about binary trees
in the chapter about functional programming in Gallina
to align it with the section about Peano numbers
in Week 01
- 17 Jan 2025:
added the exercises for Week 01
- 17 Jan 2025:
removed the chapter about polymorphism
and
simplified the chapter about functional programming in Gallina
in Week 01
- 17 Jan 2025:
fleshed out
the chapter about soundness and completeness
and
the chapter about functional programming in Gallina
in Week 01
- 14 Jan 2025:
added most of the material for Week 01
- 14 Jan 2025:
created