Seminar: Software Foundations

SupervisionProf. Dr. Peter Thiemann
Time and PlaceSR 00-019, Geb. 079 Wednesdays, 14:00 -- 16:00
AssistantLuminous Fennell


This seminar is based on the interactive self-study course Software Foundations (SF) of Benjamin Pierce et al. The participants will explore the theoretical foundations of software and programming languages through formal modelling and interactive theorem proving using the Coq proof assistant.


Each participant will present a selected chapter from the SF course. The time table lists chapters, dates and presenters.

In addition to the presentation each participant has to prepare a written summary of the presented chapter, to be submitted two weeks after the presentation date. The summary should be written in LaTeX using the llncs style and should not exceed 10 pages.

Also, each participant should submit an index of the novel concepts introduced in his chapter. See the index section.


The final grade will combine the grades for the moderator presentation (40%), the written summary (40%), and overall participation (20%).


No specific previous knowledge of the topic is required, as the course introduces all necessary concepts. However, participants should have taken some basic logic (or logic-related) course in the past, and should have some interest in logic, formal methods, programming languages or related topics.

The required software should be installable on all major operating systems. Also, a VM image will be provided and there is the possibility to use the Proglang-Pool (079-00-018) for participants without a laptop.

Time Table

Presentation DateSelected ChaptersModerator
2014-10-29Preface, BasicsLuminous Fennell
2014-11-19LogicDavid S.
2014-12-03PropHannes S.
2014-12-17Equiv, HoareViktor B., David Z.
2015-01-14STLCJannis L.
2015-01-21 time: 12:30!Types Nico H.
2015-01-28STLCPropJulian J.

Index of concepts and tactics

To index a chapter, insert anchors in the Coq source file using the following syntax:

(** #<a name="anchor_id"/># *)

Replace "anchor_id" with a unique name. Then create a CSV file with the basename as the chapter and two columns (see Basics.txt for an example). The first column should contain the terms you would like to index and the second the names of the corresponding anchor you inserted in the Coq source file. Then send the modified Coq source and the CSV file to Luminous Fennell.

  • Current index (includes: Basics, Logic, Prop, Imp, Hoare) online, zip, tar.gz (open www/sf/sf-index.html in your browser after unpacking)
  • Basics.txt (example for csv format)
  • Basics.v (example for anchors)