3 ms·

Homotopy Type Theory by Vladimir Voevodsky is another possibility. This is an attempt to link Topology and Computer Science https://homotopytypetheory.org/boo

Homotopy Type Theory by Vladimir Voevodsky is another possibility. This is an attempt to link Topology and Computer Science https://homotopytypetheory.org/book/ https://homotopytypetheory.org/book/ Back in the day there was Feynman's Lectures on Computation. Hint: pdf can be found by searching https://www.amazon.com/Feynman-Lectures-Computation-Richard-P/dp/0738202967 https://www.amazon.com/Feynman-Lectures-Computation-Richard-... See also nLab https://ncatlab.org/nlab/show/higher+category+theory https://ncatlab.org/nlab/show/higher+category+theory one should never forget Jacob Lurie's "Higher Topos Theory" which is 1000 pages just like that http://www.math.harvard.edu/~lurie/papers/croppedtopoi.pdf http://www.math.harvard.edu/~lurie/papers/croppedtopoi.pdf Actually I recommend against readin it as it only covers 2 of the 4 topics you discuss (Topology and Logic). However it certainly has applications to the other two.

fmap 10y ago
The infinity groupoid models of type theory have already revolutionized our understanding of equality in type theory. So far, the 21st century has been an incredible time for logicians. There are also older, and very different topological models for typed lambda calculi (see e.g. http://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf http://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf). These motivate things like Escardo's "seemingly impossible functional programs" (http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ http://math.andrej.com/2007/09/28/seemingly-impossible-funct...) and, along different lines, Abstract Stone Duality (http://www.paultaylor.eu/ASD/ http://www.paultaylor.eu/ASD/).
torustic 10y ago
Lurie's "On Infinity Topoi"[0] preceded the book and is, I quote[1], > 50 pages of pure cake, beautifully and informally written. The book is 1000 pages long. There is some new cake there, but not 20 times as much. [0] https://arxiv.org/abs/math/0306109 https://arxiv.org/abs/math/0306109 [1] https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/comment-page-1/#comment-209 https://mathematicswithoutapologies.wordpress.com/2015/05/13...

fmap 10y ago

The infinity groupoid models of type theory have already revolutionized our understanding of equality in type theory. So far, the 21st century has been an incredible time for logicians. There are also older, and very different topological models for typed lambda calculi (see e.g. http://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf http://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf). These motivate things like Escardo's "seemingly impossible functional programs" (http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ http://math.andrej.com/2007/09/28/seemingly-impossible-funct...) and, along different lines, Abstract Stone Duality (http://www.paultaylor.eu/ASD/ http://www.paultaylor.eu/ASD/).

torustic 10y ago

Lurie's "On Infinity Topoi"[0] preceded the book and is, I quote[1], > 50 pages of pure cake, beautifully and informally written. The book is 1000 pages long. There is some new cake there, but not 20 times as much. [0] https://arxiv.org/abs/math/0306109 https://arxiv.org/abs/math/0306109 [1] https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/comment-page-1/#comment-209 https://mathematicswithoutapologies.wordpress.com/2015/05/13...