Over deze cursus
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)
Leerresultaten
- 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.
Voorkennis
2IT60 Logic and set theory
Bronnen
- Introduction to Type Theory - pdf file available through the webpage
- The book Type Theory and Formal Proof -- An Introduction (Rob Nederpelt and Herman Geuvers, Cambridge University Press, November 2014)
- The slides of the cours - pdf file available through the webpage
Aanvullende informatie
- Meer infoCursuspagina op de website van Eindhoven University of Technology
- Neem contact op met een coordinator
- StudiepuntenECTS 5
- Niveaumaster
Als er nog iets onduidelijk is, kijk even naar de FAQ van TU Eindhoven.
Aanbod
Dit aanbod is voor studenten van Utrecht University