Lecture Notes, Week 01

• The events leading to the term project and the oral exams
  • Expectations
  • Template for the reports
  • On generative AI
  • Postlude
  • Version
• Introduction and motivation
  • Version
• Soundness and completeness
  • Version
• Functional programming in Gallina
  • Goal
  • Resources
  • Three windows
  • TCPA’s toplevel loop
  • The Check command
  • The Compute command
  • Example of inductive definition: natural numbers
  • Interlude
  • Decomposition of inductive data
  • Recursive definitions
  • Example of recursive definition: the addition function
  • Interlude
  • Exercise 01
  • Partial solution for Exercise 01: the multiplication function
  • Example of inductive definition: binary trees of natural numbers
  • Example of recursive definition: binary trees of natural numbers
  • Exercise 02
  • Exercise 03
  • Exercise 04
  • Associativity
  • Food for thought
  • Resources
  • Version
• Polymorphism in Gallina
  • Resources
  • Etymology
  • Polymorphism in Gallina
  • Polymorphic functions in Gallina
  • Polymorphic data types in Gallina
  • Exercise 05
  • Structural equality of polymorphic binary trees
  • Interlude
  • Exercise 06
  • Interlude (continued)
  • Polymorphism at work
  • Exercise 07
  • Exercise 08
  • Partial solution for Exercise 08
  • Exercise 09
  • Exercise 10
  • Implicit parameters and the option type
  • Resources
  • Version
• Exercises for Week 01
  • Exercise 00
  • Warmup
  • Mandatory exercises
  • Optional exercises
  • Exercise for the overachievers
  • Expectations
  • Food for thought
  • Interlude about adding one to the result of evaluating an expression
  • Interlude about subtracting one to the result of evaluating an expression
  • Interlude about defining the Fibonacci function
  • Interlude about implementing a function that returns the smallest of two natural numbers
  • Version
• Index of concepts for Week 01
  • Version