[POPLmark] Meta-comment

[Michael Norrish]

Frank Pfenning writes:
 
> I may be wrong about each of those---if there is someone listening
> who has better knowledge, please correct me.
 
> - Isabelle/HOL uses type variables, type classes, and overloading.
>   I believe there is an argument for the correctness of this (a note
>   by John Harrison?), but it is certainly different from pure
>   Church's type theory (often called Higher-Order Logic).
>   Also, I don't believe that the theory of higher-order logic
>   in the presence of description and/or choice operators is
>   really all that well understood.  Chad Brown's recent thesis
>   makes a lot of progress in understanding extensionality and
>   equality, but description is still outside its scope.
 
The HOL system's logic (Church's system + parametric polymorphism
basically) is as sound as ZFC.  The description/choice operator is an
embodiment of the Axiom of Choice.  It's all pretty obvious: each
ground type is a non-empty set; function-spaces in HOL are represented
by functional cartesian products in the set theory.  Polymorphic types
are modelled as families of sets.  Again, this is well documented.

Isabelle/HOL complicates things somewhat with its type classes
(axiomatic and not), and overloading.  Nonetheless, it seems
reasonably clear how these fit into the standard set-theoretic model.

> Don't get me wrong---I have the greatest respect for the developers of
> these systems and I believe they are well-engineered and rest on good
> foundations, but I don't see that their basis is crystal clear or in
> some essential way better understood than Twelf.
 
I won't make any remarks about Twelf.  However, I will make the claim
that HOL's basis *is* crystal clear.

Michael.