http://www.rubrication.net Annotations concerning art, science and life. Fri, 14 May 2010 07:56:28 +0000 http://backend.userland.com/rss092 en I've been working with System F quite a bit lately, as it has a complicated enough typing system to be interesting, without having the full insanity of dependent types. I've been working with System F including sums products and recursive types. However, all of these can actually be ... http://www.rubrication.net/2010/05/06/system-f-is-amazing/ Standard functional programming languages like Haskell and SML use polymorphic type systems. These type systems however, are not sound. What this means is that the type-systems themselves can not be used to prove properties of the software in the sense of "total correctness". To see that ... http://www.rubrication.net/2009/11/09/type-checking-and-cyclic-proof/ 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/