Re: [isabelle] Literature on the type system of Isabelle/HOL; text by Mike Gordon
It can be downloaded from here: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.27.6103
> On 8 Aug 2016, at 12:13, Ken Kubota <mail at kenkubota.de> wrote:
> Dear Members of the Research Community,
> As part of my efforts to try to understand the type system of Isabelle/HOL, I
> have gathered the references from the mails written by Corey Richardson and
> Michael Norrish and from The Isabelle/Isar Reference Manual, especially from
> a) Chapter 10: Higher-Order Logic (pp. 236 f.)
> b) Â 11.7 Semantic subtype definitions (pp. 260-263)
> c) Â 11.8 Functorial structure of types (pp. 263 f.).
> In all cases, with one exception, I was able to obtain either the link to the
> online version or the ISBN number.
> The exception is Mike Gordon's text "HOL: A machine oriented formulation of
> higher order logic" (Technical Report 68, University of Cambridge Computer
> Laboratory), registered at
> As Isabelle is provided by the University of Cambridge Computer Laboratory,
> among others, would it be possible for the Isabelle developers to make this
> technical report available online as a PDF file? This was done for the first
> five reports listed at
> According to the references supplied with the traditional (Mike Gordon's) HOL
> variant, a revised version exists: "Technical Report No.\ 68 (revised
> version)", quoted from
> Either both versions or the revised version should be made available.
> I would like to take this opportunity to thank Michael Norrish for his advice.
> The LOGIC part of HOL4 system's documentation at
> is the kind of short and precise formulation of the logical core I recently
> proposed for Isabelle/HOL, too:
> In this HOL4 document, it is stated: "From a logical point of view it would be
> better to have a simpler substitution primitive, such as 'Rule R' of Andrews'
> logic Q0, and then to derive more complex rules from it." (p. 27)
> This is exactly the same idea that I presented recently: "The main criterion is
> expressiveness [cf. Andrews, 2002, p. 205], or, vice versa, the reducibility of
> mathematics to a minimal set of primitive rules and symbols. [...] For the
> philosopher it is not proof automation but expressiveness that is the main
> criterion, such that the method with the least amount of rules of inferences,
> i.e., a Hilbert-style system, is preferred, and all other rules become derived
> Similarly, the HOL4 document argues in favor of definitions instead of
> introducing new axioms: "The advantages of postulation over definition have
> been likened by Bertrand Russell to the advantages of theft over honest toil.
> As it is all too easy to introduce inconsistent axiomatizations, users of the
> HOL system are strongly advised to resist the temptation to add axioms, but to
> toil through definitional theories honestly." [p. 33]
> In the same manner, I wrote: "One consequence [...] is to avoid the use of
> non-logical axioms. [...] The appropriate way to deal with objects of certain
> properties is to create a set of objects with these properties." [Kubota, 2015,
> p. 29]
> For this reason, in the R0 implementation, the group axioms are expressed not
> as axioms, but as properties in the definition of "Grp" (wff 266):
> http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf (p. 359)
> Kind regards,
> Ken Kubota
> [S1] The Isabelle/Isar Reference Manual (February 17, 2016)
> [S2] Reference in the e-mail written by Corey Richardson
> Dmitry Traytel / Andrei Popescu / Jasmin C. Blanchette, Foundational,
> Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to
> Theorem Proving
> [S3] Reference in the e-mail written by Michael Norrish
> "The chapters from the HOL book mentioned above are available as part of the
> HOL4 system's documentation at:
> See Â2.5.4 in particular for a discussion of how the system can be extended
> with new types."
> The HOL System: LOGIC (November 6, 2014)
> Derived References (from [S1], pp. 260-263)
>  W. M. Farmer. The seven virtues of simple type theory. J. Applied Logic,
> 6(3):267-286, 2008.
>  M. J. C. Gordon. HOL: A machine oriented formulation of higher order
> logic. Technical Report 68, University of Cambridge Computer Laboratory, 1985.
>  A. Pitts. The HOL logic. In M. J. C. Gordon and T. F. Melham, editors,
> Introduction to HOL: A Theorem Proving Environment for Higher Order Logic,
> pages 191-232. Cambridge University Press, 1993.
> ISBN 0-521-44189-7
>  M. Wenzel. Type classes and overloading in higher-order logic. In E. L.
> Gunter and A. Felty, editors, Theorem Proving in Higher Order Logics: TPHOLs
> '97, volume 1275 of Lecture Notes in Computer Science. Springer-Verlag, 1997.
>  F. Haftmann and M. Wenzel. Constructive type classes in Isabelle. In T.
> Altenkirch and C. McBride, editors, Types for Proofs and Programs, TYPES 2006,
> volume 4502 of LNCS. Springer, 2007.
>  O. Kuncar and A. Popescu. A consistent foundation for Isabelle/HOL. In C.
> Urban and X. Zhang, editors, Interactive Theorem Proving - 6th International
> Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings, volume
> 9236 of Lecture Notes in Computer Science. Springer, 2015.
> Standard References
> Andrews, Peter B. (1986), An Introduction to Mathematical Logic and Type
> Theory: To Truth Through Proof. Orlando: Academic Press. ISBN 0-12-058535-9
> (Hardcover). ISBN 0-12-058536-7 (Paperback).
> Andrews, Peter B. (2002), An Introduction to Mathematical Logic and Type
> Theory: To Truth Through Proof. Second edition. Dordrecht / Boston / London:
> Kluwer Academic Publishers. ISBN 1-4020-0763-9. DOI: 10.1007/978-94-015-9934-4.
> Andrews, Peter B. (2014), "Church's Type Theory". In: Stanford Encyclopedia of
> Philosophy (Spring 2014 Edition). Ed. by Edward N. Zalta. Available online at
> http://plato.stanford.edu/archives/spr2014/entries/type-theory-church/ (July 2,
> Church, Alonzo (1940), "A Formulation of the Simple Theory of Types". In:
> Journal of Symbolic Logic 5, pp. 56-68.
> Further References
> Kubota, Ken (2015), On the Theory of Mathematical Forms (draft from May 18,
> 2015). Unpublished manuscript. SHA-512: a0dfe205eb1a2cb29efaa579d68fa2e5
> 45af74d8cd6c270cf4c95ed1ba6f7944 fdcffaef2e761c8215945a9dcd535a50
> 011d8303fd59f2c8a4e6f64125867dc4. DOI: 10.4444/100.10. See:
> Kubota, Ken (2015a), Excerpt from [Kubota, 2015] (pp. 356-364, pp. 411-420, and
> pp. 754-755). Available online at
> (January 24, 2016). SHA-512: 67a48ee12a61583bd82c286136459c0c
> 9fd77f5fd7bd820e8b6fe6384d977eda 4d92705dac5b3f97e7981d7b709fc783
> Ken Kubota
> doi: 10.4444/100
This archive was generated by a fusion of
Pipermail (Mailman edition) and