Properties of a Computational Lambda Calculus for Higher-Order Relational Queries

We study the operational semantics of an untyped computational lambda calculus whose normal forms represent queries on databases. The calculus extends the computational core with additional operations and rewriting rules whose effect is to turn the monadic type of computations into a multiset monad that captures tables. Moreover, we introduce comonadic constructs and additional rewriting rules to be able to form tables of tables. Proving confluence becomes tricky: we succeed exploiting decreasing diagrams. In the second part, we study a Curry style type assignment system for the calculus. We introduce an idempotent intersection type system establishing type invariance under conversion.