A Generic Type System for Featherweight Java
We introduce a generic type system for Featherweight Java (FJ) that is parametrized with a monad-like structure, and prove a uniform soundness theorem. Its instances include some region type systems studied by Martin Hofmann et al. as well as a new one that performs more precise analysis of trace-based properties. Their soundness is guaranteed by the uniform theorem. We only need to verify some natural conditions. Instead of refining the FJ type system as in the previous work, our region type system is separate from the FJ type system, making it simpler and also easier to move to larger fragments of Java. Moreover, the uniform framework helps to avoid redundant work on the meta-theory when extending the system to cover other language features such as exception handling.
Tue 13 JulDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
14:00 - 16:35 | |||
14:00 5mTalk | Welcome FTfJP | ||
14:05 30mTalk | Refactoring traces to identify concurrency improvements FTfJP | ||
14:35 30mTalk | A Generic Type System for Featherweight Java FTfJP | ||
15:05 30mTalk | Source code patches from dynamic analysis FTfJP | ||
15:35 30mTalk | Reconstructing Z3 Proofs in KeY: There and Back Again FTfJP P: Wolfram Pfeifer Karlsruhe Institute of Technology (KIT), Jonas Schiffl , Mattias Ulbrich Karlsruhe Institute of Technology File Attached | ||
16:05 30mTalk | Using Dafny to Solve the VerifyThis 2021 Challenges FTfJP P: Marie Farrell University of Liverpool, Rosemary Monahan National University of Ireland, A: Conor Reynolds Maynooth University |