Byron Cook, of Terminator fame, has just been looking at using F# in conjunction with the Z3 theorem prover, a great new .NET and native component out of Microsoft Research Redmond.

Recent work onF#'s math libraries, together with the latest release ofZ3make for a pretty powerful mixture. In particular I find it interesting that its so easy to combine the polymorphic matrix code support together with the power of Z3. To play around with F#'s new matrix syntax and the new release of Z3 I decided to re-implement the rank function synthesis engine used withinTERMINATOR. The result turned out to be so concise that I thought it would be interesting to the larger F# community. ...

At the high-level we're going to build a tool that takes in a mathematical relation represented as the conjunction of linear inequalities....

It's a really beautiful piece of work, and read all about it over on Byron's blog.

PingBack from http://www.christian.luiscorreia.com/making-use-of-fs-math-libraries-together-with-z3/

F# extensions can install on Visual Studio 2008?