'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.'