eduXchange.nl
The new minor offering from Leiden, Delft and Erasmus will be visible in early March.

Proving with computer assistanceOrganization logo: Eindhoven University of Technology

About this course

​​​​​​

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, dependemtly 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 typing algorithm of Hindley-Milner.
  • The Curry-Howard isomorphism (or 'formulas-as-types' interpretation).
  • Translation of logical propositions in first and higher order logic to a type system.
  • Natural Deduction proofs with the proof assistant Coq.
  • The formalization of a problem in computer science (the correctness of an algorithm) in the proof assistant Coq. (Project)

Learning outcomes

  • 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 Coq. The proof assistant Coq will be studied and used for a formalization project.

Prior knowledge

2IT60 Logic and set theory

If anything remains unclear, please check the FAQ of TU Eindhoven.

Offering(s)

  • Start date

    5 februari 2024

    • Ends
      7 april 2024
    • Term *
      Block GS3
    • Location
      Eindhoven
    • Instruction language
      English
    • Register between
      15 Nov, 00:00 - 7 Jan 2024
    Enrolment period closed
These offerings are valid for students of Utrecht University