Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] types in higher order logic

view this post on Zulip Email Gateway (Aug 19 2022 at 14:35):

From: Gergely Buday <gbuday@gmail.com>
Hi,

is type inhabitation decidable in Isabelle's higher order logic? I.e. given
any term t and type T, whether

G |- t : T

holds? Is Isabelle/HOL's type system basically Hindley-Milner?

view this post on Zulip Email Gateway (Aug 19 2022 at 14:35):

From: Lawrence Paulson <lp15@cam.ac.uk>
Yes, type-checking in Isabelle is static and is essentially Hindley-Milner, augmented with type classes.
Larry

Last updated: Apr 30 2024 at 08:19 UTC