SeLINQ: Tracking Information across Application-Database Boundaries

Full version of paper

This version includes the soundness proof for the type system.
Full paper

Code of the implementation

The code of the implementation is available at the following link. See README.md in the archive for build and usage instructions.
Code