Cover Image

Verified functional programming in Agda /

Bibliographic Details
Main Author: Stump, Aaron (Author)
Format: eBook
Language:English
Published: [New York] : [San Rafael, California] : Association for Computing Machinery ; Morgan & Claypool, 2016.
Edition:First edition.
Series:ACM books ; #9.
Subjects:
Agda (Computer program language)
Functional programming languages.
Type theory.
Electronic data.
Online Access:Connect to the full text of this electronic book
Table of Contents:
  • 9. Reasoning about termination
  • 9.1 Termination proofs
  • 9.2 Operational semantics for SK combinators
  • 9.3 Conclusion
  • Exercises
  • 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
  • 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
  • 7. Generating Agda parsers with gratr
  • 7.1 A primer on grammars
  • 7.2 Generating parsers with gratr
  • 7.3 Conclusion
  • Exercises
  • 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
  • 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
  • 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
  • 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
  • 6. Type-level computation
  • 6.1 Integers
  • 6.2 Formatted printing
  • 6.3 Proof by reflection
  • 6.4 Conclusion
  • Exercises
  • Appendix A. Quick guide to symbols
  • Appendix B. Commonly used Emacs control commands
  • Appendix C. Some extra Emacs definitions
  • References
  • Index
  • Author's biography.
  • 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