Re: [isabelle] Where to learn about HOL vs FOL?
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Where to learn about HOL vs FOL?
- From: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr>
- Date: Sun, 29 Dec 2013 22:55:22 +0100
- Organization: Ada @ Home
- References: <op.wrrj47uzule2fv@cardamome> <510A79F0.firstname.lastname@example.org> <CAAPnxw2g6Di9MEmQgyqhf_+NBW5HLrVAPi2JVxohcFLTqWe1dA@mail.gmail.com>
- User-agent: Opera Mail/12.16 (Linux)
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
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
Le Thu, 31 Jan 2013 16:51:59 +0100, Alfio Martini
<alfio.martini at acm.org> a écrit:
Adding to Gottfried´s selected readings, I strongly recommend the highly
"The Seven Virtues of Simple Type Theory' by William Farmer (Journal of
Applied Logic 6, 2008.
“Syntactic sugar causes cancer of the semi-colons.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and