Saarland University Computer Science

Semantics Derek Dreyer and Gert Smolka


Lecture Notes and Coq Developments 

  1. Compiling arithmetic expressions (Coq)
  2. Small-step and big-step semantics of abstract Imp (Coq)
  3. Small-step evaluation of abstract expressions (Coq)
  4. Call-by-value lambda calculus (Coq)
  5. Confluence (Coq1Coq2)
  6. From L to Lambda-Beta
  7. Substitution (Coq)
  8. Untyped lambda calculus (from 2015)
  9. Paper on call-by-value lambda calculus as a model of computation (ITP 2017)
  10. Semantics of Type Systems

You may also check the material of previous editions of this course (2015/16 edition).


  • Coq Home Page (download system here, we are using version 8.7)
  • There are two user interfaces for Coq: CoqIDE and Proof General. You can choose which one you want to use.
    • CoqIDE: You can download and install CoqIDE along with the rest of Coq from the Coq Home Page. Documentation about CoqIDE can be found here.
    • Proof General: Proof General is an emacs mode that supports many theorem provers, including Coq. You can download Proof General from this link. Using Proof General, Company Coq is an extension allowing you to look up lemmas and the Coq Documentation.
  • Coq Documentation