Software Verification

Catalog description

A course on programming languages and software verification, with hands-on exercise in an interactive theorem prover such as Coq. Topics may include, but are not limited to: logic; functional programming; inductive datatypes, recursion, and structural induction; operational, denotational, and axiomatic semantics; simply typed lambda calculus; polymorphic lambda calculus; type systems and type-checking.