Tag Archives: Program Derivation

Maximally Dense Segments — Code and Proof

Code and proof accompanying our forthcoming paper Functional Pearl: Maximally Dense Segments.

Posted in Software | Also tagged | Leave a comment

A Survey of Binary Search

If you think you know everything you need to know about binary search, but have not read Netty van Gasteren and Wim Feijen’s note The Binary Search Revisited, you should.

Posted in Research Blog | Also tagged | 5 Comments

A “Side-Swapping” Lemma Regarding Minimum, Using Enriched Indirect Equality

If every solution returned by D is no better than some solution returned by X, any optimal solution by X must be no worse than some optimal solution by D “What? How could this be true?” It turned out that the reasoning can be correct, and the proof uses indirect equality in an unusual way.

Posted in Research Blog | Also tagged , | Leave a comment

Determining List Steepness in a Homomorphism

A list of numbers is called steep if each element is larger than the sum of elements to its right. It is an example we often use when we talk about tupling. Can we determine the steepness of a list by a list homomorphism?

Posted in Research Blog | Also tagged | 8 Comments

The Windowing Technique for Longest Segment Problems

Reviewing Zantema’s “windowing” technique for computing the longest segment of the input that satisfies a suffix-closed predicate.

Posted in Research Blog | Also tagged , | Leave a comment

Longest Segment Satisfying Suffix and Overlap-Closed Predicates

Translating Zantema’s work to Bird-Meertens style, to compute the longest consecutive segment of the input that satisfies a predicate that is suffix and overlap-closed.

Posted in Research Blog | Also tagged , | Leave a comment

On a Basic Property for the Longest Prefix Problem

Giving a constructive proof for one of the essential properties in Hans Zantema’s Longest Segment Problems.

Posted in Research Blog | Also tagged , | Leave a comment

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]

Posted in Journal | Also tagged , , | Leave a comment

Tail-Recursive, Linear-Time Fibonacci

How can I introduce accumulating parameters to derive the linear-time, tail recursive implementation of fib.

Posted in Research Blog | Also tagged | 2 Comments

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]

Posted in Conference | Also tagged , | Leave a comment