3
$\begingroup$

Is there a good source on the type theory of HOL/Isabelle/other HOL-based LCF-style theorem provers?

$\endgroup$
1

1 Answer 1

1
$\begingroup$

I don't think Isabelle's implementation manual is a good place to look at this. It may certainly contain links to the explanation but you can find instead a pedagogical introduction in section 2 of this thesis.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.