The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

I agree this information should be clearly available in the documentation/FAQ.
The parts that are not well-described/developed could make good
(PhD-)student topics.

I could try to collect some references here, but the coqdevs are in a
better position for that.

Bas


On Wed, Jul 15, 2015 at 9:34 AM, Soegtrop, Michael
<michael.soegtrop AT intel.com>
 wrote:
>> 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
>