There is a free book "Certified Programming with Dependent Types" about COQ available at: http://adam.chlipala.net/cpdt/cpdt.pdf
Tim _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer