We have two open positions in formal methods/verification at our team at
Intel:
http://jobs.intel.com/ShowJob/Id/1504155/Sr.-Formal-Verification-Engineer/
While the work centers around formal-verification of Intel's microprocessor
offerings, people with background in functional programming and g
I'm happy to announce a new release of SBV (v4.0); a library for seamlessly
integrating SMT solvers with Haskell.
https://hackage.haskell.org/package/sbv
Most of the changes in this release are due to Brian Huffman of Galois;
essentially adding capabilities so end-users can define symbolic
I'm pleased to announce v3.1 release of SBV, a library for integrating SMT
solvers into Haskell.
This release coincides with GHC 7.8.3: A a prior bug in the 7.8 series
caused SBV to crash under heavy load. GHC 7.8.3 fixes this bug; so if
you're an SBV user, please upgrade to both GHC 7.8.3 and you
Our formal methods team at Intel has a full-time position available that I
think would be a good fit for functional programming and formal methods
enthusiasts. I'm including the description below. Do not hesitate to
contact me if you've any questions, or just want to talk about it in
general. To ap
A new release (v0.5) of hArduno is out, now supporting servo-motors,
shift-registers, seven-segment displays, and distance sensors. Comes with a
bunch of examples to play around with:
http://leventerkok.github.com/hArduino/
On Hackage: http://hackage.haskell.org/package/hArduino
-Levent.
___
I'm happy to announce hArduino: a library that allows Arduino boards to be
controlled directly from Haskell. hArduino uses the Firmata protocol (
http://firmata.org), to communicate with and control Arduino boards, making
it possible to implement many controller projects directly in Haskell.
On Wed, 17 Sep 2003, Brandon Michael Moore wrote:
> > > Don't the laws for loop and mfix justify the transformation?
> >
> > The loop axioms do, but Levent didn't assume right tightening, which
> > corresponds to moving bindings down from a rec, because monads like
> > exceptions don't satisfy it
On Wed, 17 Sep 2003, Brandon Michael Moore wrote:
> The problem with that is that not all monads support recursive bindings.
> We can deal with that, but the desuagring of a do statement wouldn't be so
> trivial any more. The most sensible approach I can think of is to analyze
> the bindings an
> On the necessity of rec syntax, how is a statement like
> do rec binds1
> rec binds2
> stmts
> different from
> do BV1 <- mdo binds1
>return BV1
> BV2 <- mdo binds2
>return BV2
> stmts
> where BVn is a tuple of all the variables bound in bindsn.
On Monday 14 October 2002 09:25 am, you wrote:
> While I'm happy that the fix versions outperform the 2-pass versions for
> boxed arrays, the discrepency between 79.16 seconds for one million
> elements and 4.54 sectons on the same data is alarming. Can anyone
> suggest a way to reconcile this?
On Friday 27 September 2002 05:19 pm, Hal Daume III wrote:
> There is a one pass solution using mfix. This looks like:
>
> mfix (\ ~s -> ioaA a 1 s)
>
> where ioaA is defined as:
>
> ioaA a i s
>
> | i > sz = return 0
> | otherwise =
>
> do s' <- ioaA a (i+1) s
>v
A couple of days ago, Hal Daume III asked
> what does fixST do?
Briefly, fixST allows recursive definitions of values in the ST monad. As
you can guess, there's a bunch of such operators for different monads, the
most famous being "fixIO", the corresponding operator for the IO monad.
These o
On Thursday 25 October 2001 07:21 am, John Hughes wrote:
> My proposal is that := should bind *monomorphically* -- just like lambda
> binding. The motivation for that is that a polymorphic function can easily
> become overloaded after a small change to the program, such as adding
> removal of dupl
How about:
===
data Expr a = Haskell a
| If (Expr Bool) (Expr a) (Expr a)
| forall b . Appl (Expr (b->a)) (Expr b)
| forall b c . MkPair (Expr b) (Expr c) (b -> c -> a)
eval :: Expr a -> a
eval (
> Sorry, this one should be OK:
>
> fixIO m = let
> x = unsafePerformIO (liftM Box (m (unbox x)))
> in return . unbox $! x
Unfortunately, that's not good either: Consider again:
e :: IO Int
e = do { x <- fixIO (\x -> do {putStr "hello"; return (x+1)}); return 2}
If I run e several tim
Marcin 'Qrczak' Kowalczyk wrote:
>
> Fri, 16 Feb 2001 10:01:06 -0800, Levent Erkok <[EMAIL PROTECTED]> pisze:
>
> > The non-strict version is not good either, because it won't do
> > the effects!
>
> data Box a = Box {unbox :: a}
>
>
I recently wrote:
> So, it looks like:
>
> fixIO m = let x = unsafePerformIO (m x) in return x
>
> will do a better job.
But of course, I forgot to make my point before sending the message!
The non-strict version is not good either, because it won't do the
effects!
Consider the definition:
Marcin 'Qrczak' Kowalczyk wrote:
>
> Fri, 16 Feb 2001 04:14:26 -0800, Simon Peyton-Jones <[EMAIL PROTECTED]> pisze:
>
> > fixIO m = do { v <- newEmptyMVar
> >; result <- m (unsafePerformIO (takeMVar v))
> >; putMVar v result
> >; return result }
>
(Apologies to the list: The previous version of this message got out a little
premature, here's the complete version of it..)
Here's the pointer:
http://www.cse.ogi.edu/PacSoft/projects/muHugs/
The paper titled "Recursive Monadic Bindings" explains the ideas. (It also
briefly talks
On Tue, 06 Jun 2000, Koen Claessen wrote:
> Now, obviously there are not that many people who use
> polymorphic let-bindings in do, but I don't think that is a
> reason to introduce this restriction.
I agree. We were just trying to see if such polymorphic
let-generators were used often in practi
Thanks for everyone who participated in the recent poll. Here are the results:
Never used: 6
Sometimes used: 1
Common commments:
willing to give it up for something cool
can be easily rewritten
wouldn't make a lot of difference
not sure if used ever, but wouldn't expect it t
On Sun, 04 Jun 2000, Marcin 'Qrczak' Kowalczyk wrote:
> And "<-"-bound variables would be visible everywhere too?
That's right.
> I'm curious how the generic translation into mfix could look like if
> everything is visible everywhere, e.g.:
> do
> a <- f1 b
> b <- f2 a
>
On Sun, 04 Jun 2000, Koen Claessen wrote:
> You cannot ask a question like this without explaining why
> you are interested in this subject! :-) Just out of
> curiosity... (I think that it is has to do with a recursive
> do-translation, am I right?
Yes, we're working on a new semantics for do, w
ponse is fine too.
Thanks for your time.
John Launchbury & Levent Erkok
Hi,
I've come accross an interesting bit of code:
class X a where
u :: a b -> a b
f :: X a => b -> a b
f = f
g :: X a => a b -> b
g = g
-- h :: X a => b -> a c
h b = f (g (h b))
25 matches
Mail list logo
