Teaching
Our lab is responsible for two courses:
CS-214 — Software Construction (200-level, 8 credits)
Learn how to design and implement reliable, maintainable, and efficient software using a mix of programming skills (declarative style, higher-order functions, inductive types, parallelism) and fundamental software construction concepts (reusability, abstraction, encapsulation, composition, proofs). Jointly taught by Clément Pit-Claudel, Martin Odersky, and Viktor Kunčak.
Syllabus
Functional programming paradigm
Recursion and tail-recursion
Evaluation strategies, lazy evaluation, substitution model
Modularity, data abstraction, representation independence
Subtyping, inheritance, type classes
Polymorphism, variance
Structural induction
Stateless parallelism, map-reduce, associative operations
Effects: state, exceptions
Documentation, tests, specification
Interpreters and program semantics
Program transformation and program correctness
CS-428 — Interactive Theorem Proving (Graduate-level, 6 credits)
A hands-on introduction to interactive theorem proving, proofs as programs, dependent types, and to the Coq proof assistant. Jointly taught by Clément Pit-Claudel and Aurèle Barrière.
Syllabus
Intro to the Coq proof assistant (logic, higher-order functions, tactics)
Functional programming (inductive types and fixpoints)
Structural induction (data structures and verified algorithms)
Interpreter-based program semantics (intro to compiler verification)
Inductive relations (predicates, rule induction)
Automation and tactics I (bottom-up reasoning and logic programming)
Operational program semantics (small- and big-step semantics)
Program logics (hoare triples)
Automation and tactics II (top-down reasoning)
Type systems (Simply-typed lambda calculus)
Dependent types and equality proofs
Automation and tactics III (proofs by reflection)
Real-world interactive theorem proving (guest lecture)