Differences
This shows you the differences between two versions of the page.
| Next revision Both sides next revision | |||
|
sav08:results_proved_in_hol [2008/05/28 03:21] vkuncak created |
sav08:results_proved_in_hol [2008/05/28 03:26] vkuncak |
||
|---|---|---|---|
| Line 17: | Line 17: | ||
| * [[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]] | ||
| * [[http://portal.acm.org/citation.cfm?id=1182776|Formalization of fixed-point arithmetic in HOL]] | * [[http://portal.acm.org/citation.cfm?id=1182776|Formalization of fixed-point arithmetic in HOL]] | ||
| + | * Also results in variations of HOL implemented in systems PVS, Coq, NuPRL | ||