Verify algebra using a prover

w3c / sparql-dev

SPARQL dev Community Group

https://w3c.github.io/sparql-dev/

Other

121 stars 18 forks source link

Verify algebra using a prover #123

Open namedgraph opened 3 years ago

namedgraph commented 3 years ago

Why?

Formal provers are used to verify the correctness of programs and mathematical proofs.

Previous work

Cosette: An Automated Prover for SQL

Proposed solution

Write down SPARQL algebra using the Lean prover

Considerations for backward compatibility

None

ericprud commented 3 years ago

That paper is cool as hell 'cause it has practical implications for optimizers and query rewriters. They used Coq + Rosette to find bugs in deployed code and prove query equivalence, two capabilities which would could improve SPARQL implementations.

You could probably reuse their join semantics for both BGPs and joins, and all of aggregation, so I guess you'd have a fair amount to show after modelling triple patterns (though property paths might be tricky).

akuckartz commented 3 years ago

http://cosette.cs.washington.edu