Tag Archives: Dependent Type

Terminating Unfolds (1)

I hope to come up with a variation of unfoldr which, given a proof of well-foundedness, somehow passes the termination check.

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

AoPA — Algebra of Programming in Agda

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

Agda Exercise: Proving that Mergesort Returns Ordered Lists

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.

Posted in Research Blog | Also tagged | 2 Comments

Agda Exercise: Sized Mergesort

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.

Posted in Research Blog | Also tagged | 4 Comments

My First Agda Program: Append, Reverse, and Merge

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.

Posted in Research Blog | Also tagged , | 2 Comments

Developing Programs and Proofs Spontaneously using GADT

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.

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