20 ms·
Tangential question. Is there a mathematics curriculum out there that focuses on constructive foundations? Or is it possible to assemble one? I feel this would
by nextos 7y ago
Tangential question. Is there a mathematics curriculum out there that focuses on constructive foundations? Or is it possible to assemble one?
I feel this would be much more adequate for then following up with pure CS studies on topics such as [1-6].
Classical math bootcamps, like Math 55, are typically algebra plus analysis and they don't even focus too much on classical foundations.
[1] https://www.elsevier.com/books/lectures-on-the-curry-howard-isomorphism/sorensen/978-0-444-52077-7 https://www.elsevier.com/books/lectures-on-the-curry-howard-...
[2] https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/
[3] https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/
[4] https://www.springer.com/gb/book/9783540654100 https://www.springer.com/gb/book/9783540654100
[5] http://www.concrete-semantics.org/ http://www.concrete-semantics.org/
[6] http://adam.chlipala.net/frap/ http://adam.chlipala.net/frap/
- hackermailman 7y agoBesides these lecture notes http://www2.masfak.ni.ac.rs/cmfp2013/Nis%20lecture%20170113.pdf http://www2.masfak.ni.ac.rs/cmfp2013/Nis%20lecture%20170113.... I haven't found a curriculum. This is one of the goals of Robert Harper et. all involved in type theory research https://existentialtype.wordpress.com/2018/01/15/popl-2018-tutorial/ https://existentialtype.wordpress.com/2018/01/15/popl-2018-t... There is a guy however with a rational foundations of Math curriculum, doing algebraic calculus and rational Trig that I find easy to work with (ie: building a library) https://www.youtube.com/user/njwildberger/playlists https://www.youtube.com/user/njwildberger/playlists
- throwawaymath 7y agoI'm not familiar with any curriculum focusing on constructivist foundations. Out of curiosity, why do you feel constructivist foundations would be more complementary to theoretical computer science?
- logicchains 7y agoConstructive maths is generally computable maths, which means less worry about whether whatever you just did is computable or not.
- Gondolin 7y agoMore precisely the effective topos is a kind of realizability topos with a nno where every function is computable. Such a (non trivial) topos cannot be classical, otherwise the halting problem would be decidable. However the effective topos can only deal with calculability, not complexity. For complexity linear logic (without exponentials) and symmetric monoidal categories are better suited (but I don't know if there exists a model where every function is in P for instance).
- valw 7y agoYou might be interested in the works of Gérard Huet! http://gallium.inria.fr/~huet/PUBLIC/FSCD16.pdf http://gallium.inria.fr/~huet/PUBLIC/FSCD16.pdf
- nextos 7y agoThanks. I know about Gérard Huet, but not about this particular publication.