| Title: | Software Foundation Volume 3: Verified Functional Algorithms |
|---|
PRINT
PDF
WORD
CSV
EXCEL
Moocable is learner-supported. When you buy through links on our site, we may earn an affiliate commission.
Description
In this volume you will learn how to specify and verify (prove the correctness of) sorting algorithms, binary search trees, balanced binary search trees, and priority queues. Before using this book, you should have some understanding of these algorithms and data structures, available in any standard undergraduate algorithms textbook.
This electronic book is Volume 3 of the Software Foundations series, which presents the mathematical underpinnings of reliable software. It builds on Software Foundations Volume 1 (Logical Foundations), but does not depend on Volume 2. The exposition here is intended for a broad range of readers, from advanced undergraduates to PhD students and researchers.The principal novelty of Software Foundations is that it is one hundred percent formalized and machine-checked: the entire text is literally a script for Coq. It is intended to be read alongside an interactive session with Coq. All the details in the text are fully formalized in Coq, and the exercises are designed to be worked using Coq.
Books
University of Pennsylvania
Free 
No Certificate 
300 
Software Foundation Volume 3: Verified Functional Algorithms
Affiliate notice
-
Type
-
Provider
-
PricingFree
-
CertificateNo Certificate
In this volume you will learn how to specify and verify (prove the correctness of) sorting algorithms, binary search trees, balanced binary search trees, and priority queues. Before using this book, you should have some understanding of these algorithms and data structures, available in any standard undergraduate algorithms textbook.
This electronic book is Volume 3 of the Software Foundations series, which presents the mathematical underpinnings of reliable software. It builds on Software Foundations Volume 1 (Logical Foundations), but does not depend on Volume 2. The exposition here is intended for a broad range of readers, from advanced undergraduates to PhD students and researchers.The principal novelty of Software Foundations is that it is one hundred percent formalized and machine-checked: the entire text is literally a script for Coq. It is intended to be read alongside an interactive session with Coq. All the details in the text are fully formalized in Coq, and the exercises are designed to be worked using Coq.
Loading...
Saving...
Loading...