A survey on embedding programming logics in a theorem prover
2002
Theorem provers were also called 'proof checkers' because that is what
they were in the beginning. They have grown powerful, however, capable
in many cases to automatically produce complicated proofs. In particular,
higher order logic based theorem provers such as HOL and PVS became
popular because the logic is well known and very expressive. They are
generally considered to be potential platforms to embed a programming
logic for the purpose of formal verification. In this paper we investigate
a number of most commonly used methods of embedding programming
logics in such theorem provers and expose problems we discover. We will
also propose an alternative approach : hybrid embedding.
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
22
References
13
Citations
NaN
KQI