OpenTheory
The goal of the OpenTheory project is to allow specifications and proofs to be shared between different theorem prover implementations of higher order logic, including HOL Light, HOL4 and ProofPower. It is hoped that OpenTheory packages are adopted by the higher order logic theorem proving community as a common format to build a standard library of formalized mathematics and verified software.
Keywords for this software
References in zbMATH (referenced in 15 articles )
Showing results 1 to 15 of 15.
Sorted by year (- Abrahamsson, Oskar: A verified proof checker for higher-order logic (2020)
- Abrahamsson, Oskar; Ho, Son; Kanabar, Hrutvik; Kumar, Ramana; Myreen, Magnus O.; Norrish, Michael; Tan, Yong Kiam: Proof-producing synthesis of CakeML from monadic HOL functions (2020)
- Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
- Chihani, Zakaria; Miller, Dale; Renaud, Fabien: A semantic framework for proof evidence (2017)
- MÃ¼ller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian: Classification of alignments between concepts of formal mathematical systems (2017)
- Arthan, Rob: On definitions of constants and types in HOL (2016)
- Carneiro, Mario M.: Conversion of HOL Light proofs into Metamath (2016)
- Ebner, Gabriel; Hetzl, Stefan; Reis, Giselle; Riener, Martin; Wolfsteiner, Simon; Zivota, Sebastian: System description: GAPT 2.0 (2016)
- Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott: Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (2016)
- Lin, Yuhui; Grov, Gudmund; Arthan, Rob: Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC (2016)
- Davis, Jared; Myreen, Magnus O.: The reflective Milawa theorem prover is sound (down to the machine code that runs it) (2015)
- Gauthier, Thibault; Kaliszyk, Cezary: Matching concepts across HOL libraries (2014)
- Kaliszyk, Cezary; Rabe, Florian: Towards knowledge management for HOL Light (2014)
- Kumar, Ramana; Hurd, Joe: Standalone tactics using OpenTheory (2012)
- Hurd, Joe: The opentheory standard theory library (2011) ioport