Zulip Chat Archive

Stream: general

Topic: hitchhikers guide


view this post on Zulip Marijn Stollenga (Apr 14 2021 at 20:02):

Man the Hitchhikers guide to Logical Verification is great. Are there some other good books to understand the basics of Leans' logic?

view this post on Zulip Kevin Buzzard (Apr 14 2021 at 21:20):

There's #tpil

view this post on Zulip Bryan Gin-ge Chen (Apr 14 2021 at 21:23):

I recommended Nederpelt and Geuvers's book in another thread:
Bryan Gin-ge Chen said:

In terms of type theory background, I found Nederpelt and Geuvers's "Type Theory and Formal Proof" fairly enlightening, though as an introductory text, it doesn't cover CIC (calculus of inductive constructions, some variant of which is used in Lean's foundations, I believe).

view this post on Zulip Jeremy Avigad (Apr 15 2021 at 17:28):

If I can indulge in some self-promotion, here is a general overview of formal foundations that will appear in a handbook on proof assistants that is being edited by Jasmin Blanchette and Assia Mahboubi: https://arxiv.org/abs/2009.09541.

view this post on Zulip Jasmin Blanchette (Apr 19 2021 at 19:00):

Isn't there also @Mario Carneiro 's MSc thesis?

view this post on Zulip Mario Carneiro (Apr 19 2021 at 19:01):

https://github.com/digama0/lean-type-theory/releases/tag/v1.0 (although calling it "the basics" is a bit of a stretch :grinning: )

view this post on Zulip Mario Carneiro (Apr 19 2021 at 19:02):

It's "basic" as in "foundational" but not "basic" as in "simple"

view this post on Zulip Marcus Rossel (Apr 20 2021 at 18:55):

@Jeremy Avigad Is there some way to be notified about when the full book is released?

view this post on Zulip Jeremy Avigad (Apr 20 2021 at 19:21):

@Jasmin Blanchette is the person to ask. Getting academics to meet deadlines is like herding cats, so with any multi-author handbook, it's hard to predict when all the chapters will be done (and I wouldn't hold my breath). But maybe Jasmin knows of others who have made their drafts available.

view this post on Zulip Jasmin Blanchette (Apr 21 2021 at 00:12):

The truth is, I don't know.. The best is probably to keep an eye on the News part of my web site and look for keywords like "Mahboubi" or "Proof Assistants and Their Applications in Mathematics and Computer Science" (if you have some automatic mechanism for doing so).

view this post on Zulip Jasmin Blanchette (Apr 21 2021 at 00:14):

and I wouldn't hold my breath

Alas, so true. Thankfully, one of {Assia,I} can be a real bully with authors who don't deliver.

view this post on Zulip Marcus Rossel (Apr 21 2021 at 09:30):

@Jasmin Blanchette what's the URL to your website?

view this post on Zulip Kevin Buzzard (Apr 21 2021 at 10:22):

Did you try search? https://www.cs.vu.nl/~jbe248/

view this post on Zulip Jasmin Blanchette (Apr 21 2021 at 10:28):

Google isn't ranking it high enough I guess.

view this post on Zulip Kevin Buzzard (Apr 21 2021 at 10:31):

I used duck duck go :P


Last updated: May 13 2021 at 19:20 UTC