http://www.rubrication.net Annotations concerning art, science and life. Thu, 28 Feb 2008 11:19:03 +0000 http://backend.userland.com/rss092 en I was playing around with the Peano numerals in Haskell (as I often do), because I remember briefly reading about a generalisation of exponentiation in a paper once when I didn't have time to read it. I decided I'd quickly look at it again now that I was in ... http://www.rubrication.net/2008/02/27/the-co-natural-numbers/ A while ago I wrote a post about how one can use coq to make a proper monad module. I was just thinking today that it would be nice to have a tool for haskell that would allow one to write down conjectures and discharge them automatically with a ... http://www.rubrication.net/2008/02/09/verifying-the-monad-laws-with-supercompilation/ Program transformation is a sort of meta-compilation where the source and target languages are the same. In this sense it can be seen as an automorphism on the set of programs in a language. As was pointed out by Turchin, it is sometimes possible to prove properties of programs simply ... http://www.rubrication.net/2008/01/26/proof-by-program-transformation/ I've mentioned a number of times that given a sufficiently rich type theory we can use the type to provide a specification for the function, such that the function is correct by construction. I'd like to give a simple example of how this works in the Coq proof assistant. The ... http://www.rubrication.net/2007/04/24/strong-specifications/ In my last post I described how unbelievably cool modules are in Coq. Well it turns out that there is some disagreement in the community about whether one should even use them! Why? Because the type system in Coq is so powerful we hardly even need them. ... http://www.rubrication.net/2007/04/21/we-dont-need-no-stinking-modules/ I've been playing with the Coq proof assistant over the past few days, following closely on some frustrations that I've been having with using SML's module system and a bit of toying with type-classes in Haskell. The gist of the problem is this. Although you can define type-classes and modules ... http://www.rubrication.net/2007/04/21/how-a-real-module-system-should-work/ A few months ago I started messing around with The Coq Proof Assistant to figure out what exactly it was, and proceeded to go through the tutorial. Coq provides a nice interface for doing proofs in an interactive session. It was a lot of fun but didn't seem particularly useful ... http://www.rubrication.net/2007/03/07/coq/ The following is some SML code that implements the natural numbers using peano arithmetic in the SML type system. These numbers can be used to protect access to list functions. I haven't yet figured out if addition is possible, but I'm hoping that it is. It could ... http://www.rubrication.net/2007/02/28/protected-access-using-lightweight-capabilities/ I just got "ML for the working programmer" in the mail a few days ago, and worked through it at a breakneck pace since receiving it. It turns out that a lot of the stuff from the "Total Functional Programming" book is also in this one. Paulson goes through the use of ... http://www.rubrication.net/2007/02/03/automated-deduction-and-functional-programming/ Recently on Lambda the Ultimate there was a post called "Total Functional Programming". The title didn't catch my eye particularly, but I tend to read the abstract of any paper that is posted there that doesn't sound terribly boring. I've found that this is a fairly good strategy ... http://www.rubrication.net/2007/01/26/total-functional-programming/