What is the definitive roadmap to understanding Coq’s theory and source code for extremely skeptical and pedantic mathematician? Is there at least an order of reading sources? I want explicitly, not just be able to prove theorem, i can, I want to understand the whole theory and meta-theory with academic regouriousity. Not just something, all of it. What is the best way to do it?
Perhaps look into MetaCoq and related papers such as Correct and Complete Type Checking and Certified Erasure for Coq, in Coq.
1 Like