LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
sav08:results_proved_in_hol [2008/05/28 03:51]
vkuncak
sav08:results_proved_in_hol [2009/03/05 11:58] (current)
vkuncak
Line 3: Line 3:
   * See textbook by Andrews for definitions of number theory in HOL   * See textbook by Andrews for definitions of number theory in HOL
   * [[http://​isabelle.in.tum.de/​library/​HOL/​index.html|Isabelle library]]   * [[http://​isabelle.in.tum.de/​library/​HOL/​index.html|Isabelle library]]
-  * [[http://​afp.sourceforge.net/​|Isabelle ​Arhive ​of Formal proofs]] containing:+  * [[http://​afp.sourceforge.net/​|Isabelle ​Archive ​of Formal proofs]] containing:
     * semantics and type soundness of Java     * semantics and type soundness of Java
     * cryptographic primitives and systems     * cryptographic primitives and systems
Line 14: Line 14:
     * distributed algorithms (clock synchronization,​ disk paxos)     * distributed algorithms (clock synchronization,​ disk paxos)
     * quantifier elimination     * quantifier elimination
 +  * [[http://​www.springerlink.com/​content/​fr28285458l06g58/​|The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/​ZF]]
   * In HOL system   * In HOL system
     * [[http://​www.cl.cam.ac.uk/​~jrh13/​papers/​tang.html|Floating point verification in HOL Light: the exponential function]]     * [[http://​www.cl.cam.ac.uk/​~jrh13/​papers/​tang.html|Floating point verification in HOL Light: the exponential function]]