hitchhikers guide

Stream: general

[Marijn Stollenga]

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

[Kevin Buzzard]

There's #tpil

[Bryan Gin-ge Chen]

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]

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]

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

[Mario Carneiro]

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]

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

[Marcus Rossel]

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

[Jeremy Avigad]

@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]

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]

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]

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

[Kevin Buzzard]

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

[Jasmin Blanchette]

Google isn't ranking it high enough I guess.

[Kevin Buzzard]

I used duck duck go :P