coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert "coqchk" and prove anything
chronological Thread
- From: Stéphane Glondu <steph AT glondu.net>
- To: Georges Gonthier <gonthier AT microsoft.com>
- Cc: Bruno Barras <bruno.barras AT inria.fr>, "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert "coqchk" and prove anything
- Date: Wed, 04 May 2011 13:49:31 +0200
Le 04/05/2011 13:20, Georges Gonthier a écrit :
[...] Also coqchk should have an option to trace the assumptions under which
the file is checked. [...]
It has (-o).
Cheers,
--
Stéphane
- [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert "coqchk" and prove anything, guninski
- Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert "coqchk" and prove anything, Stéphane Glondu
- <Possible follow-ups>
- Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert "coqchk" and prove anything,
Bruno Barras
- RE: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert "coqchk" and prove anything,
Georges Gonthier
- Re: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert "coqchk" and prove anything, Stéphane Glondu
- RE: [Coq-Club] hostile plugin hidden inside big archive with proofs can subvert "coqchk" and prove anything,
Georges Gonthier
Archive powered by MhonArc 2.6.16.