Index of /users/moore/acl2/v3-4/distrib/acl2-sources/books/powerlists

Icon  Name                    Last modified      Size  Description
[DIR] Parent Directory                             -   
[   ] Makefile                17-Dec-2007 09:58  1.2K  
[   ] algebra.acl2            17-Dec-2007 09:58   47   
[TXT] algebra.lisp            17-Dec-2007 09:58   43K  
[   ] batcher-sort.acl2       17-Dec-2007 09:58   52   
[TXT] batcher-sort.lisp       17-Dec-2007 09:58   35K  
[   ] bitonic-sort.acl2       17-Dec-2007 09:58   52   
[TXT] bitonic-sort.lisp       17-Dec-2007 09:58  4.6K  
[TXT] certify.lsp             17-Dec-2007 09:58  1.4K  
[   ] cla-adder.acl2          17-Dec-2007 09:58   49   
[TXT] cla-adder.lisp          17-Dec-2007 09:58   12K  
[   ] defpkg.lisp             17-Dec-2007 09:58  1.3K  
[   ] gray-code.acl2          17-Dec-2007 09:58   49   
[TXT] gray-code.lisp          17-Dec-2007 09:58  8.1K  
[   ] merge-sort.acl2         17-Dec-2007 09:58   50   
[TXT] merge-sort.lisp         17-Dec-2007 09:58  8.4K  
[   ] prefix-sum.acl2         17-Dec-2007 09:58   49   
[TXT] prefix-sum.lisp         17-Dec-2007 09:58   27K  
[   ] simple.acl2             17-Dec-2007 09:58   46   
[TXT] simple.lisp             17-Dec-2007 09:58  7.2K  
[   ] sort.acl2               17-Dec-2007 09:58   44   
[TXT] sort.lisp               17-Dec-2007 09:58  6.7K  

This directory contains some events related to Misra's theory of
powerlists (see Misra's paper "Powerlists: A Structure for Parallel
Recursion" in ACM Transactions on Programming Languages and Systems
(TOPLAS), November 1994).  In essense, powerlists are lists with
constructors and destructors designed to operate well with divide and
conquer parallel algorithms.  These constructors build a new powerlist
L from a pair of powerlists L1 and L2 of equal length.  The length of
the new powerlist L will be twice the length of L1 (equivalently twice
the length of L2).  Misra proposes two such constructors, namely tie
and zip: Tie constructs L by placing the elements of L2 after the
elements of L1, and zip constructs L by shuffling the elements of L1
and L2.

All the books here were created by Ruben Gamboa and are described in
his paper, "Defthms About Zip and Tie," (UTCS tech report TR97-02) and
in his dissertation (University of Texas, Austin, May 1999).  A
version of the paper was also submitted to JAR, but it appears to have
vanished into a black hole.

This directory contains the following books:

    * defpkg.lisp	    -- Defines the powerlist package.
    * algebra.lisp	    -- Basic theory of powerlists.
    * simple.lisp	    -- Easy theorems about powerlists,
			       mostly examples from Misra's paper.
    * sort.lisp		    -- Proof obligations for a sort routine.
    * merge-sort.lisp	    -- Proof of the correctness of an abstract 
			       merge sort.
    * batcher-sort.lisp	    -- A proof of correctness of the Batcher
			       sort.  This proof departs from the one
			       given by Misra in significant ways.
    * bitonic-sort.lisp	    -- A proof of the correctness of a
			       particular instance of bitonic sort,
			       closely following Misra's proof.
    * gray-code.lisp	    -- Properties of a gray code generator,
			       based on Misra's proof.
    * prefix-sum.lisp	    -- Proof of various parallel prefix sum 
			       algorithms.  This departs significantly 
			       from Misra's proof.
    * cla-adder.lisp	    -- Solution to a challenge posed by Misra,
			       to use the results about prefix sums to 
			       show the correctness of a
			       carry-lookahead adder.