Chalmers course on Semantics in Calculus of Constructions

Hard exercise: Copy syntax.v, little.v, and axiom.v into syntax2.v little2.v and axiom2.v remove all

Prove the associativity of sequences, this time using denotational semantics. Example ex4 : forall r

To set up your working environment, you need to have coq-8.1 running on your machine. The development

Sorry, it seems that google has not solved the problem on how to embed a google calendar page in a

I added information about what keen students may want to read to have an easier task during the