added description of files

README.md

 # SepLog
 
-An implementation of Separation Logic for a monadic language, while while loops defined usinf domain theory.
+An implementation of Separation Logic for a monadic language, while while loops defined using domain theory.
+
+Files:
+
+- ACPO.v, ADCPO.v, CPO.v, EXP.v, FunComp.v, Haddock.v, Ideal.v, Kleene.v, Option.v, Setof.v : domain-theoretical constructions. 
+
+- Monad.v : a combined termination, exception, and state monad.
+
+- Primitives.v : definition of the state of the monadic language and primitives instructions for reading/writing in the state.
+
+- While.v  : while loops for the monadic language, defined using the domain-theoretical constructions above.
+
+- BasicTriples.v : weakest-precondition Hoare triples for primitive instructions of the language.
+
+- SepTriples.v : building on BasicTriples.v, a reformulation of the  weakest-precondition triples with separation-logic assertions in pre/post conditions.
+
+- Hoare.v : Hoare rules the for monadic instructions and for while loops.
+
+- Pred.v :a predicate calculus on states of the monadic language.
+
+- Heap.v: a model of heaps, part of the state of the language.
+
+- GenAssertions : separation-logic assertions for a state consisting of a heap and a store.
+
+- StateAssertions.v : additional assertions for the case of a store consisting of two registers.
+
+- ListAssertions : additional assertions for single-linked lists.
+
+- Reverse.v : a program in the monadic language forin-place reversing a single-linked list.
+
+- ReverseObligations.v : proof obligations arising in the proof of the list-reversing program above.
+
+- ReverseProof.v : the proof of the list-reversing program in Separation Logic.
+
+