Functional Algorithms Ch. 1

By popular demand, we're working on a new cycle of Software Foundations (https://softwarefoundations.cis.upenn.edu/current/index.html).

Let's do the Coq exercises for chapter 1 of Part 3: Functional Algorithms, and discuss.

The Coq proof assistant is central to the whole ecosystem for verified software that is being developed under the NSF Deep Specification initiative. Software Foundations is an online text in principles of verified software from a type-theoretic point of view, emphasizing hands-on work with Coq.

Both classrooms we have used may still be busy, so let's meet by the main checkout desk of the library, a couple of doors further into the campus from the Bannan Engineering building where we met before.

The university has apparently tightened parking enforcement. If you arrive after 6 p.m., a free 2-hour visitor parking permit should be enough, but it is required to have one for any time before 8 p.m.