2016: Computer Aided Crypto Proodfs (10ETCS)
Homotopy type theory: Univalent Foundations of Mathematics
Course on Coq homotopy type theory library at CMU (2015)
of Logic Programming 2012.
of Logic Programming 2011.
of Logic Programming 2010.
thesis by Martin Devillers (2010)
Developed and taught two courses in the masterclass
Type theory and Proof Assistants (with
Constructivism and the continuum
Teaching assistant for:
Formal Thinking for information scientists. (with
statistics for biologists; numerical analysis; introduction to logic
(for mathematicians and computer scientists); differential equations;
introduction to logic (for mathematicians and computer scientists);
proof theory and set theory (for mathematicians and computer
scientists); discrete mathematics; introduction to mathematics.