Janis Voigtländer
Skip Abstract Section
Abstract
This pearl develops a statement about parallel prefix computation in the spirit of Knuth's 0-1-Principle for oblivious sorting algorithms. It turns out that 0-1 is not quite enough here. The perfect hammer for the nails we are going to drive in is relational parametricity.
- G. E. Blelloch. Prefix sums and their applications. In J. H. Reif, editor, Synthesis of Parallel Algorithms, pages 35--60. Morgan Kaufmann, 1993.Google Scholar
- S. Böhme. Free theorems for sublanguages of Haskell. Master's thesis, Technische Universität Dresden, 2007a.Google Scholar
- S. Böhme. Much ado about two. Formal proof development. In G. Klein, T. Nipkow, and L. Paulson, editors, The Archive of Formal Proofs. http://afp.sf.net/entries/MuchAdoAboutTwo.shtml, 2007b.Google Scholar
- A. Bove and T. Coquand. Formalising bitonic sort in type theory. In Types for Proofs and Programs, TYPES 2004, Revised Selected Papers, volume 3839 of LNCS, pages 82--97. Springer-Verlag, 2006. Google ScholarDigital Library
- R. P. Brent and H. T. Kung. The chip complexity of binary arithmetic. In ACM Symposium on Theory of Computing, Proceedings, pages 190--200. ACM Press, 1980. Google ScholarDigital Library
- N. A. Danielsson, R. J. M. Hughes, P. Jansson, and J. Gibbons. Fast and loose reasoning is morally correct. In Principles of Programming Languages, Proceedings, pages 206--217. ACM Press, 2006. Google ScholarDigital Library
- N. A. Day, J. Launchbury, and J. Lewis. Logical abstractions in Haskell. In Haskell Workshop, Proceedings. Technical Report UU--CS--1999--28, Utrecht University, 1999.Google Scholar
- P. Dybjer, Q. Haiyan, and M. Takeyama. Verifying Haskell programs by combining testing, model checking and interactive theorem proving. Information & Software Technology, 46(15):1011--1025, 2004.Google ScholarCross Ref
- J. Gibbons and G. Hutton. Proof methods for corecursive programs. Fundamenta Informaticae, 66(4):353--366, 2005. Google ScholarDigital Library
- R. Hinze. An algebra of scans. In Mathematics of Program Construction, Proceedings, volume 3125 of LNCS, pages 186--210. Springer--Verlag, 2004.Google Scholar
- P. Johann and J. Voigtländer. Free theorems in the presence of seq. In Principles of Programming Languages, Proceedings, pages 99--110. ACM Press, 2004. Google ScholarDigital Library
- S. Knowles. A family of adders. In Computer Arithmetic, Proceedings, pages 277--284. IEEE Press, 2001. Google ScholarDigital Library
- D. E. Knuth. The Art of Computer Programming, volume 3: Sorting and Searching. Addison--Wesley, 1973. Google ScholarDigital Library
- R. E. Ladner and M. J. Fischer. Parallel prefix computation. Journal of the ACM, 27(4):831--838, 1980. Google ScholarDigital Library
- Y.-C. Lin and J.-W. Hsiao. A new approach to constructing optimal parallel prefix circuits with small depth. Journal of Parallel and Distributed Computing, 64(1):97--107, 2004. Google ScholarDigital Library
- T. Lynch and E. Swartzlander. The redundant cell adder. In Computer Arithmetic, Proceedings, pages 165--170. IEEE Press, 1991.Google ScholarCross Ref
- T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer-Verlag, 2002. Google ScholarDigital Library
- S. L. Peyton Jones, editor. Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, 2003.Google Scholar
- J. C. Reynolds. Types, abstraction and parametric polymorphism. In Information Processing, Proceedings, pages 513--523. Elsevier Science Publishers B. V., 1983.Google Scholar
- M. Sheeran. Finding regularity: Describing and analysing circuits that are not quite regular. In Correct Hardware Design and Verification Methods, Proceedings, volume 2860 of LNCS, pages 4--18. Springer-Verlag, 2003.Google Scholar
- M. Sheeran. Hardware design and functional programming: a perfect match. Journal of Universal Computer Science, 11(7):1135--1158, 2005.Google Scholar
- M. Sheeran. Searching for prefix networks to fit in a context using a lazy functional programming language. Talk at Hardware Design and Functional Languages, 2007.Google Scholar
- J. Sklansky. Conditional-sum addition logic. IRE Transactions on Electronic Computers, EC-9(6):226--231, 1960.Google ScholarCross Ref
- H. S. Stone and P. M. Kogge. A parallel algorithm for the efficient solution of a general class of recurrence equations. IEEE Transactions on Computers, 22(8):786--793, 1973.Google Scholar
- P. Wadler. Theorems for free! In Functional Programming Languages and Computer Architecture, Proceedings, pages 347--359. ACM Press, 1989. Google ScholarDigital Library
Index Terms
- Much ado about two (pearl): a pearl on parallel prefix computation
Recommendations
Much ado about two (pearl): a pearl on parallel prefix computation
POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesThis pearl develops a statement about parallel prefix computation in the spirit of Knuth's 0-1-Principle for oblivious sorting algorithms. It turns out that 0-1 is not quite enough here. The perfect hammer for the nails we are going to drive in is ...
Bidirectionalization for free! (Pearl)
POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesA bidirectional transformation consists of a function get that takes a source (document or value) to a view and a function put that takes an updated view and the original source back to an updated source, governed by certain consistency conditions ...
All sorts of permutations (functional pearl)
ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional ProgrammingThe combination of non-determinism and sorting is mostly associated with permutation sort, a sorting algorithm that is not very useful for sorting and has an awful running time. In this paper we look at the combination of non-determinism and sorting in ...
Comments