October 2, 2008
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.
[More ...]
- 0 Comments
Tags: Agda, Dependent Type, Termination.
September 28, 2008
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.
[More ...]
- 0 Comments
Tags: Agda, Dependent Type, Termination.
September 24, 2008
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.
[More ...]
- 0 Comments
Tags: Agda, Dependent Type, λ calculus.
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.
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.
April 20, 2008
Given a relation < that has been shown to be well-founded, we know that a recursively defined function is terminating if its arguments becomes “smaller” with respect to < at each recursive call. We can encode such well-founded recursion in Agda’s style of structural recusion.
[More ...]
- 2 Comments
Tags: Agda, Dependent Type, Termination.
April 13, 2008
After seeing our code, Nils Anders Danielsson suggested two improvements. Firstly, to wrap the bound in the seed. Secondly, to define unfoldT↓ using well-founded recursion.
[More ...]
- 0 Comments
Tags: Agda, Dependent Type, Termination.
April 8, 2008
I hope to come up with a variation of unfoldr which, given a proof of well-foundedness, somehow passes the termination check.
[More ...]
- 0 Comments
Tags: Agda, Dependent Type, 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.
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.