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 ...]
- 0 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.
September 28, 2007
This time I am implementing the example in another section of Why Dependent Types Matter by Altenkirch, McBride, and McKinna in Agda: proving that mergesort returns an ordered list.
[More ...]
- 2 Comments
Tags: Agda, Dependent Type.
September 27, 2007
Continuing with my Adga programming practice. Part of the mergesort example became easy once Max showed me how I should perform the pattern matching in insert.
[More ...]
- 4 Comments
Tags: Agda, Dependent Type.
September 19, 2007
During the WG 2.1 meeting, my attention was brought to Agda. So, here is my first Agda program. I am merely repeating some simple exercises on lists, which I tried using Haskell in a previous entry Developing Programs and Proofs Spontaneously using GADT.
[More ...]
- 2 Comments
Tags: Agda, Curry-Howard, Dependent Type.
August 6, 2007
I am curious about the possibility of developing Haskell programs spontaneously with proofs about their properties and have the type checker verify the proofs for us, in a way one would do in a dependently typed language. I tried to redo part of the merge-sort example in Altenkirch, McBride, and McKinna’s introduction to Epigram: deal the input list into a binary tree, and fold the tree by the function merging two sorted lists into one.
[More ...]
- 3 Comments
Tags: Curry-Howard, Dependent Type, GADT, Haskell, Types.