Index of /users/moore/acl2/books/books/powerlists

Icon  Name                    Last modified      Size  Description
[DIR] Parent Directory                             -   
[   ] Makefile                18-Jan-2004 09:59  1.2K  
[   ] algebra.acl2            05-Jun-2000 09:33   47   
[TXT] algebra.lisp            25-Jan-2004 10:25   43K  
[   ] batcher-sort.acl2       05-Jun-2000 09:35   52   
[TXT] batcher-sort.lisp       18-Jan-2004 14:23   35K  
[   ] bitonic-sort.acl2       05-Jun-2000 09:35   52   
[TXT] bitonic-sort.lisp       18-May-2000 16:47  4.6K  
[TXT] certify.lsp             01-Jan-1999 08:41  1.4K  
[   ] cla-adder.acl2          05-Jun-2000 09:35   49   
[TXT] cla-adder.lisp          18-May-2000 16:47   12K  
[   ] defpkg.lisp             05-Jun-2000 09:32  1.3K  
[   ] gray-code.acl2          05-Jun-2000 09:35   49   
[TXT] gray-code.lisp          04-Feb-1999 13:09  8.1K  
[   ] merge-sort.acl2         05-Jun-2000 09:36   50   
[TXT] merge-sort.lisp         15-Sep-2003 11:40  8.4K  
[   ] prefix-sum.acl2         05-Jun-2000 09:36   49   
[TXT] prefix-sum.lisp         14-Oct-2001 18:36   27K  
[   ] simple.acl2             05-Jun-2000 09:35   46   
[TXT] simple.lisp             18-May-2000 16:47  7.2K  
[   ] sort.acl2               05-Jun-2000 09:36   44   
[TXT] sort.lisp               06-May-2000 12:27  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.