Zulip Chat Archive

Stream: general

Topic: hitchhikers guide


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?

Kevin Buzzard (Apr 14 2021 at 21:20):

There's #tpil

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).

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.

Jasmin Blanchette (Apr 19 2021 at 19:00):

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

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: )

Mario Carneiro (Apr 19 2021 at 19:02):

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

Marcus Rossel (Apr 20 2021 at 18:55):

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

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.

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).

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.

Marcus Rossel (Apr 21 2021 at 09:30):

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

Kevin Buzzard (Apr 21 2021 at 10:22):

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

Jasmin Blanchette (Apr 21 2021 at 10:28):

Google isn't ranking it high enough I guess.

Kevin Buzzard (Apr 21 2021 at 10:31):

I used duck duck go :P


Last updated: Dec 20 2023 at 11:08 UTC