More Web Proxy on the site http://driver.im/

extended-abstract

Teaching algorithms and data structures with a proof assistant (invited talk)

Author:

Tobias NipkowAuthors Info & Claims

CPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs

Pages 1 - 3

https://doi.org/10.1145/3437992.3439910

Published: 20 January 2021 Publication History

Abstract

We report on a new course Verified Functional Data Structures and Algorithms taught at the Technical University of Munich. The course first introduces students to interactive theorem proving with the Isabelle proof assistant. Then it covers a range of standard data structures, in particular search trees and priority queues: it is shown how to express these data structures functionally and how to reason about their correctness and running time in Isabelle.

References

[1]

Andrew W. Appel. Verified Functional Algorithms, volume 3 of Software Foundations. Electronic textbook, 2020. htp://softwarefoundations. cis.upenn.edu.

[2]

Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development. Texts in Theoretical Computer Science. Springer, 2004.

Digital Library

[3]

Jasmin Christian Blanchette, Lukas Bulwahn, and Tobias Nipkow. Automatic proof and disproof in Isabelle/HOL. In C. Tinelli and V. Sofronie-Stokkermans, editors, Frontiers of Combining Systems (FroCoS 2011 ), volume 6989 of Lecture Notes in Computer Science, pages 12-27. Springer, 2011.

[4]

Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Cliford Stein. Introduction to Algorithms, 3rd Edition. MIT Press, 2009. URL: htp://mitpress.mit.edu/books/introduction-algorithms.

Digital Library

[5]

Adam Grabowski, Artur Kornilowicz, and Adam Naumowicz. Mizar in a nutshell. Journal of Formalized Reasoning, 3 ( 2 ): 153-245, 2010. URL: htps://jfr.unibo.it/article/view/ 1980.

[6]

Jay A. McCarthy, Burke Fetscher, Max S. New, Daniel Feltey, and Robert Bruce Findler. A Coq library for internal verification of runningtimes. In Oleg Kiselyov and Andy King, editors, Functional and Logic Programming, FLOPS 2016, volume 9613, pages 144-162. Springer, 2016. URL: htps://doi.org/10.1007/978-3-319-29604-3_10.

[7]

Tobias Nipkow. Winskel is (almost) right: Towards a mechanized semantics textbook. In Vijay Chandru and V. Vinay, editors, Foundations of Software Technology and Theoretical Computer Science, volume 1180 of Lecture Notes in Computer Science, pages 180-192. Springer, 1996. URL: htps://doi.org/10.1007/3-540-62034-6_48.

[8]

Tobias Nipkow. Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects Comput., 10 ( 2 ): 171-186, 1998. URL: htps://doi.org/10.1007/s001650050009.

Digital Library

[9]

Tobias Nipkow. Teaching semantics with a proof assistant: No more LSD trip proofs. In Viktor Kuncak and Andrey Rybalchenko, editors, Verification, Model Checking, and Abstract Interpretation, VMCAI 2012, volume 7148 of Lecture Notes in Computer Science, pages 24-38. Springer, 2012. URL: htps://doi.org/10.1007/978-3-642-27940-9_3.

[10]

Tobias Nipkow. Verified root-balanced trees. In Bor-Yuh Evan Chang, editor, Programming Languages and Systems, APLAS 2017, volume 10695, pages 255-272. Springer, 2017. URL: htps://doi.org/10.1007/978-3-319-71237-6_13.

[11]

Tobias Nipkow, Jasmin Blanchette, Manuel Eberl, Peter Lammich, Christian Sternagel, Bohua Zhan, et al. Verified functional data structures and algorithms. To appear, 2021.

[12]

Tobias Nipkow, Manuel Eberl, and Maximilian P. L. Haslbeck. Verified textbook algorithms-A biased survey. In Dang Van Hung and Oleg Sokolsky, editors, Automated Technology for Verification and Analysis, ATVA 2020, volume 12302 of Lecture Notes in Computer Science, pages 25-53. Springer, 2020. URL: htps://doi.org/10.1007/978-3-030-59152-6_2.

[13]

Tobias Nipkow and Gerwin Klein. Concrete Semantics with Isabelle/HOL. Springer, 2014. htp://concrete-semantics.org.

[14]

Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle/HOL-A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002.

[15]

Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, 1998.

[16]

Benjamin C. Pierce. Lambda, the ultimate TA: using a proof assistant to teach programming language foundations. In Graham Hutton and Andrew P. Tolmach, editors, Proc. 14th ACM SIGPLAN international conference on Functional programming, ICFP 2009, pages 121-122. ACM, 2009. URL: htps://doi.org/10.1145/1596550.1596552.

Digital Library

[17]

Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Catalin Hritcu, Vilhelm Sjöberg, Andrew Tolmach, and Brent Yorgey. Programming Language Foundations, volume 2 of Software Foundations. Electronic textbook, 2020. htp://softwarefoundations.cis.upenn.edu.

[18]

Markus Wenzel. Isabelle/ Isar-A Versatile Environment for HumanReadable Formal Proof Documents. PhD thesis, Institut für Informatik, Technische Universität München, 2002.

Cited By

Jacobsen FVilladsen J(2023)On Exams with the Isabelle Proof AssistantElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.375.6375(63-76)Online publication date: 10-Mar-2023
https://doi.org/10.4204/EPTCS.375.6
Ehimwenma KWang JZheng ZZhou H(2022)A symbolic-arithmetic for teaching double-black node removal in red-black treesEducational Dimension10.31812/educdim.762959(112-129)Online publication date: 11-Dec-2022
https://doi.org/10.31812/educdim.7629
Villadsen JJacobsen F(2022)Using Isabelle in Two Courses on Logic and Automated ReasoningFormal Methods Teaching10.1007/978-3-030-91550-6_9(117-132)Online publication date: 1-Jan-2022
https://doi.org/10.1007/978-3-030-91550-6_9

Index Terms

Teaching algorithms and data structures with a proof assistant (invited talk)
1. Applied computing
  1. Education
2. Software and its engineering

Recommendations

Programming and verifying a declarative first-order prover in Isabelle/HOL

We certify in the proof assistant Isabelle/HOL the soundness of a declarative first-order prover with equality. The LCF-style prover is a translation we have made, to Standard ML, of a prover in John Harrison’s Handbook of Practical Logic and Automated ...
Foundational extensible corecursion: a proof assistant perspective
ICFP 2015: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming

This paper presents a formalized framework for defining corecursive functions safely in a total setting, based on corecursion up-to and relational parametricity. The end product is a general corecursor that allows corecursive (and even recursive) calls ...
Foundational extensible corecursion: a proof assistant perspective
ICFP '15

This paper presents a formalized framework for defining corecursive functions safely in a total setting, based on corecursion up-to and relational parametricity. The end product is a general corecursor that allows corecursive (and even recursive) calls ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs

January 2021

342 pages

ISBN:9781450382991

DOI:10.1145/3437992

Program Chairs:
Cătălin Hriţcu,
Andrei Popescu

Copyright © 2021 Owner/Author.

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 January 2021

Check for updates

Author Tags

Qualifiers

Extended-abstract

Conference

CPP '21

Sponsor:

SIGPLAN

CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs

January 17 - 19, 2021

Virtual, Denmark

Acceptance Rates

Overall Acceptance Rate 18 of 26 submissions, 69%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
139
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)2

Reflects downloads up to 24 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Jacobsen FVilladsen J(2023)On Exams with the Isabelle Proof AssistantElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.375.6375(63-76)Online publication date: 10-Mar-2023
https://doi.org/10.4204/EPTCS.375.6
Ehimwenma KWang JZheng ZZhou H(2022)A symbolic-arithmetic for teaching double-black node removal in red-black treesEducational Dimension10.31812/educdim.762959(112-129)Online publication date: 11-Dec-2022
https://doi.org/10.31812/educdim.7629
Villadsen JJacobsen F(2022)Using Isabelle in Two Courses on Logic and Automated ReasoningFormal Methods Teaching10.1007/978-3-030-91550-6_9(117-132)Online publication date: 1-Jan-2022
https://doi.org/10.1007/978-3-030-91550-6_9

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents