Seminar: Software Foundations
| Supervision | Prof. Dr. Peter Thiemann | |
| Time and Place | SR 00-019, Geb. 079 | Wednesdays, 14:00 -- 16:00 |
| Assistant | Luminous Fennell |
Description
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.
Execution
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.
Examination
The final grade will combine the grades for the moderator presentation (40%), the written summary (40%), and overall participation (20%).
Prerequisites
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 Date | Selected Chapters | Moderator |
|---|---|---|
| 2014-10-29 | Preface, Basics | Luminous Fennell |
| 2014-11-05 | Q&A | N.A. |
| 2014-11-12 | N.A. | N.A. |
| 2014-11-19 | Logic | David S. |
| 2014-11-26 | N.A. | N.A. |
| 2014-12-03 | Prop | Hannes S. |
| 2014-12-10 | N.A. | N.A. |
| 2014-12-17 | Equiv, Hoare | Viktor B., David Z. |
| 2015-01-07 | N.A. | N.A. |
| 2015-01-14 | STLC | Jannis L. |
| 2015-01-21 time: 12:30! | Types | Nico H. |
| 2015-01-28 | STLCProp | Julian 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)
Material
- Software Foundations
- Overview of the chapters in Software Foundations
- Coq proof assistant (download, includes an IDE)
- Proof General, an alternative IDE for Coq (based on Emacs)