Not signed in (Sign In)

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 book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics comma 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 finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics 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 stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft 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
    • CommentTimeNov 9th 2018

    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
    • CommentTimeNov 10th 2018
    • (edited Nov 10th 2018)

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

    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 10th 2018

    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
    • CommentTimeNov 10th 2018
    • (edited Nov 10th 2018)

    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
    • CommentTimeNov 11th 2018

    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
    • CommentTimeNov 11th 2018
    • (edited Nov 11th 2018)

    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
    • CommentTimeNov 12th 2018

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

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeNov 12th 2018

    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.