The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

I'm not very familiar with the Coq implementation, so I won't comment
on that, but I would like to point out that your link to Idris
verifier is very incomplete. TT.hs defines the formal language of the
kernel (in around 950 lines), but does not implement its verifier,
which should rather be found at:
  https://github.com/edwinb/Idris-dev/blob/master/src/Core/Typecheck.hs
(around 200 lines)
  which depends on
  https://github.com/edwinb/Idris-dev/blob/master/src/Core/Evaluate.hs
(around 800 lines)

The Matita team wrote an article about a compact implementation of a
kernel for CiC, that could be a basis for comparison (and details the
design choices and architecture). "A compact kernel for the calculus
of inductive constructions", by Asperti, Ricciotti, Sacerdoti Coen and
Tassi, in 2009. It says the whole implementation is around 2300 lines,
which is in the same ballpark.


On Sun, Sep 8, 2013 at 1:31 PM, t x 
<txrev319 AT gmail.com>
 wrote:
> As a followup to this thread:
> https://sympa.inria.fr/sympa/arc/coq-club/2013-05/msg00071.html
>
> I recently installed the Idris language, and was pleasantly surprised to
> find that it's core verifier is only 1000 LOC:
> https://github.com/edwinb/Idris-dev/blob/a76627e7a62cd0816001017439523d491c4c9e8d/src/Core/TT.hs
>
> In Coq, is there is a corresponding *.ml file that does the checking when I
> type in "Qed." ?
> (and if not, is there some toy project that implements a minimal verifier?)
>
> I'm not looking for unification / inference / notation / ltac. Nor am I
> interested in various proofs -- just the very core "dumb/minimal" verifier
> that verifiers the terms generated.
>
> Thanks!