Lab for Automated Reasoning and Analysis 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]]
 
sav08/results_proved_in_hol.txt · Last modified: 2009/03/05 11:58 by vkuncak
 
© EPFL 2018 - Legal notice