Praktische Semantik von Programmiersprache (SoSe 2013)

Für eine Kursbeschreibung, siehe: Praktische Semantik von Programmiersprachen.

Erste Vorlesung: 17.04., 16:15

• If Coq is not included in your package manager, download it from here.
• You will need at least one front-end for Coq: either CoqIde (part of Coq distribution) or Proof General, an Emacs-based front-end.

This is the online book we follow during the course. Up-to-date versions of the chapters will be posted here as we cover them.

1. Preface
2. Functional programming in Coq
3. Proof by induction
4. Working with structured data
5. Polymorphism and higher-order functions
6. More About Coq
7. Propositions and evidence
8. More propositions and evidence
9. Logic in Coq
10. More on induction
11. Simple imperative programs
12. Optional material! Parser for Imp (see also Coq code)
13. Optional material! Evaluation function for Imp (see also Coq code)
14. Program equivalence
15. Hoare logic, part 1
16. Hoare logic, part 2
17. Small-step operational semantics
18. More automation
19. Simply typed lambda calculus
20. Properties of simply typed lambda calculus
21. Optional material we did not manage to cover, ordered by chapter dependencies: More on STLC → A type checker for STLC → Typing mutable references → Subtyping → Adding records to STLC → Subtyping with references → Postscript

• 29.4: Basics.v, Induction.v, Lists.v.
• 8.5: Poly.v, MoreCoq.v
• 15.5: FinishingMoreCoq.v Prop.v
• 22.5: Logic.v
• 29.5: PropRelInd.v, SfLib.v, AutEval.v
• 5.6: Imp.v (corrected on June 16: error-generating use of notation in the definition of ceval)
• 12.6: Equiv.v
• 19.6: Hoare.v
• 26.6: Hoare2.v
• 03.7: Smallstep.v
• 10.7: Auto.v, Types.v, Stlc.v
• 17.7: StlcProp.v

1. Warm-up. (pdf)
2. The second sheet (posted Apr 29, deadline May 8, submissions by email to Tadeusz). (coq script)
3. Third assignment (posted May 10, deadline May 15, submissions by email to Daniel). (coq script)
4. Fourth assignment (posted May 20, deadline May 24, submissions by email to Tadeusz). Coq version HTML version
5. Fifth assignment (posted May 27, deadline June 2, submissions by email to Tadeusz). Coq version HTML version
6. Sixth assignment (posted June 2, deadline June 9, submissions by email to Tadeusz). Coq version HTML version
7. Seventh assignment (posted June 6, deadline June 15, submissions by email to Daniel). (Coq script)
8. Eight assignment (posted June 16, deadline June 30, submissions by email to Tadeusz). Coq script HTML file
9. Ninth assignment (posted June 23, deadline July 3, submissions by email to Daniel). (Coq script)
10. Tenth assignment (posted July 1, deadline July 11, submissions by email to Daniel). (Coq script)
11. Eleventh assignment (posted July 8, a hint added July 12, deadline July 18, submissions by email to Tadeusz). Coq script HTML file
12. Twelfth assignment (posted July 12, deadline July 21, submissions by email to Tadeusz). Coq script HTML file