search

abau / co4

COmplexity COncerned COnstraint COmpiler
GNU General Public License v3.0
2 stars 3 forks source link

README.md: Fix unbound identifiers #106

Closed Blaisorblade closed 10 years ago

Blaisorblade commented 10 years ago

encMain and main are not currently described — both the README and the actual program use encConstraint and constraint. It took me a while to figure out what was happening.

abau commented 10 years ago

so I had no clue what the code snippet meant

Ah, I see the problem. I merged your fix. Thanks a lot.

It would be cooler if the Template Haskell API accepted the name of the function to convert

Nice idea, I opend an issue for that: https://github.com/apunktbau/co4/issues/107

are there restrictions on k

It must either one of the types you defined in your constraint or either one of CO4's prelude types: so there is now way right now to pass functional value. And unfortunately I don't have a clue how to support that.

Finally: is there any link to any Haddock documentation?

No there was not. But I just uploaded the Haddock documentation to http://www.imn.htwk-leipzig.de/~abau/co4/doc/html/co4/ . I recommend to start with CO4.Solve

Blaisorblade commented 10 years ago

And unfortunately I don't have a clue how to support that.

My PhD is not in verification but in PL (or anyway, in a somewhat different (sub)area from yours), but I still heard of a couple of very good papers which seem relevant.

There's a standard technique to transform higher-order programs to first-order ones, called defunctionalization (introduced by Reynolds). That's used (IIRC) in HALO: haskell to logic through denotational semantics? They use SAT (and/or SMT)-solvers to check if a program satisfies a contract, with both the program and the contract expressed in Haskell, and they do support higher-order functions using (essentially) this technique.

But I've not seen them do synthesis — in that paper, they just produce counterexamples (at most). Instead, this year at PLDI I've seen people use SAT-solvers to produce pieces of programs: http://dl.acm.org/citation.cfm?doid=2594291.2594340 — unfortunately, in this other work higher-order functions are simply inlined away, so they can't be synthesized.