The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

> Thorsten Altenkirch wrote:
>
> How detailed is the semantics for the rest of Coq? (This is a serious 
> question).

I would also be interested in some answer / pointers on this. E.g. has the 
work described in the 1997 "Coq in Coq" paper by Bruno Barras and Benjamin 
Werner been taken further? In 2014 there was the paper "Towards a Formally 
Verified Proof Assistant" by Abhishek Anand and Vincent Rahli on the 
formalization of Nurpl in Coq. I would appreciate some pointers on research 
done in this direction.

Of cause one can discuss how worthwhile it is to formalize the metatheory of 
a language in itself, but for those working with Coq it would at least serve 
as a thorough documentation.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Prof. Dr. Hermann Eul
Chairperson of the Supervisory Board: Tiffany Doon Silva
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928