Sharon Curtis and Shin-Cheng Mu. Journal of Functional Programming, Vol. 25, 2015.
[Paper (doi: 10.1017/S095679681500026X)| Supplementary Proofs | Code]

The problem of finding a densest segment of a list is similar to the well-known maximum segment sum problem, but its solution is surprisingly challenging. We give a general specification of such problems, and formally develop a linear-time online solution, using a sliding window style algorithm. The development highlights some elegant properties of densities, involving partitions that are decreasing and all right-skew.

The Code

The accompanying Haskell programs and Agda proofs are available on GitHub:
https://github.com/scmu/mds
The Haskell program consists of the following files:

• FDSList.hs: a main program that, for expository purpose, represents sequences by lists.
• FDSSeq.hs: a linear-time implementation of the algorithm, using refined data structures as described in the paper.
• ProbMDS.hs: problem specification for the MDS problem. To be imported by FDSList.hs or FDSSeq.hs.
• ProbMMS.hs: problem specification for the MMS problem. To be imported by FDSList.hs or FDSSeq.hs.
• MDSTest.hs: QuickCheck tests for the MDS problem.
• MMSTest.hs: QuickCheck tests for the MMS problem.