*To*: "Yannick Duchêne (Hibou57)" <yannick_duchene at yahoo.fr>*Subject*: Re: [isabelle] Where to learn about HOL vs FOL?*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Sun, 29 Dec 2013 22:02:19 +0000*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <op.w8vi6k0qule2fv@cardamome>*References*: <op.wrrj47uzule2fv@cardamome> <510A79F0.9050308@gmx.com> <CAAPnxw2g6Di9MEmQgyqhf_+NBW5HLrVAPi2JVxohcFLTqWe1dA@mail.gmail.com> <op.w8vi6k0qule2fv@cardamome>

Yes, the question of whether or not to adopt an explicit logic of “definedness” continues to attract discussion. Most implemented formal systems have only total functions. Then there is PVS and the dependently-typed calculi, which allow partial functions but still don’t formalise the notion of “undefined”. I believe that Farmer advocates such formalisms. LCF and related systems formalise domain theory, in which the concept of definedness induces a partial ordering over all values. As always, increasing the expressiveness of the formalism also increases the difficulty of conducting proofs. Larry Paulson On 29 Dec 2013, at 21:55, Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr> wrote: > From the same author (W. M. Farmer), an academic course (link below) I landed into. Its wordings in chapter 5, made me feel I've read something like this before… indeed, as I checked, this was in the Seven Virtues of STT. > > http://imps.mcmaster.ca/courses/SE-2F03-05/slides/ > > Chapter 5 concisely explains (to me, even more concisely than in the Seven Virtues) many of the theoretical concepts found in Isar‑Ref and the Isabelle Tutorial (for people like me who are not from the academic world). He's a lot fan of the type theory. > > Interestingly, at the end, he suggest an extension of STT, which would include indefinite expressions, which seems to be the same as what shown‑up during another topic with references to HOL+LCF as HOLCF (an Isabelle theory).

**References**:**Re: [isabelle] Where to learn about HOL vs FOL?***From:*Yannick Duchêne (Hibou57)

- Previous by Date: Re: [isabelle] Where to learn about HOL vs FOL?
- Next by Date: [isabelle] Question on sequential pattern matching
- Previous by Thread: Re: [isabelle] Where to learn about HOL vs FOL?
- Next by Thread: [isabelle] A problem on ML-like function programming
- Cl-isabelle-users December 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list