## 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.

Skip to content
# Agda

## Functional pearl: folding polynomials of polynomials

## Calculating a linear-time solution to the densest segment problem

## Proving the Church-Rosser Theorem Using a Locally Nameless Representation

## No Inverses for Injective but Non-Surjective Functions?

## Proof Irrelevance, Extensional Equality, and the Excluded Middle

## Algebra of programming in Agda: dependent types for relational program derivation

## “General Recursion using Coinductive Monad” Got Right

## General Recursion using Coindutive Monad

## Typed λ Calculus Interpreter in Agda

## Algebra of programming using dependent types

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 …

Proving the Church-Rosser Theorem Using a Locally Nameless Representation Read More »

“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?

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.

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]

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.

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.

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.

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]