Isabelle/HOL

By Tobias Nipkow, Lawrence Charles Paulson, M. Wenzel. Lecture Notes in Computer Science, 2002

622 citations recorded by the source corpus.

Subfields: Artificial Intelligence

View Paper: https://www.semanticscholar.org/paper/628b6018231ec49782def9f0b83e086a0cdc9b3e

Citations in the corpus

• A FORMAL PROOF OF THE KEPLER CONJECTURE (2015, neutral): “Other required software tools are Isabelle/HOL [ 37 ], HOL Light [ 23 ], OCaml (the implementation language of HOL Light), the CamlP5 preprocessor (for a syntax extension to OCaml for parsing of mathematical terms), and GLPK (for linear programming) [ 8 ].”