Teaching

• March 2013: Spring school on formal methods in software engineering (IAMI, Ho Chi Minh City, Vietnam)
  • Elements of mathematics and logic for computer program analysis
  • Introduction to the OCaml programming language
  • Introduction to the Coq proof assistant

• May 2012: Introduction to domain theory and topology (ISCAS, Beijing, China)

• August 2010: 2nd Asian-Pacific Summer School on Formal Methods (Beijing, China)
  • Type checking and type inference in the simply-typed lambda-calculus
  • Termination of beta-reduction in the simply-typed lambda-calculus

• August 2009: 1st Asian-Pacific Summer School on Formal Methods (Beijing, China)

• March 2009: Lectures on the meta-theory of System F (Tsinghua University, Beijing, China)

• October 2008 - February 2009: Lectures on Coq (Tsinghua University, Beijing, China)

• March 2008: Introduction to typed lambda-calculus and logic (Tsinghua University, Beijing, China)