The Coq mailing list

[Randy Pollack <rap AT inf.ed.ac.uk>]

In our Coq constructive proof of the fundamental theorem of algebra we
use setoids for quotienting.

@Article{algHier02,
  author =       {H. Geuvers and R. Pollack and F. Wiedijk and J. Zwanenburg},
  title =        {A Constructive Algebraic Hierarchy in {C}oq},
  journal =      "Journal of Symbolic Computation",
  year =         2002,
  volume =       34,
  number =       4,
  pages =        {271--286},
  note = {Special Issue on the Integration of Automated Reasoning 
          and Computer Algebra Systems}
}

The library of algebraic structures developed for this project has
been considerably improved and developed by people at Nijmegen.  See
http://www.cs.kun.nl/fnds/ccorn.

Randy
--
Lawrence Paulson writes:
 > How frequently are quotient constructions used in formal proofs? I 
 > think John Harrison used one to construct the rationals, and there are 
 > a couple in Isabelle, but are there others? Also, are there any 
 > publications describing such proofs?
 > 
 > Larry Paulson
 > 
 > 
 > --------
 > Send messages to 
 > isabelle-users AT cl.cam.ac.uk
 > Conference announcements should be relevant and brief