Proving with Computer Assistance

URL study guide

Description

Please note that the the lecture is not completely in slot A. The lectures are scheduled on Thursdays hours 3+4 and 5+6

• Type systems, especially simply typed, dependently typed, polymorphically typed and higher order typed lambda calculi.
• Type systems in programming languages: implicit/explicit typing, polymorphic types, inductive and abstract data types; the prinicipal types algorithm of Hindley-Milner.
• The Curry-Howard isomorphism (or 'formulas-as-types' , “proofs-as-terms”  interpretation).
• Translation of logical propositions in first and higher order logic to a type system.
• Natural Deduction proofs with the proof assistant Rocq.
• The formalization of a problem in computer science (the correctness of an algorithm) in the proof assistant Rocq. (Project)

Objectives

• The primary goal is to understand interactive theorem provers ("proof assistants"), and to learn how to use a proof assistant to formalize a program and to verify its correctness to the currently highest possible degree.
• The secondary goal is to understand type systems, from the point of view of (functional) programming and from the point of view of logic, following the Curry-Howard interpretation of "formulas-as-types".
  Combining these two viewpoints, type theory forms the theoretical basis for the proof assistant Rocq. The proof assistant Rocq will be studied and used for a formalization project.

Method of Assessment