# Agda

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

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

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