- Record: found
- Abstract: not found
- Book Chapter: not found
Interactive Theorem Proving
Importing HOL Light into Coq
other
Read this book at
There is no author summary for this book yet. Authors can add summaries to their books on ScienceOpen to make them more accessible to a non-specialist audience.
Related collections
Most cited references8
- Record: found
- Abstract: not found
- Book Chapter: not found
HOL Light: A tutorial introduction
John Harrison (1996)
- Record: found
- Abstract: not found
- Book Chapter: not found
Importing HOL into Isabelle/HOL
Steven Obua, Sebastian Skalberg (2006)
- Record: found
- Abstract: not found
- Book Chapter: not found
Towards Self-verification of HOL Light
John Harrison (2006)