The goal is mainly to understand its relation to proof assistants, I have experience with it before as a purely logical study but i haven’t tried to see it in this new context for myself. This book looks excellent though, thank you for your recommendation
The goal is mainly to understand its relation to proof assistants, I have experience with it before as a purely logical study but i haven’t tried to see it in this new context for myself. This book looks excellent though, thank you for your recommendation
Ah, then you’ll want to read about the [https://hal.inria.fr/inria-00076024/document](Calculus of Constructions):
Yeah, TAPL is the book on type systems. I’m not aware of competition.