lucaspena / coinduction Goto Github PK

theory/
contains some developments about the foundations,
acceptable forms of decidable rules, higher order proofs, etc.

This is more than we need for the first round of examples,
where transitivity and step seem to be enough for derived rules,
and first order properties suffice.

common/
Define the proof principles specialized to transitivity,
and also a representation of map with an ACU equivalence
relation, and some lemmas on that

himp/
example proofs for imp-type language with heaps

stack/
forth-like stack based language

lambda/
lambda calculus, no named functions (de bruijn indices)

csl/
very simple imp language (adapted from Chlipala's FRAP text),
first concurrency examples; first examples with locks


all files compiled using Coq version 8.4