coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] classical logic and decidability
- Date: Wed, 26 Dec 2012 07:45:42 +0100
Hi,
Thanks for your explanations about decidability. Very interesting,
made me think a lot, I think a true definition of decidability in
Coq should be very complicated, since it implies that we define the
notion of algorithm, and tutti quanti. I think Bruno Barras' thesis
(Coq in Coq) contains this.
--
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/
- [Coq-Club] classical logic and decidability, Daniel de Rauglaudre, 12/21/2012
- Re: [Coq-Club] classical logic and decidability, Adam Chlipala, 12/21/2012
- Re: [Coq-Club] classical logic and decidability, Pierre Courtieu, 12/21/2012
- Re: [Coq-Club] classical logic and decidability, Jean Goubault-Larrecq, 12/21/2012
- Re: [Coq-Club] classical logic and decidability, Daniel de Rauglaudre, 12/26/2012
- Re: [Coq-Club] classical logic and decidability, AUGER Cédric, 12/26/2012
- Re: [Coq-Club] classical logic and decidability, Daniel de Rauglaudre, 12/26/2012
- Re: [Coq-Club] classical logic and decidability, AUGER Cédric, 12/21/2012
Archive powered by MHonArc 2.6.18.