Verified functional programming in Agda / Aaron Stump.

Format:

Book

Author/Creator:

Stump, Aaron, author.

Series:

ACM books.

ACM Bks

Language:

English

Subjects (All):

Computer programming.

Physical Description:

1 online resource (285 pages)

Edition:

First edition.

Place of Publication:

San Rafael, California : Morgan & Claypool, [2016]

Summary:

Verified Functional Programming in Agda is the first book to provide a systematic exposition of external and internal verification in Agda, suitable for undergraduate students of Computer Science. No familiarity with functional programming or computer-checked proofs is presupposed. 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.

Contents:

Contents

Preface

1. Functional Programming with the Booleans

2. Introduction to Constructive Proof

3. Natural Numbers

4. Lists

5. Internal Verification

6. Type-Level Computation

7. Generating Agda Parsers

8. A Case Study: Huffman Encoding and Decoding

9. Reasoning About Termination

10 Intuitionistic Logic and Kripke Semantics

A. Quick Guide to Symbols

B. Commonly Used Emacs Control Commands

C. Some Extra Emacs

References

Index

Author’s Biography Generated by AI.

Notes:

Description based on publisher supplied metadata and other sources.

Description based on print version record.

Includes bibliographical references and index.

Part of the metadata in this record was created by AI, based on the text of the resource.

ISBN:

9781970001266

1970001267

9781970001259

1970001259

OCLC:

1048183371