Zulip Chat Archive

Stream: new members

Topic: Type theory books?

Vaibhav Karve (Mar 23 2020 at 13:00):

This is going to sound like a SE/SO post. Is there a recommended text for Type theory?

  1. need not be Lean-specific.
  2. I am not necessarily interested in researching type-theory. I want more beginner-level texts that don't require a ton of background.

This was promoted by my realization that my set-theoretic intuition doesn't always work in type theory. So I think books might help (apart from doing more Lean!).

Mario Carneiro (Mar 23 2020 at 13:05):

Learn you a haskell is pretty good

Rob Lewis (Mar 23 2020 at 13:05):

Nederpelt and Geuvers is a good comprehensive reference, although calling it "beginner level" is a bit of a stretch.

Mario Carneiro (Mar 23 2020 at 13:06):

The HoTT book is also good, if you ignore the stuff about HoTT (I mean that part's good too but not necessary to understand for lean)

Mario Carneiro (Mar 23 2020 at 13:08):

I have heard good things about Software foundations, and certified programming with dependent types, although those might have too much CS bent for you

Kevin Buzzard (Mar 23 2020 at 13:13):

I read all three as a mathematician starting with no idea of what a type was. Learn you a Haskell I read three times, each time getting further than the last. Then I tried certified programming with dependent types and found it much too hard going because I still knew no Coq or lean. I then read Theorem proving in lean the first time, understanding some of it but certainly not typeclasses, and then I read the first book of software foundations and I did a bunch of the harder and more mathematical exercises in lean. I then read Theorem proving in lean again and all the way through I was working on concrete mathematics questions from my own example sheets or books

Kevin Buzzard (Mar 23 2020 at 13:13):

And I just asked loads of questions here

Kevin Buzzard (Mar 23 2020 at 13:14):

I later came back to CPDT and implemented the first chapter in Lean

Bryan Gin-ge Chen (Mar 23 2020 at 14:12):

I started reading Nederpelt and Geuvers recently and while it's slow going it's been pretty enlightening so far. I don't think it really requires any special background, though there were a lot of things at the start that probably would've seemed unmotivated / way too boring if I hadn't already played around with Lean.

Vaibhav Karve (Mar 23 2020 at 19:20):

Thank you all for these great recommendations! Some of these I have tried reading before while there are others I hadn't heard of. Time to do more reading (and working out in Lean).

Miguel Raz Guzmán Macedo (Mar 24 2020 at 05:23):

Sorry to come in so late, but would any of you all know about a Lean version of Formal Reasoning About Programs? Its It's by Chlipala, the same author of CPDT. FRAP is also a course in MIT 6.822 to use verification methods in software, but unfortunately it is built atop of Coq. Would Lean prove to be more powerful in this context due to its higher logic than Coq?

Mario Carneiro (Mar 24 2020 at 05:30):

Lean doesn't have any significant logical advances over Coq that would be relevant here AFAIK

Mario Carneiro (Mar 24 2020 at 05:30):

or do you mean something else?

Miguel Raz Guzmán Macedo (Mar 24 2020 at 05:34):

Well, I guess there is just more tooling now for Coq than Lean.

Miguel Raz Guzmán Macedo (Mar 24 2020 at 05:35):

If I do a deep dive into Lean, it would be for formally verifying differential equation codes written in Julia.

Miguel Raz Guzmán Macedo (Mar 24 2020 at 05:35):

But seeing this book there might be more tools to leverage with Coq.

Miguel Raz Guzmán Macedo (Mar 25 2020 at 05:31):

Answering my own question, in the tutorials section there is the "Logical Verification in Lean" book, based on a course given by Jasmin Blanchette and Alexander Bentkamp, so thank to them, this looks like just what I needed!

Jasmin Blanchette (Apr 03 2020 at 12:42):

@Miguel Raz Guzmán Macedo: Be aware that there is a new version of the book, with 50 or so more pages, color, etc. See

https://lean-forward.github.io/logical-verification/2020/index.html#material

The old book was really just our first draft. Based on the experience of teaching with it, we found a lot that could be improved. This concerns especially the early chapters.

Mario Carneiro (Apr 03 2020 at 12:43):

you should put the links in links instead of code blocks

Miguel Raz Guzmán Macedo (Apr 03 2020 at 13:41):

Beautiful! I'll be sure to take a look!

Miguel Raz Guzmán Macedo (Apr 03 2020 at 13:42):

And thank you so much for coming back to this @Jasmin Blanchette ! Very much appreciated!

Last updated: Dec 20 2023 at 11:08 UTC