Not signed in (Sign In)

Start a new discussion

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry beauty bundles calculus categories category category-theory chern-weil-theory cohesion cohesive-homotopy-theory cohesive-homotopy-type-theory cohomology combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundations functional-analysis functor galois-theory gauge-theory gebra geometric-quantization geometry goodwillie-calculus graph graphs gravity grothendieck group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory history homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory infinity integration-theory internal-categories k-theory kan lie lie-theory limit limits linear linear-algebra locale localization logic manifolds mathematics measure-theory modal modal-logic model model-category-theory monad monoidal monoidal-category-theory morphism motives motivic-cohomology nonassociative noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pasting philosophy physics planar pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory string-theory subobject superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 14th 2016

    The new second edition is recorded at Practical Foundations for Programming Languages plus a link to a description of the changes.

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTime7 days ago

    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”?

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTime6 days ago
    • (edited 6 days ago)

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

  1. 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?

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTime6 days ago
    • (edited 6 days ago)

    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.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTime5 days ago

    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.

    • CommentRowNumber7.
    • CommentAuthorRichard Williamson
    • CommentTime5 days ago
    • (edited 5 days ago)

    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.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTime4 days ago

    If it can be useful for the reader, all these books should well point to each other.

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTime4 days ago

    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.

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)