Email Gateway (Aug 23 2022 at 08:17): Email Gateway (Aug 23 2022 at 08:17):From: Gergely Buday <buday.gergely@uni-eszterhazy.hu>
Hi,
Church's classical paper on higher order logic introduces a simply-typed
logic.
As I understand, Isabelle/Pure, Isabelle/HOL and HOL4 have polymorphicly
typed higher order logics.
Is there a standard reference where this polymorphic higher order logic is
defined mathematically? I know that Isabelle's HOL is a bit different from
HOL4's HOL, I am interested in both.
Email Gateway (Aug 23 2022 at 08:17):From: Ken Kubota <mail@kenkubota.de>
HOL4: https://sourceforge.net/p/hol/mailman/message/36805192/
Also, Larry Paulson's paper on simple type theory in Isabelle might be of interest:
https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-175.pdf
The statement "Coquand [8] has shown that polymorphic higher-order logic is inconsistent." (p. 14) has to be interpreted with care.
Coq has (or had) some implicit mechanisms causing certain dependencies not being made explicit.
Kind regards,
Ken Kubota
Ken Kubota
http://doi.org/10.4444/100 <http://doi.org/10.4444/100>
Email Gateway (Aug 23 2022 at 08:24):From: Lawrence Paulson <lp15@cam.ac.uk>
For Isabelle/HOL with type classes, try this:
https://link.springer.com/article/10.1007/s10817-018-9454-8
See also https://www.researchgate.net/publication/322749560_A_Consistent_Foundation_for_IsabelleHOL to obtain a free version
Larry Paulson
Last updated: Apr 26 2024 at 01:06 UTC