Chen-Mou Cheng, Ruey-Lin Hsu and Shin-Cheng Mu. In Functional and Logic Programming (FLOPS), John Gallagher and Martin Sulzmann, editors, pp 68-83, 2018.
Sharon Curtis and Shin-Cheng Mu. Calculating a linear-time solution to the densest segment problem. 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.
Around 2 years ago, for an earlier project of mine (which has not seen its light yet!) in which I had to build a language with variables and prove its properties, I surveyed a number of ways to handle binders. For some background, people have noticed that, when proving properties about a language with bound …
I was puzzled by the fact stated in a number of places that axiom of choice, proof irrelevance, and extensional equality together entail the law of excluded middle.
In a recent meeting I talked to my assistants about using dependent type to guarantee that, in an evaluator for λ calculus using de Bruin indices, that variable look-up always succeeds.