Syllabus
We will mostly follow the Hitchhiker's Guide:
Basics:
- Definitions and Statements,
- Backward Proofs, Forward Proofs
(Quantifiers, Connectives, Tactics, Propositions as Types / Proofs as Terms)
Functional–Logic Programming:
- Functional Programming
- Inductive Predicates
- Monads
(Basic Data Structures, Proofs by induction, Arithmetic tactics)
Program Semantics:
- Operational Semantics
- Hoare Logic
- Denotational Semantics
(Small-step/big-step, Partial vs Total correctness, Monotone functions, lattices and fixpoints)
Mathematics:
- Logical Foundations of Mathematics
- Basic Mathematical Structures
- Rationals and Real Numbers
(Foundational principles, Subtypes, Quotient types, Type Classes)
Annotation
The topic of the course are formal (computer-understandable) mathematics and proof assistants (interactive theorem provers). A proof assistent is a tool to assist with the development of formal proofs by human-machine collaboration.
The language of communication is some variant of formal logic and the main aim a high level of assurance that the proven actually holds.We will have a look at the proof assistent Lean, study its theoretical foundations and explore the ways in which it can be used to develop theories, model systems, and prove theorems in computer science.