Set-theoretical mathematics in Coq
Simpson, Carlos
HAL, hal-00118006 / Harvested from HAL
Text on HAL
We give a brief discussion of some of the issues which have arisen in the course of formalizing some classical set-theoretical mathematics in the Coq system. This sprouts from, expands and replaces a chapter of math.HO/0311260 which will be removed in revision, and also contains as a tar-attachment to the source file the revised and expanded version of the proof development which had been attached to math.HO/0311260.
Publié le : 2004-07-05
Classification:  [MATH.MATH-LO]Mathematics [math]/Logic [math.LO] 
@article{hal-00118006,
     author = {Simpson, Carlos},
     title = {Set-theoretical mathematics in Coq},
     journal = {HAL},
     volume = {2004},
     number = {0},
     year = {2004},
     language = {en},
     url = {http://dml.mathdoc.fr/item/hal-00118006}
}

Simpson, Carlos. Set-theoretical mathematics in Coq. HAL, Tome 2004 (2004) no. 0, . http://gdmltest.u-ga.fr/item/hal-00118006/