One of the goals of the new language paradigms aspect-orientation and collaboration-based programming is the development of security-critical applications.

The underlying theory is still developing while practical examples of languages like AspectJ grow ever new extensions by language elements and program-constructors.

The goal of this project is to apply interactive theorem proving with Higher Order Logic (HOL) to analyze the new language paradigms, for example with respect to type safety, but also other security properties like non-interference and confinement. Starting from a small base language and its semantics we analyze by adding various language constructs step by step while observing whether they respect safety properties.

We use either Coq or Isabelle/HOL to develop a mechanized HOL model. From the formalization we can generate compilers and type checkers that may serve as reference implementation and test-oracles.