coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Survey Paper

From: Tobias Nipkow <nipkow AT in.tum.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] Survey Paper
Date: Mon, 19 Oct 2020 08:21:01 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=nipkow AT in.tum.de; spf=Pass smtp.mailfrom=nipkow AT in.tum.de; spf=None smtp.helo=postmaster AT mail-out2.informatik.tu-muenchen.de
Ironport-phdr: 9a23:prfvTxVRQZizdBd7OYsFSzPiHQ3V8LGtZVwlr6E/grcLSJyIuqrYbBeFt8tkgFKBZ4jH8fUM07OQ7/m/HzNYqs/Z6jgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrrwjdrMsbjZdtJqos1hfFvGZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+2zRl8d+jr9UoAi5qhJhw4DafYKbOvRwcazSYdwXXmVBUtpLWiFdHo+xYYkCAuwcNuhYtYn9oF4OoAOgCwmrH+zvyyVHhmTr1qMi0uQhCQLG3AsuHtkTt3nUqtT1NL8RUeCywqjF1jTDb/VM1Tfh9YjIdwotruySUr9pd8fa1EYgGR/fgFqKtYzlIy2a1v4Ls2WD6+dtSeaihnM6pgxsvDSi2sQhh5TUi48LyV3I6Ct3zJsoKNC4VkJ2YNqpHpVOuyyeOYV7Q80sTW91tCg0yrALtpi2dzUExpQgwh7Qcf2Hc46Q7xL9UuaRPC10i2x4d7KinRqy706gx+vhXce3yFZHtjdJn9fRunwXyhDe6syKRuFh8ku71zuC1gbe4fxeL08uj6rUMZshz6YwlpUNtUTDGTf7mEDsg6+XckUo4++o6/n7Yrn4vJOcNol0ig/5MqQ0n8ywG/g4MgkNX2SB5eS8yaTv/UjkQLpUiP05jqnZv47cJcgBu6G2HRdZ0ocl6xmhEzeryMkUkHcaIF5fZR6Kj4zkN0vSLPziA/qygkygkDJxyPDHOr3hDI/NLn/GkLr5e7Z96lZcyAk0zdFR/J9UC7cBLOjvWk/ssdzUFAI2PBKsz+b9FNp9zp8eWX6IAqKBLKzStkaI6vszLOmIeY8aoy3wK+Ml5v7rlX82g0URfaiv3ZsNaXC3BO5qI0uDYSmkvtBUGmAT+wE6UebCiVuYUDcVaWzhcbg742QHD4inBJyLYIG1g7uelHO9H4VVYX9uC1bKDWrtMYmJDaRfIBmOK9Nsx2RXHYOqTJUsgEn35V3KjoF/J++RwRU28Jfq1dx7/erWzEhg9DoyE9mYlW2AHTgtwzE4AgQu1aU6mnRTj1eO1a8j3K5dHN1XovRUTl18NJjSyPZ/AszzWUTdY5KMVVugSdWrB3c9Q4BpmoNcUwNGA9ynyyv78W+yGbZMzu6KAtoo76ea03Wjf8s=

Dear All,

You may be interested in this new survey paper:

-------------------------------------------------------------------------
Verified Textbook Algorithms. A Biased Survey
Tobias Nipkow, Manuel Eberl, Maximilian P. L. Haslbeck

This article surveys the state of the art of verifying standard textbook algorithms. We focus largely on the classic text by Cormen et al. Both correctness and running time complexity are considered.
-------------------------------------------------------------------------

It is an invited ATVA 2020 paper. The ATVA proceedings are freely available online http://fit.uet.vnu.edu.vn/atva2020/ for 4 weeks.

Enjoy!
Tobias

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

[Coq-Club] Survey Paper, Tobias Nipkow, 10/19/2020