coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Gallina evaluator that plows thru stuck proofs?

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Gallina evaluator that plows thru stuck proofs?
Date: Wed, 9 Aug 2017 15:46:23 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua0-f170.google.com
Ironport-phdr: 9a23:Tr1NfB9CSIdIyf9uRHKM819IXTAuvvDOBiVQ1KB42u8cTK2v8tzYMVDF4r011RmSDNWds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2e2//57ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/mhikEKjA37n3Yh9dsjK5Huh+tuwBzz5LWbYyTKfFwfrndfdQfRWdZQsteTCxBAoKnb4sPEeUBPvtTopX7p1QUqxuxGBSnCeT1xTBThn/23LY60+Q/HgHFxgAvBdQOv27SrNroLqsSUOG1zLXHzTjYYPNW3C3y6InMchw7vf6MWrdwfNPXxEIyGQ3FiVCQppbkPzOTzukCr2+b7/BmVe2xj24nrxt9rSayyccxjITCm4Ebykjc+Cln3Io4Ice0RU17bNK+DpdcqiOXO5FrTs4gX21lvjsxxKcctp6hZicKzYwqxx7BZPyDdIiF+hfjW/yQITd8nX5lZaiwiwqr/Uiu1+HxVNW43ExFripCldnMuXQN2ALJ5sebTft9+1+t2TeJ1w/N9uFJOV44mbbfJpI7wbM9loAfvVreEiL0gkn6ka2belk89uit8evnY7HmppGGN49zjwHzKr4hlde/AeQ5KQgOX3aU+eem2LL5+032WrNKgeAsnqnYsZDaOcsbq7W2Aw9QyIkj6hK/Ay2639QfmHkLNEhFdw6fj4j1J1HOJ+j1Auu4g1S1iTtk2/TGPqD6DZjWNXjCkLLhfa5n5EJGyQozy8pf55NOBb0bLvLzQBy5iNuNBRggdgew3uyvXN56z8YVXX+FKq6fKqLb91GSsLEBOe6JMaYfuDfmK/Umr9fohHk10QsUd6moxpsaazaxGP1gLwOYYGbjqtgEGGYO+AE5Sbq52xW5TTdPaiPqDOoH7TYhBdf+AA==

I am wondering whether someone has written a more lenient version of
vm_compute (or native_compute) that plows through stuck proofs,
similar to the way extracting to OCaml and then evaluating would.

I understand that such an evaluator may in general diverge and produce
results that disagree
with Coq's reduction semantics. However, it seems possible to have the
evaluator
agree with the result of evaluating the OCaml extract, at least for
programs of "simple" non-propositional types such as nat.

Thanks,
-- Abhishek
http://www.cs.cornell.edu/~aa755/

[Coq-Club] Gallina evaluator that plows thru stuck proofs?, Abhishek Anand, 08/09/2017
- Re: [Coq-Club] Gallina evaluator that plows thru stuck proofs?, Guillaume Melquiond, 08/10/2017