Higher-Order Symbolic Execution

[auggierose]

On page 3, I see this:

    (define/contract (f x)
    (positive? . âĘŠ . negative?) ; contract
    (* x -1))

Am I missing fonts or does âĘŠ actually mean something?

[groovy2shoes]

I see the same thing, but I think it's supposed to be a rightward arrow, as in a function from positive numbers to negative numbers. At least, that's how it usually appears in the Racket documentation.

[samth]

This is now fixed.

[spdegabrielle]

"it can form the basis of automated verification and bug-finding tools for higher-order programs. "

Does this mean I can verify C++, Haskell, Python, JavaScript & Common Lisp code that uses Higher Order Functions?

[samth]

That's the idea. We've only done it for Racket so far.

[quietplatypus]

How is this different from defunctionalizing and converting to smt backend or prolog engine without higher-order capabilities?

[samth]

Other people have taken that approach, for example the HALO project in Haskell. But the imprecision of the defunctionalizaton often makes it hard to prove the properties you want, especially without static types.

[jsli]

I am looking for papers about converting to prolog backend. Could you name one for me? Thanks.