CODEWITHSUNDEEP
coq
user1868607
user1868607

Reputation: 2600

The foundations of Coq

I'm assuming Coq at some point moved to an LCF approach. In the past, I wondered about the foundations of the kernel in Isabelle. And I found some nice description of Isabelle/Pure in a master thesis summarizing somehow the existing literature.

I was wondering if there is a description of Coq's kernel covering the logical and implementation aspects of it.

Upvotes: 0

Views: 115

Answers (1)

Théo Winterhalter
Théo Winterhalter

Reputation: 5108

I think your questions is similar to How does one implement Coq?. At least I'm tempted to give a similar answer.

I think MetaCoq is the state-of-the-art effort to specify and (partially) verify the Coq kernel: https://github.com/MetaCoq/metacoq. It is initially a library for meta-programming in Coq and as such implements a representation of the kernel inside Coq. It has evolved a lot and now contains the typing rules of (a subset of) Coq as well as formalisation of several meta-theoretical properties, a type-checker and an erasure mechanism.

Now understanding your question: The Coq reference manual already offers some sort of specification of the Calculus of Inductive Constructions, which should always be up to date with the latest version of Coq.

The MetaCoq Project paper also attempts a specification of the predicative calculus of cumulative inductive constructions (PCUIC). You seem to think that this somehow might have less value than a paper specification when done in the proof assistant itself, obviously I do not exactly think so (but I'm one of the authors, I'm biased). This is a fair concern, but at least as far as the specification is concerned, it only makes it much more precise than could be done on paper. The Coq reference manual can be imprecise at times. Our work also forces us to explicit invariants of representations that are not enforced in ocaml. Also we separate implementation and specification (the Coq reference manual is pretty implementation oriented). Arguably more works need to be done on this separation.

Otherwise, usually people treat subsets of these calculi, espcially regarding inductive types which are rather painful to lay out entirely.

Upvotes: 2

Related Questions