Skip to content

Latest commit

 

History

History
77 lines (51 loc) · 2.79 KB

README.md

File metadata and controls

77 lines (51 loc) · 2.79 KB
Raw

This is a github repository containing Aaron Stump's Iowa Agda Library (IAL) (for those of us who don't use svn and wish to obtain IAL using github).

The original IAL distribution is available at

https://svn.divms.uiowa.edu/repos/clc/projects/agda/ial-releases/

This software is protected under the MIT license. See the LICENSE.txt file included with this repository.

The Iowa Agda Library (IAL)

Author: Aaron Stump

  1. About the library
    The goal is to provide a concrete library focused on verification examples, as opposed to mathematics. The library has a good number of theorems for booleans, natural numbers, and lists. It also has trees, tries, vectors, and rudimentary IO. A number of good ideas come from Agda's standard library.

  2. Using the library
    This library works with Agda Release Candidate 2.5.1. If you are using an older version of Agda, try version 1.2.

    Starting with Agda 2.5.1, to use the library you must add it to your Agda libraries. On linux, create the directory ~/.agda, and add a file called "libraries" to it, containing the full path to the .agda-lib file contained in this directory (for the IAL version 1.3). Then create a file called "defaults", and add the word "IAL" to it (no quotes). These steps tell Agda where the IAL library is, and that you want to include it when opening .agda files in emacs (or with the command-line tool).

    In Agda, you can include the whole library by importing lib.agda.

    You can compile the whole library by running "make".

    The library is set up so there are no name conflicts between modules (except sometimes I have several versions of the same module, like stream and stream2 or nat-division and nat-division2, and there might be name conflicts in such cases).

  3. Browsing the library
    You can get some overview of what is in the library by following imports from lib.agda (this is the main entry point for the library).

  4. Credits
    The library is mostly written by myself, but it also includes some contributions from John Bodeen, Harley Eades, and undergraduates who took my Programming Language Concepts class, Spring 2014 and 2015, especially Tom Werner.

  5. Releases

    Released versions of the library can be found at

    https://svn.divms.uiowa.edu/repos/clc/projects/agda/ial-releases

    The development version is at

    https://svn.divms.uiowa.edu/repos/clc/projects/agda/ial

  6. License

    This library is currently provided under the MIT License, see LICENSE.txt.

  7. Documentation

    There is no formal documentation currently, besides comments in the files.

    Much of the library is described in my book, "Verified Functional Programming in Agda", published 2016 with ACM Books.