Hybrid Enforcement and Certification of Domain Specific Program Annotations (DesignerTypeLab)
Insecure software systems cost society heavily in terms of financial loss and privacy violations. Existing techniques for improving the safety and security of software systems go beyond what is offered by ordinary programming languages. These approaches address concerns such as access control or information flow, resource usage, and architectural properties like ownership, using extra program annotations expressing domain-specific type systems. Properties expressed in these systems can be enforced using a hybrid of static and dynamic checks.
Many domain specific type systems exist. Unfortunately, developing the desired meta-theory and toolset for such systems requires a considerable amount of effort. In order to increase the impact of and the confidence in such domain specific type systems, the DesignerTypeLab project will develop a unified and general framework and associated toolset which will offer full lifecycle support for type system design and debugging, formal verification of the type system's meta-theory, automatically generated (hybrid) checking algorithms, and support for reasoning about programs written using a particular domain specific type system.