The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

I am late in this discussion, but I have been programming language 
semantics for 6 to 7 years
now, and I have been integrating courses in Coq progressively over the 
last 3 years.

To make things tractable I initially only work with Winskel's first 
chapters, and I even removed
the "if-then-else" construct from the language.  I obtained the 
responsibility for two modules.

First module

- An introduction to pure lambda-calculus,
- An introduction to typed lambda-calculus,
- Natural semantics (i.e. big-step operational semantics),
- Denotational semantics (CPOs, Tarski-Fixpoint theorem),
- Axiomatic semantics (both Hoare logic and Dijkstra's weakest 
pre-condition calculus).

Second module

I am unlucky that the students who come for the second module often have 
not attended the
first module, so I usually re-do the introduction to natural semantics.  
I then add the following things:

- Structural Operational Semantics (small-step),
- Proof of equivalence between Natural (big-step) operational semantics 
and SOS,
- Axiomatic semantics (proof of soundness wrt. natural semantics),
- Introduction to abstract interpretation : I show how to encode a small 
abstract interpreter
 for intervals on the language of while loops.

============================
This year I also taught a course at Chalmers, where everything was 
concentrated on week.  3 hours
of lectures in the morning and 3 hours of lab sessions in the afternoon: 
every student had to have
their own computer with Coq running and I brought the basic data.  We 
happened to organize
this course on a week with a day off, so that there were only four 
lectures and four lab sessions.

For this course the content was:

- first day: natural semantics (big step) and structural operational 
semantics (small step), and a functional
implementation of the latter.  the structural operational semantics and 
the functional implementation
were proved correct in Coq: this yields a little interpreter that you 
can run inside Coq (you can repeat
small steps for some amount of times).  This shows how to do proofs by 
induction with respect to
inductive data structures (arithmetic expressions and instructions) and 
inductive properties (the
natural semantics relation).

- second day: denotational semantics and CPOs, this yields an 
interpreter based on classical axioms,
which you can extract to obtain a interpreter for the language (with no 
guarantee of termination).
Extraction is based on associating a computational content to Tarski's 
fixpoint theorem (an idea I
still want to describe in a publication).  The denotation semantics is 
proved correct with respect to
the natural semantics: it shows how to perform proofs by induction with 
respect to Tarski's least
fixpoint theorem in complete partial orders with a minimal element.

- third day: axiomatic semantics and Dijkstra verification condition 
generation.  This yields a miniature
 why tool, which you can run inside Coq to prove properties of programs 
(using reflection).  The main
 aspects of the proof are
  i) to show how to perform a "hybrid" embedding of assertions in the 
programming
     language, so that assertions can be considered as first-order 
data, but are easily interpreted as regular
     propositions of the Coq meta-language,
  ii) to show how to avoid double inductions by replacing an inductive 
property with non-structural
      rules (like Hoare logic, which contains a consequence rule) with 
an inductive property with
      only structural rules.  This issue also appears when you describe 
a type system for sub-typing and
     the "sub-typing" rule can be used freely.

- fourth day: abstract interpretation on interval values (no lab 
session: I left early in the afternoon).
 For this course, I spend most of the time describing the structure of 
the abstract interpreter, and have
 only a little time left to browse the formal proofs.  The correctness 
proof relies on the verification
 condition generator that is defined on the previous day.

=============
For all these courses, the main problem is to make sure the students 
know enough of Coq quickly enough
to perform experiments on the machine.  I believe you can perform the 
first proofs (especially equivalence
between natural and operational semantics) knowing only 12 tactics:

intros, elim, discriminate, injection, inversion, apply, assert (H : 
...), assert (H := ...), simpl, fold,
replace, rewrite

but in fact, I also frequently use the derived tactics case, induction, 
destruct, case_eq, subst,
whose behavior can be taught in a few words from elim and rewrite.

Because my language describes arithmetic operations I also need to 
perform proofs about
integer arithmetics and comparisons, for which I use ring and omega.

Students also need to understand that a universally quantified theorem 
can be used as a function,
and this usage yields an instantiation of the universally quantified 
variable.

To give students material without making them read the whole Coq'Art, I 
wrote down a 20 page
introduction to Coq (without the theory), which I called "Coq in a 
Hurry".  I have been trying
to introduce students to Coq using this 20 page introduction over the 
last two years, I am not completely
satisfied with it because I usually have only a 3 hour session, while 
the material covered in the
notes actually should performed in a lab session, with instructor 
supervision for at least 6 hours.

===============
The exercises I have given to students are the following:

- Show the provability of the execution statement for a small ground 
program (requires applying the
 constructors of the inductive definition),
- Prove that the sequence construct of the imperative programming 
language is associative (requires
 inversion),
- Show that if some while loop programs terminate, then the final state 
has some property (requires
 a proof by induction on derivations).  Example:
 prove that if one executes "while x < 10 do x := x+3 done" then the 
initial and final values of
 the variable "x" are separated by a multiple of 3.
- Prove that  "while b do i1;i2 done" can be replaced with "i1; while b 
do i2;i1 done; i2" under some
 conditions on the input environment.
- Redo the second and third exercises using denotational semantics,
- Redo the third exercise using the verification condition generator,
- Add a conditional statement to the language, adapt the natural, sos, 
axiomatic semantics to the change
 and redo the proof.

To make students play with the language, I also provide a parser that 
can be executed in Coq.  In its
current version, this parser is rather slow (it relies on nat addition, 
multiplication, and comparison
to detect regular characters, digits, and the like), but then students 
can play with it and I hope they
get the feeling that all this can be useful.  I also provide a parser in 
ocaml and a few encapsulation
functions, so that the extracted code from the denotational semantics, 
the verification condition
generator, and the abstract interpreter can also be run on sample 
programs outside Coq.

All this material (except the slides) is available from a google group 
that was created for the course in
Chalmers: the name of the group is
"Chalmers course on Semantics in Calculus of Constructions"

I will probably put this data in the Coq contribution and on my on web 
page, but I am still adding
improvements (for instance I am currently re-designing my abstract 
interpreter to have a better
separation between the generic part and the description of the abstract 
domain of intervals).

I will be happy to share ideas around this,

Yves