Verified functional programming in Agda / (Record no. 359)
[ view plain ]
| 000 -LEADER | |
|---|---|
| fixed length control field | 05459nam a2200613 a 4500 |
| 001 - CONTROL NUMBER | |
| control field | 011452841316 |
| 003 - CONTROL NUMBER IDENTIFIER | |
| control field | MOCL |
| 005 - DATE AND TIME OF LATEST TRANSACTION | |
| control field | 20260528133338.0 |
| 006 - FIXED-LENGTH DATA ELEMENTS--ADDITIONAL MATERIAL CHARACTERISTICS | |
| fixed length control field | m eo d |
| 007 - PHYSICAL DESCRIPTION FIXED FIELD--GENERAL INFORMATION | |
| fixed length control field | cr cn |||m|||a |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION | |
| fixed length control field | 160219s2016 nyu fob 000 0deng d |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| Canceled/invalid ISBN | 9781970001273 |
| Qualifying information | hardcover |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| Canceled/invalid ISBN | 9781970001242 |
| Qualifying information | paperback |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| International Standard Book Number | 9781970001259 |
| Qualifying information | ebook |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| Canceled/invalid ISBN | 9781970001266 |
| Qualifying information | ePub |
| 024 7# - OTHER STANDARD IDENTIFIER | |
| Standard number or code | 10.1145/2841316 |
| Source of number or code | doi |
| 035 ## - SYSTEM CONTROL NUMBER | |
| System control number | (CaBNVSL)swl00406212 |
| 035 ## - SYSTEM CONTROL NUMBER | |
| System control number | (OCoLC)939937303 |
| 040 ## - CATALOGING SOURCE | |
| Original cataloging agency | CaBNVSL |
| Language of cataloging | eng |
| Description conventions | rda |
| Transcribing agency | CaBNVSL |
| Modifying agency | CaBNVSL |
| 050 #4 - LIBRARY OF CONGRESS CALL NUMBER | |
| Classification number | QA76.62 |
| Item number | .S788 2016 |
| 082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER | |
| Classification number | 005.13 |
| Edition information | 23 |
| 100 1# - MAIN ENTRY--PERSONAL NAME | |
| Personal name | Stump, Aaron., |
| Relator term | author. |
| 245 10 - TITLE STATEMENT | |
| Title | Verified functional programming in Agda / |
| Statement of responsibility, etc. | Aaron Stump. |
| 250 ## - EDITION STATEMENT | |
| Edition statement | First edition. |
| 264 #1 - PRODUCTION, PUBLICATION, DISTRIBUTION, MANUFACTURE, AND COPYRIGHT NOTICE | |
| Place of production, publication, distribution, manufacture | [New York] : |
| Name of producer, publisher, distributor, manufacturer | Association for Computing Machinery ; |
| Place of production, publication, distribution, manufacture | [San Rafael, California] : |
| Name of producer, publisher, distributor, manufacturer | Morgan & Claypool, |
| Date of production, publication, distribution, manufacture, or copyright notice | 2016. |
| 300 ## - PHYSICAL DESCRIPTION | |
| Extent | 1 PDF (xxiv, 258 pages) |
| 336 ## - CONTENT TYPE | |
| Content type term | text |
| Source | rdacontent |
| 337 ## - MEDIA TYPE | |
| Media type term | electronic |
| Source | isbdmedia |
| 338 ## - CARRIER TYPE | |
| Carrier type term | online resource |
| Source | rdacarrier |
| 490 1# - SERIES STATEMENT | |
| Series statement | ACM books, |
| International Standard Serial Number | 2374-6777 ; |
| Volume/sequential designation | #9 |
| 538 ## - SYSTEM DETAILS NOTE | |
| System details note | Mode of access: World Wide Web. |
| 538 ## - SYSTEM DETAILS NOTE | |
| System details note | System requirements: Adobe Acrobat Reader. |
| 504 ## - BIBLIOGRAPHY, ETC. NOTE | |
| Bibliography, etc. note | Includes bibliographical references (pages 253-256) and index. |
| 505 8# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 9. Reasoning about termination -- 9.1 Termination proofs -- 9.2 Operational semantics for SK combinators -- 9.3 Conclusion -- Exercises -- |
| 505 8# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 3. Natural numbers -- 3.1 Peano natural numbers -- 3.2 Addition -- 3.3 Multiplication -- 3.4 Arithmetic comparison -- 3.5 Even/odd and mutually recursive definitions -- 3.6 Conclusion -- Exercises -- |
| 505 8# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 5. Internal verification -- 5.1 Vectors -- 5.2 Binary search trees -- 5.3 Sigma types -- 5.4 Braun trees -- 5.5 Discussion: internal vs. external verification -- 5.6 Conclusion -- Exercises -- |
| 505 8# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 7. Generating Agda parsers with gratr -- 7.1 A primer on grammars -- 7.2 Generating parsers with gratr -- 7.3 Conclusion -- Exercises -- |
| 505 8# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 4. Lists -- 4.1 The list datatype and type parameters -- 4.2 Basic operations on lists -- 4.3 Reasoning about list operations -- 4.4 Conclusion -- Exercises -- |
| 505 8# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 2. Introduction to constructive proof -- 2.1 A first theorem about the Booleans -- 2.2 Universal theorems -- 2.3 Another example, and more on implicit arguments -- 2.4 Theorems with hypotheses -- 2.5 Going deeper: Curry-Howard and constructivity -- 2.6 Further examples -- 2.7 Conclusion -- Exercises -- |
| 505 8# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 8. A case study: Huffman encoding and decoding -- 8.1 The files -- 8.2 The input formats -- 8.3 Encoding textual input -- 8.4 Decoding encoded text -- 8.5 Conclusion -- Exercises -- |
| 505 0# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 1. Functional programming with the Booleans -- 1.1 Declaring the datatype of Booleans -- 1.2 First steps interacting with Agda -- 1.3 Syntax declarations -- 1.4 Defining Boolean operations by pattern matching: negation -- 1.5 Defining Boolean operations by pattern matching: and, or -- 1.6 The if-then-else operation -- 1.7 Conclusion -- Exercises -- |
| 505 8# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 6. Type-level computation -- 6.1 Integers -- 6.2 Formatted printing -- 6.3 Proof by reflection -- 6.4 Conclusion -- Exercises -- |
| 505 8# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | Appendix A. Quick guide to symbols -- Appendix B. Commonly used Emacs control commands -- Appendix C. Some extra Emacs definitions -- References -- Index -- Author's biography. |
| 505 8# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 10. Intuitionistic logic and Kripke semantics -- 10.1 Positive propositional intuitionistic logic (PPIL) -- 10.2 Kripke structures -- 10.3 Kripke semantics for PPIL -- 10.4 Soundness of PPIL -- 10.5 Completeness -- 10.6 Conclusion -- Exercises -- |
| 520 3# - SUMMARY, ETC. | |
| Summary, etc. | Agda is an advanced programming language based on Type Theory. Agda's type system is expressive enough to support full functional verification of programs, in two styles. In external verification, we write pure functional programs and then write proofs of properties about them. The proofs are separate external artifacts, typically using structural induction. In internal verification, we specify properties of programs through rich types for the programs themselves. This often necessitates including proofs inside code, to show the type checker that the specified properties hold. The power to prove properties of programs in these two styles is a profound addition to the practice of programming, giving programmers the power to guarantee the absence of bugs, and thus improve the quality of software more than previously possible. The book begins with an introduction to functional programming through familiar examples like booleans, natural numbers, and lists, and techniques for external verification. Internal verification is considered through the examples of vectors, binary search trees, and Braun trees. More advanced material on type-level computation, explicit reasoning about termination, and normalization by evaluation is also included. The book also includes a medium-sized case study on Huffman encoding and decoding. |
| 530 ## - ADDITIONAL PHYSICAL FORM AVAILABLE NOTE | |
| Additional physical form available note | Also available in print. |
| 588 ## - SOURCE OF DESCRIPTION NOTE | |
| Source of description note | Title from PDF title page (viewed on February 19, 2016). |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name entry element | Agda (Computer program language) |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name entry element | Functional programming languages. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name entry element | Type theory. |
| 776 08 - ADDITIONAL PHYSICAL FORM ENTRY | |
| Relationship information | Print version: |
| International Standard Book Number | 9781970001273 |
| -- | 9781970001242 |
| 830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE | |
| Uniform title | ACM books ; |
| Volume/sequential designation | #9. |
| International Standard Serial Number | 2374-6777 |
| 856 48 - ELECTRONIC LOCATION AND ACCESS | |
| Materials specified | Abstract with links to full text |
| Uniform Resource Identifier | <a href="http://dl.acm.org/citation.cfm?id=2841316">http://dl.acm.org/citation.cfm?id=2841316</a> |
No items available.