Title: Towards A Framework for Soundness Proofs of Type Systems in 
Language-based Information-flow Security

Abstract: In language-based information flow security, type systems 
are often developed as basis for an automatic security analysis of 
programs. It is essential that these type systems are sound, i.e. can 
only type programs that satisfy the wanted notion of security. 
Currently, such soundness proofs are almost always conducted on paper. 
This is error-prone and requires a lot of work.

In the on-going master's thesis with the above title, we aim at 
1) providing a more reliable soundness guarantee for 3 already 
   existing type systems by providing machine-checked soundness proofs 
   using Isabelle/HOL
2) providing means to facilitate the development of soundness proofs

This talk presents intermediate results for the first objective and 
outlines future plans for the second one.