This work was supported by funding from the topic Engineering Secure Systems of the Helmholtz Association (HGF) and by KASTEL Security Research Labs. It was also supported by a Mitacs Globalink Research Award for the project "Scalable Verification of Imperative Programs". This work was supported by the KIT International Excellence Fellowships Program with funds granted to the University of Excellence concept of Karlsruhe Institute of Technology.

This package contains the implemenation and evaluation for our paper of the same title. To build and execute our type checker, see the `README.md` in the main directory. To replicate our evaluations, see the `README.md`s in the subdirectories `daikon_case_study` and `web_shop_case_study`.