'Type Checking Versus Flow Logics'

Student thesis: Master Thesis and HD Thesis

  • Lars Hornbæk Jensen
  • Bjørn Mølgård Vester
4. term, Computer Science, Master (Master Programme)
'In this project we examine the relationship between control flow analysis and type checking. We develop a typed version of the LySa calculus using correspondence assertions, as well as an accompanying type system. We construct an encoding from processes with crypto-points in LySa to Typed LySa, and show that they have equivalent safety properties. Type inference is performed on the encoded process under a series of constraints. Lastly a new control flow analysis is created using correspondence assertions instead of crypto-points.'
Publication dateJun 2006
ID: 61068032