Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:results_proved_in_hol [2008/05/28 03:26] vkuncak |
sav08:results_proved_in_hol [2009/03/05 11:58] 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 of Java | + | * semantics and type soundness of Java |
* cryptographic primitives and systems | * cryptographic primitives and systems | ||
* real analysis theorems and inequalities | * real analysis theorems and inequalities | ||
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]] |