Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
The new second edition is recorded at Practical Foundations for Programming Languages plus a link to a description of the changes.
Why is Practical Foundations of Mathematics listed as a “Related page” at Practical Foundations for Programming Languages? Is it just because their titles both start with the phrase “Practical Foundations”?
There is indeed a remarkable relation between the foundations of mathematics and those of programming. A cute catchphrase for this is computational trinitarianism, where more pointers are given.
This relation becomes stronger still from a constructivistic-point of view (one might argue that it becomes an equivalence then, with foundations for programming being at the same time foundations for mathematics), which is roughly what in both these books is referred to as “practical”. More technically, this refers to the usage of the language/tools of type theory and/or categorical logic in both cases.
The “General Description page” of Taylor’s book is explicit about this right away in its first paragraph:
the book looks forward to more subtle bases in categorical type theory and the machine representation of mathematics.
as is the blurb for Harper’s book, right in its first sentence:
This text develops a comprehensive theory of programming languages based on type systems and structural operational semantics.
A text on a different level with the similarly related attitude is Lawvere-Schanuel’s Sets for Mathematics. (I have now cross-linked that entry with those of the other two books.)
As the one who coined ’homotopical trinitarianism’, Mike’s certainly aware of Harper’s catchphrase.
Is the question in #2 more about why the page cites Taylor’s book rather than, say, the HoTT book?
Oh, I didn’t see that it was Mike who asked. Why would he ask this?
Is the question in #2 more about why the page cites Taylor’s book rather than, say, the HoTT book?
The pointer to Taylor’s book was made back in 2012 (rev 1). Certainly we don’t need a discussion thread about whether to add also pointer to the HoTT book!? Please go ahead.
The question is not about why the subjects are related, but whether the books are related. If we had a page called foundation of computer science then of course it would link back and forth with foundation of mathematics. But on pages for specific books, we don’t generally even link directly to pages for other books about the same subject. For instance, Elephant doesn’t link directly to Sheaves in Geometry and Logic, and Categories Work doesn’t link directly to Categories, Allegories, Handbook of Categorical Algebra, etc. Instead they link to subject pages like topos theory and category theory, where one can find exhaustive collections of links to books about the subject in question; thus the latter list only has to be updated in one place to add a new book. So unless there is some relationship between the books PFPL and PFM more specific than the relation between their subject matters, I don’t think the two pages should link directly to each other.
I suppose the question is whether the titles are coincidental, or whether Harper’s book is a deliberate nod to Taylor’s? Harper does cite Taylor’s book, so is aware of it, though only in one reference in passing. Thus even if the title is not a nod to Taylor’s book as such, Harper must surely at least have liked the wording.
If it can be useful for the reader, all these books should well point to each other.
No, I don’t agree. I think it is more useful for the reader to direct them to a general subject page, where if they want a book about X they can look at all the options and find the one that is the most useful for them.
1 to 13 of 13