Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Request for the article "Proof Accounts in HOL"

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Request for the article "Proof Accounts in HOL"


Chronological Thread 
  • From: Mario Frank <mafrank AT uni-potsdam.de>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Request for the article "Proof Accounts in HOL"
  • Date: Wed, 15 Jan 2020 13:19:24 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mafrank AT uni-potsdam.de; spf=Pass smtp.mailfrom=mafrank AT uni-potsdam.de; spf=None smtp.helo=postmaster AT cl-mail.uni-potsdam.de
  • Autocrypt: addr=mafrank AT uni-potsdam.de; prefer-encrypt=mutual; keydata= mQINBFoxDJEBEADR2Sq8pVKjj8rhF/ybxsEPg9wXNvpBi13nslcbZEWl6DmuZprwPi4pFU1y nH1PPsTFImbpIQWXdAMlXiBi2QdLW1yvw7Hl9nPYQdnrhiZXYrL7ECslAKVcdZXb/+k3i6h9 B5xBQTPGApPkShWgcIl6bNROxQ7lpq9nWK93z6XRxW01bSKi8FLIBp+zHZvoAgnFbwqa9zv7 n+6MvaOlI1yMf4izFMrd3IrswpciIKCmfiWHzhFsFyi09Wd4I7G3etxbYC9/Eg6vuWJjttYl rjyeQxTSWuIs88eyra0fNPjxRZ/alyVAyx9GDPJMIKTjpx8i8YoA9kh2NtNOrbi9hG6yy/Cs QfRkS47JKkKFGJvGuxxtd/WesqPy2VSzVoqr91LNdn6d8QKHEDJkG8G4Jhl8UovbbBWZ+0oX zdxogAGEDWqcHIWbprb2R21BgsZP40RFsdxvQstn5eKzwSy1A+XBLl8piCeFBeX/1HL4XkTA BuPjuk3Jcct7684J8duLDyWLqbEoboEV7KoNf+uDvQFDt0SYyznVu5w3keulb5BdDAPBFTux U1mBBMOf6Gf6dF7NNeOEPJvytR+8qzeh8OgwO6h8kmxRtxLwOm8Qt/rHitbKlRaikB4buRXu IYxE8YChpClA9cBjyUnoqFbQkGZhiOW9Ywhyb8JcvzjJhfcRCQARAQABtCRNYXJpbyBGcmFu ayA8bWFmcmFua0B1bmktcG90c2RhbS5kZT6JAlcEEwEIAEECGyMFCQlmAYAFCwkIBwIGFQgJ CgsCBBYCAwECHgECF4AWIQQKmKntZdGhu/uI1pptG7hdbe5oSwUCWjENZQIZAQAKCRBtG7hd be5oS8ggD/43a8LyfUFV4lC75MkA98jVpVgwSIK1Qte1D4/bgTALWUVmHrvmwu6bTCOQ6ar5 pmSORdc/xiOM8UR+X6WGgAHV/4/jYMtrwLV0pGP027idEq4fpO68DzlC3xFEFbJTrq9NS7Jn vfIO3fWPNoMs7xBtgcc6I9ynZHEDsYX2YR6xjjBznOsKEVk6sWv/IaechL71qqyzGKPkZOCp vlGzJo84D7XzFC6cHa3eqwSEBPrBGK1HlJSHHk4/hEhThvUkTtroDNbojnfgI90X3qfWLUcZ QRU7AaZtbpProuc+So53stamzlX8o4uO8IkVznwbbC97Gr+XpvP4CFiw6N2gtr3xbDvd5Ekk MIGrZyY22r5WLx3C3ba0ykUMdcyZjtdY72j9BMHsNWpVyUimYvWu3n01ZzVGiwmEiXKAnRVI 59tuHFoB0VIRRy2EqXr/DQw8gB1y2HQVivA/pIWmrrKy99olEHcM6W1gvoWuUZ/FhPogkWv6 YZBx9wScM2Empt06+WqTueSJbhAFRfJmXHoc0niCE4wSmeF0+Pu1VzADm0eXzmxvadYm8iXM TGY22Dcpepyaa1AA4xG0DhmwxO1dxp+XuZvuvt/w8JufM5cFQCSRwIbD4wczjAqRs24l8LSF aI9KVLh3ifzu9OfZhN5xbt1/wWry+xIewC8BkZqOQ/p4HLkCDQRaMQyRARAAy2urmyA86ZX6 /0KymXZCuMFoulPuHiMUxP2Wrbj0jn1vZA7icUDVLlrFkq2FtU2+/tesA/TmeM9zsXN7jGxA je1A/KmwMt+nyqlMde/2kXLvQ3JRckWiyuaoHAFR/B8qzDqy9NApT2cWM85edK6h1LhxCqna XUzRj8NCpXfxq6W4mY+Ey7A2Pf1tWVWWNzMPt1hfaXiY1Q2OMMqkquDUkj0mXxOJfh+SzXh1 LkA5hkPLzIz6RQYgS93ck5Wvbf4WlMqr6MuQNXVbK55jX6h3XJKcHB0P4TM45MDf+CxxApxX sZf1NJKuP0e+GKuMm8f0owdr34l4vWDezwvtLfiagYR15DpGtXs6Eqqy+eYhBrEPg6obrPzZ bHYcBHowASLMv0NqQLtcA5LcT7WxDfAeEVEMmw4eEIGNP0ImE89po9vstKIrvLR8tAwWInqb zUCWNeF80htfDG13phb6VCchefK3b67uwVyA9queR0wj+21txOzm3ZGnI+4browrvpRYiQPw +q01p+8bgF6BQ5qGgI/Qewg7g0qRJ+HAaPBtxW7MsGygGcJCdjhmALz+sAh5pn4JF7MUXcQh v8B9nRpjnnkFKMf5wV39sA4H4WMrQ7ACOdBSG3SrNABs7dc/6omJMEaEZcN7aW1oHDHtzYA7 CwpolaYs+9sjZyeroWrjxiEAEQEAAYkCPAQYAQgAJhYhBAqYqe1l0aG7+4jWmm0buF1t7mhL BQJaMQyRAhsMBQkJZgGAAAoJEG0buF1t7mhL0hcQAKkKx6SyDexz5JXFog3VlADoo8RCvNFS ctuoaqBVTmfljTD4dhRR3Nc0y02xhHu2BKb3XscacdUVV/29G3jaRUGLZKiEpo5DMTrODJAo qrs0VUYkfFBxQXwKEbAppaOcXKbQKi+OFMPGF3sEoO81y6JGm+vym4/OskrHROyduLqTakG0 by9xm8nmCoOulDl7shIbyGaWzaVBXBQPGJIp+JDgOh99ftwe5S8APFn9hYi5YSrJt1iXwGWb 7Fri0Nepsm4cVsVYdecZe6Z8ucDR7rUTzxVS5fgmDPRqJbeZY7g8/nDaD/HN7o03YLpYLWw9 wIA4oHHNcTF6ldErb2kvWbVLxf7WjtnlgFa/MBLKkse8ClJAKXvnYY0vHJwuBn+aVn3ne24X 702Wpt4uKKIHLZaBOgnenS9LYzwRUyUeTY2P4sm4Z+sFBsmT2uC9PW7YJuvuYnMeqpnuMp0N +UCbzr1hm6iw8DEO8HhJaKQCP3kX/nivRpmaWn4MAYBEJfPVx/9GE++CucgmxPgF3fShTACE ANwF/AmPakk5rd1W7Sk7pfYMqw6iMtcVr70590TGX8ZbwVbtfIFBTLYWeThHG3Gn9gwtkV5p 1LgFIdW8M4y244gq6TvtaQ4iHSrXbiwZ6LZ38bCR8lCcz3TY+a5c399ve8KcOdEl1C4m8DhW g4TQ
  • Ironport-phdr: 9a23:J4SnSRB9rmOuWZvtTQl4UyQJP3N1i/DPJgcQr6AfoPdwSPv9osbcNUDSrc9gkEXOFd2Cra4d16yO6Ou7BiRAuc/H7ClZNsQUFlcssoY/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVImbuv6FZTPgMupyuu854PcYxlShDq6fLh+MAi6oR/eu8ULjoZuMLo9xxXGrnZGeeld2GdkKU6Okxrm6cq84ZBu/z5Mt/498sJLTLn3cbk/QbFEFjotLno75NfstRnNTAuP4mUTX2ALmRdWAAbL8Q/3UI7pviT1quRy1i+aPdbrTb8vQjSt871rSB7zhygZMTMy7XzahdZxjKJfpxKhugB/zovJa4ybKPZyYqXQds4cSGFcXMheSjZBD5uhYYURAeoPPeVWoYfzqFQBrxSxGRKhBOzzxjJSmnL6waM33uYnHArb3AIgBdUOsHHModvyLqgSS+G1zK7VxjvDdfNZwzH96IvVeR0mpPGDR7xwcdDLxkkpFAPIlUiQqYrkPz+MzuQNtHSb7/F9Wu21jm4rsRx+rSa2y8oql4LHhZoVx0jZ+Sh23Yo5P961RUphbdOlE5ZcrTyWO5NrTs4tXm1koiU3x7kctZO7ciUG0okryh/dZvGBboOG+AjsVPyLLjd9nH9leKywhxK18UW41uL8UtC40FNQoSpEltnArG0N1xrS6sSeUvt9+Vuh2S2S2A/J7+FIO107mrTDJ54gxL4/iIYTvFzeEiL5hUn6lqybe0E+9uWp6OnreKjqqoeZN4BuiwH+Nqoumta4AeQ9KgUOWnKU+eqm1LL5+035Q65HjuAwkqnYqZzaPcMbprKiAwBIyIkj7gyzACq439gAh3kIMEpFeA6bj4juI1zBPPf4De6mj1uwlDdr2uvJM6b6ApTNK3jDiK3ucax8605a0gozzMpQ64haCrEbc7rPXRr6s8WdBRskOSS1xfzmAZNzzNAwQ2WKV4qQKqLV+XGS7+Qsa72JbYEPsTD+A+Uj5rv2imMilVYYO6Wki8hEIEukF+hrdh3KKUHnhc0MRD9T71gOCdfygVjHagZ9InO7XqYy/DY+Udz0EIHCA5iqnKeN1SL9EpAEPzkaWGDJKm/hcsC/Y9lJcDibe5EzjzoFEKCmV5Qt3BTouAKok+M6fNqRwTURsNfY7PYw5+DXkktupzdwSsGU0mXLUmd123sPWyQ61aU5rUEvklo=

Dear Coq users and implementors,

a colleague of mine and I are interested in reading the article "Proof
Accounts in HOL"
by Avra Cohn from 1988 that was referenced in "Extracting Text from
Proofs" by
Yann Coscoy, Gilles Kahn and Laurent Théry, for example.

Sadly, this article was an unpublished (and seemingly unfinished) draft
and is not available
on the internet anymore.

We already queried Laurent who currently is not able to help us. Since
we would like to
potentially cover the contents of the article in an article we want to
submit soon, we are
searching for someone who can provide us this draft.

Does anyone of you either have access to this article or is able to
point us to the right person?

Thank you in advance and best regard
Mario


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature




Archive powered by MHonArc 2.6.18.

Top of Page