Generating Collection Transformations from Proofs
summary
A procedure converts constructive proofs of functionality for bounded delta0 specifications into concrete nested relational calculus programs, running in polynomial time by traversing a normalized sequent proof and producing an NRC interpolant that uses only shared variables; it handles nested sets, tupling, singleton and big-union, and supports extracting inverses or cached computations. A non-constructive model-theoretic argument guarantees existence of NRC implementations from classical proofs but gives no efficient algorithm. A Coq formalization is underway.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 0:23Problem Statement
- 8:30Intuitionistic Proofs
- 16:12Generalization
- 17:05Conclusion
- 18:02General Results
- 18:54Future Work
related talks
18mTranslating canonical SQL to imperative code in Coq
22mFormalization of a Proof Calculus for Incremental Linearization for Satisfiability(…)
38mThe Intensional-Extensional Problem in Probabilistic Databases
01h 05mAlgebraic Structures in Logic and Query Evaluation 2
36mOptimizing Relational Programs II
24mWhen Less Is More: Consequence-Finding in a Weak Theory of Arithmetic
41mOptimizing Relational Programs I
05mRelational Programming