'Type Checking Versus Flow Logics'

Studenteropgave: Kandidatspeciale og HD afgangsprojekt

  • Lars Hornbæk Jensen
  • Bjørn Mølgård Vester
4. semester, Datalogi, Kandidat (Kandidatuddannelse)
'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.'
Udgivelsesdatojun. 2006
ID: 61068032