Tail-Recursive, Linear-Time Fibonacci
July 12, 2008
How can I introduce accumulating parameters to derive the linear-time, tail recursive implementation of
[More ...]
- 2 Comments
Tags: Fibonacci, Program Derivation.
Research Blog of 穆信成 Shin-Cheng Mu
July 12, 2008
How can I introduce accumulating parameters to derive the linear-time, tail recursive implementation of
[More ...]
- 2 Comments
Tags: Fibonacci, Program Derivation.
July 11, 2008
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.
[PDF]
[More ...]
- 0 Comments
Tags: Agda, Dependent Type, Program Derivation.
May 27, 2008
Prove the following property in point-free style:
[More ...]
- 0 Comments
Tags: Program Derivation.
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.
[More ...]
- 0 Comments
Tags: Agda, Dependent Type, Program Derivation, Termination.
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.
[More ...]
- 0 Comments
Tags: Agda, Dependent Type, Program Derivation.
February 10, 2008
Back in 2003, my colleagues there were discussing about the third homomorphism theorem — if a function
[More ...]
- 1 Comments
Tags: List Homomorphism, Program Derivation.
November 26, 2007
Given an interpreter of a small language, derive a virtual machine and a corresponding compiler
[More ...]
- 5 Comments
Tags: Program Derivation.
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]
[More ...]
- 0 Comments
Tags: Program Derivation, Segment Problems.
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…
[More ...]
- 2 Comments
Tags: Agda, Program Derivation, Segment Problems.
October 8, 2007
Any preorder
[More ...]
- 0 Comments
Tags: Program Derivation, Thinning Theorem.