The Coq mailing list

[Konrad Slind <slind AT cs.utah.edu>]

In HOL quotients are used

  * to construct the rationals and integers (using John Harrison's package)
  * to construct bitstring theories (Anthony Fox has some nice notes on 
this)
  * for alpha-equivalence in theories of syntax with binding.
      Peter Homeier has written some papers on this (and had developed a
      package of his own).

Konrad.

 

Lawrence Paulson wrote:

> 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
>
>
>
> -------------------------------------------------------
> This SF.Net email is sponsored by: IBM Linux Tutorials
> Free Linux tutorial presented by Daniel Robbins, President and CEO of
> GenToo technologies. Learn everything from fundamentals to system
> administration.http://ads.osdn.com/?ad_id=1470&alloc_id=3638&op=click
> _______________________________________________
> hol-info mailing list
> hol-info AT lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info