Jerome Simeon
Jerome Simeon
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 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...
The code documentation is scattered at the moment. The README now points to querycert.github.io for documentation. We should have a well understood process to produce documentation, and a clear entry...
Currently, there is only a SQL++ AST (in `./coq/SQLPP/Lang/SQLPP.v`), but no associated semantics. It would be nice to provide a clean semantic foundation for SQL++, along with a proof of...
Currently, there is only a SQL AST (in `./coq/SQL/Lang/SQL.v`), but no associated semantics. It would be nice to provide a clean semantic foundation for SQL, along with a proof of...
Q*cert includes type checkers for most of the languages. However, this still requires to _guess_ a type derivation. It would be useful to support some kind of type inference in...
The main data structure for both records and environments are bindings (in `Utils/Bindings.v`). A couple of things could be improved: - The internal representation (association lists, sorted without duplicates) bleeds...