qcert
qcert copied to clipboard
querycert
Compilation and Verification of Data-Centric Languages
The idea behind the conjecture: Fields on the right of `OpRecConcat` hides corresponding fields that may exist on the left, so the type of those fields on the left do...
Wouldn't it be nice to have an instance of operator (for a given statically known type)? Something that might look like `d instanceof t` If I'm correct, this could be...
This would give us qcert-runtime, and qcert (which could depend on qcert-runtime). This would allow projects to use qcert-runtime as a dependency, and qcert as a dev-dependency, for example.
coqoon
Do we still use the coqoon plugin for eclipse? Is that useful to keep around?
There seem to be a bit of confusion in the way the avoid list collides with the variable or constant names. During code generation, variables get prefixed with `v`. If...
It prefixes all variables emmitted with "v", but the avoidance code does not account for this. As a result, "this", for example, is suffixed to avoid a conflict (needlessly, since...
Currently, the ocaml based native qcert binary has a CLI, but the generated javascript version used in the npm package does not. We should be able to reuse most/all of...
It might be worth cleaning up and consolidating date/time support in JavaScript to use a well-supported library. An example might be [moment.js](https://momentjs.com). Possible issue is that this require node.js for...
Leibnitz equality (eq) equates two collections only if they have the same order. Since we assume collections are bags, we should be using bag equality (equivalence modulo permutation). Note that...
Some of our targets (notably JavaScript and Cloudant) could be deployed on openWhisk (https://openwhisk.incubator.apache.org) instead of being run through 'query runners'. This would provide for an easy way to run...