Sciweavers

Share
JFP
2008

Types and trace effects of higher order programs

9 years 10 months ago
Types and trace effects of higher order programs
This paper shows how type effect systems can be combined with model-checking techniques to produce powerful, automatically verifiable program logics for higher order programs. The properties verified are based on the ordered sequence of events that occur during program execution, so-called event traces. Our type and effect systems infer conservative approximations of the event traces arising at run-time, and model-checking techniques are used to verify logical properties of these histories. Our language model is based on the -calculus. Technical results include a type inference algorithm for a polymorphic type effect system, and a method for applying known model-checking techniques to the trace effects inferred by the type inference algorithm, allowing static enforcement of history- and stack-based security mechanisms. A type safety result is proven for both unification and subtyping constraint versions of the type system, ensuring that statically well-typed programs do not contain tr...
Christian Skalka, Scott F. Smith, David Van Horn
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2008
Where JFP
Authors Christian Skalka, Scott F. Smith, David Van Horn
Comments (0)
books