Re: [isabelle] Where to learn about HOL vs FOL?

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.

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).

Le Thu, 31 Jan 2013 16:51:59 +0100, Alfio Martini <alfio.martini at> a écrit:

Hi Yannick,

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.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.