Lecture Notes, Week 02

• Functional programming with accumulators
  • Resources
  • Visualizing calls and returns
  • Analysis
  • A more complicated case: the factorial function
  • Exercise 01
  • Exercise 02
  • Binary trees of natural numbers revisited
  • Interlude – binary trees of natural numbers re2visited
  • Exercise 03
  • Postlude – continuations
  • Resources
  • Version
• Polymorphism in Gallina
  • Resources
  • Etymology
  • Polymorphism in Gallina
  • Polymorphic functions in Gallina
  • Polymorphic data types in Gallina
  • Exercise 04
  • Structural equality of polymorphic binary trees
  • Interlude
  • Exercise 05
  • Interlude (continued)
  • Polymorphism at work
  • Exercise 06
  • The polymorphic option type
  • Exercise 07
  • Partial solution for Exercise 07
  • Exercise 08
  • Exercise 09
  • Implicit parameters and the option type
  • Resources
  • Version
• Writing logical statements with the Coq Proof Assistant
  • Goal
  • Resources
  • TCPA: a domain-specific language for writing logical statements
  • Interlude
  • Interlude, continued
  • Exercise 10
  • Solution for Exercise 10
  • Exercise 11
  • Syntactic sugar
  • Interlude
  • Food for thought
  • The tCPA libraries and their searching facility
  • Postlude
  • Exercise 12
  • Exercise 13
  • Resources
  • Version
• Exercises for Week 02
  • Exercise 00
  • Mandatory exercises
  • Optional exercises
  • Exercise for the overachievers
  • Version
• Index of concepts for Week 02
  • Version