[ Content | View menu ]

My First Agda Program: Append, Reverse, and Merge

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: , , .

Developing Programs and Proofs Spontaneously using GADT

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: , , , , .