Functional pearl: folding polynomials of polynomials
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.
Agda
Calculating a linear-time solution to the densest segment problem
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.
Proving the Church-Rosser Theorem Using a Locally Nameless Representation
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 …
Proving the Church-Rosser Theorem Using a Locally Nameless Representation Read More »
No Inverses for Injective but Non-Surjective Functions?
“I cannot prove that if a function is injective, it has an inverse,” Hideki Hashimoto posed this question to me. Is it possible at all?
Proof Irrelevance, Extensional Equality, and the Excluded Middle
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.
Algebra of programming in Agda: dependent types for relational program derivation
S-C. Mu, H-S. Ko, and P. Jansson. Algebra of programming in Agda: dependent types for relational program derivation. In Journal of Functional Programming, Vol. 19(5), pp. 545-579. Sep. 2009. [PDF]
“General Recursion using Coinductive Monad” Got Right
Anton Setzer argued in his letter to the Agda mailing list that we should go back to a category theoretical view of codata, and Dan Doel soon successfully experimented the ideas.
General Recursion using Coindutive Monad
It would be nice to if we could write the program and prove its termination separately. Adam Megacz published an interesting paper: A Coinductive Monad for Prop-Bounded Recursion. As a practice, I tried to port his code to Agda.
Typed λ Calculus Interpreter in Agda
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.
Algebra of programming using dependent types
S-C. Mu, H-S. Ko, and P. Jansson. Algebra of programming using dependent types. In Mathematics of Program Construction 2008, LNCS 5133, pp 268-283. July 2008.
Superseded by the extended version for Journal of Functional Programming.
[PDF]