CAS 763 / Certified Programming with Dependent Types

3 unit(s)

W. Kahl

Type systems featuring types depending on values empower not only logics that can capture common mathematical formalizations more naturally than conventional first-order or higher-order logics; they also empower programming languages where specifications may be incorporated into the type of programs, and well-typed programs are thus guaranteed to satisfy these specifications. Students will learn at least one dependently-typed programming language in depth. The course will also cover associated foundations, including relevant type theories and the Curry-Howard correspondence, as well as useful patterns of formalizing, programming, and proving in dependently-typed programming languages.