I love this book so much. As a UW student I took CS245E, a logic course where this was used as the textbook, and that course made me seriously consider pursuing pure mathematics as a minor for my degree. Really accessible introduction to dependent type theory and predicate logic.
For those interested in type theory and looking for a more video-y/live treatment of the subject, the HoTTEST Summer School 2022 is happening right now. The first week just ended but they put up videos and notes so you can catch up if you’re interested: https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest_summer_school_2022.html
Ah, I think the links are on the Discord server. The page I linked is probably not regularly updated? Regular updates are on the Discord, along with profs/TAs to ask questions and other students to work with.
Thanks for posting! I was actually looking for a simple undergrad text in logic and computation from a Curry-Howard angle. There are not many such texts. Any other recommendations?
I am not super familiar with other materials in this field, though I was told by the professor that the Resources section of the book would be a decent starting point for someone moving beyond the contents of the book.
Prabhakar is probably the most impressive prof i had in Waterloo. He taught my Math145, 146 and CS145 courses 🙏
I did not have the mental capacity to fully digest all the contents in my university years. But once I started to hit some of the bleeding edges field at work, I appreciate the courses a lot more.
I love this book so much. As a UW student I took CS245E, a logic course where this was used as the textbook, and that course made me seriously consider pursuing pure mathematics as a minor for my degree. Really accessible introduction to dependent type theory and predicate logic.
For those interested in type theory and looking for a more video-y/live treatment of the subject, the HoTTEST Summer School 2022 is happening right now. The first week just ended but they put up videos and notes so you can catch up if you’re interested: https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest_summer_school_2022.html
Sorry, I don’t see the videos there? I’m on mobile.
Ah, I think the links are on the Discord server. The page I linked is probably not regularly updated? Regular updates are on the Discord, along with profs/TAs to ask questions and other students to work with.
That said, the videos are uploaded here: https://www.youtube.com/playlist?list=PLtIZ5qxwSNnzpNqfXzJjlHI9yCAzRzKtx
And the assignments and notes are here: https://github.com/martinescardo/HoTTEST-Summer-School
Thanks for posting! I was actually looking for a simple undergrad text in logic and computation from a Curry-Howard angle. There are not many such texts. Any other recommendations?
Jeremy Avigad has a few great texts: https://www.andrew.cmu.edu/user/avigad/. There’s also https://raw.githubusercontent.com/blanchette/logical_verification_2020/master/hitchhikers_guide.pdf, but I don’t know other texts.
For graduate material, there is quite a lot of choice, though. https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching/INF551/ in particular looks very promising.
I am not super familiar with other materials in this field, though I was told by the professor that the Resources section of the book would be a decent starting point for someone moving beyond the contents of the book.
You could consider looking at Mark Tarver’s Logic, Proof, and Computation.
Thanks. Can I access the TOC of this book somewhere?
Yes, http://web.archive.org/web/20161118142913/https://www.shenlanguage.org/LPC/lpc.html
Thank you, much appreciated.
You’re welcome! You are potentially already familiar with Wadler’s Propositions As Types, but the video does a great job (imho) of expressing some key conceptual takeaways from roughly the first half of Mimram’s Proof = Program. https://homepages.inf.ed.ac.uk/wadler/topics/history.html#propositions-as-types.
Good luck on your journey =)
Prabhakar is probably the most impressive prof i had in Waterloo. He taught my Math145, 146 and CS145 courses 🙏
I did not have the mental capacity to fully digest all the contents in my university years. But once I started to hit some of the bleeding edges field at work, I appreciate the courses a lot more.
+1 for the Mission Of Burma quote at the start of the intro.