Tag Archives: Program Derivation

A Simple Exercise using the Modular Law

By Shin | Published: May 27, 2008

Prove the following property in point-free style:

S ⊆ C . S     ⇐     R ⊆ C . R   ∧   S ⊆ R
Posted in Research Blog | Tagged | Leave a comment

Well-Foundedness and Reductivity

By Shin | Published: April 25, 2008

It seems that reductivity of Doornbos and Backhouse is in fact accessibility, which is often taken by type theorists to be an alternative definition of well-foundedness.

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

AoPA — Algebra of Programming in Agda

By Shin | Published: March 30, 2008

The AoPA library allows one to encode Algebra of Programming style program derivation, both functional and relational, in Agda, accompanying the paper Algebra of Programming Using Dependent Types (MPC 2008) developed in co-operation with Hsiang-Shang Ko and Patrik Jansson.

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

Constructing List Homomorphism from Left and Right Folds

By Shin | Published: February 10, 2008

Back in 2003, my colleagues there were discussing about the third homomorphism theorem — if a function f can be expressed both as a foldr and a foldl, there exists some associative binary operator ⊚ such that f can be computed from the middle. The aim was to automatically construct ⊚.

Posted in Research Blog | Also tagged , | 1 Comment

Deriving a Virtual Machine

By Shin | Published: November 26, 2007

Given an interpreter of a small language, derive a virtual machine and a corresponding compiler

Posted in Research Blog | Tagged | 5 Comments

Maximum segment sum is back: deriving algorithms for two segment problems with bounded lengths

By Shin | Published: November 13, 2007

S-C. Mu. Maximum segment sum is back: deriving algorithms for two segment problems with bounded lengths. In Partial Evaluation and Program Manipulation (PEPM ’08), pp 31-39. January 2008.
[PDF] [GZipped Postscript]

Posted in Conference | Also tagged , | Leave a comment

Maximum Segment Sum, Agda Approved

By Shin | Published: November 11, 2007

To practise using the Logic.ChainReasoning module in Agda, Josh proved the foldr-fusion theorem, and I thought it would be an small exercise over the weekend to start off where he finished…

Posted in Research Blog | Also tagged , , | 2 Comments

The Pruning Theorem: Thinning Based on a Loose Notion of Monotonicity

By Shin | Published: October 8, 2007

Any preorder R induces a lax preorder ∋ . R. If a relation S is monotonic on R∘, it is monotonic on lax preorder ∋ . R. Furthermore, prune (∋ . R) = thin R. Therefore, pruning is a generalisation of thinning. We need the notion of lax preorders because, for some problems, the generating relation S is monotonic on a lax preorder, but not a preorder.

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

Proving the Thinning Theorem by Fold Fusion

By Shin | Published: October 4, 2007

Prove the thinning theorem by fold fusion. Horrifyingly, I could not do it anymore! Have my skills become rusty due to lack of practice in the past few years?

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

Zipping Half of a List with Its Reversal

By Shin | Published: June 20, 2007

Given a list, zip its first half with the reverse of its second half, in only “one and a half” traversals of the list.

Posted in Research Blog | Also tagged | 4 Comments