Much Ado About Two

Sascha Böhme

Document: Link

Abstract: This article is an Isabelle formalisation of a paper with the same title. In a similar way as Knuth's 0-1-principle for sorting algorithms, that paper develops a "0-1-2-principle" for parallel prefix computations.

Bibtex entry:

@incollection{
  author =    {Sascha B\"ohme},
  title =     {Much Ado About Two},
  booktitle = {The Archive of Formal Proofs},
  editor =    {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
  publisher = {\url{http://afp.sf.net/entries/MuchAdoAboutTwo.shtml}},
  month =     Nov,
  year =      2007,
  note =      {Formal proof development}
}