'Type Checking Versus Flow Logics'
Translated title
Authors
Term
4. term
Education
Publication year
2006
Submitted on
2012-02-14
Abstract
'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.'
Documents