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.
Research
Agda Approximation Bidirectional Updating Burrows-Wheeler Transform Concurrency Converse-of-a-Function Theorem Curry-Howard Data Structure Dependent Type Fibonacci GADT Galois Connection Greedy Theorem Haskell HaXML Imperative Programs Indirect Equality List Homomorphism Logic Logic Programming Optimisation Problems Program Derivation Program Inversion Quantum Programming Quine Regular Expression Segment Problems Termination Thinning Theorem Types XML Streaming λ calculusRecent Comments
- Matt on A Survey of Binary Search
- Shin on The Maximum Segment Sum Problem: Its Origin, and a Derivation
- Shin on The Maximum Segment Sum Problem: Its Origin, and a Derivation
- minime on Beamer Article Mode Does Not Save Paper?
- wren ng thornton on Proving the Church-Rosser Theorem Using a Locally Nameless Representation