This paper formalizes the folklore result that strongly-typed applets are more secure than untyped ones. We formulate and prove several security properties that all well-typed applets possess, and identify sufficient conditions for the applet execution environment to be safe, such as procedural encapsulation, type abstraction, and systematic type-based placement of run-time checks. These results are a first step towards formal techniques for developing and validating safe execution environments for applets.

We present the extensional polymorphism, a framework to type check ad hoc polymorphic functions. This formalism is compatible with parametric polymorphism, and supports a large class of functions defined by structural pattern matching on types.

We present a functional language featuring a form of dynamic overloading akin to message passing in object oriented languages. We give a dynamic semantics describing a non-deterministic evaluation, as well as a type discipline (static semantics) supporting type inference. The type system ensures that a well-typed program has a correct execution, unique up to a semantic equivalence relation, and allows this execution to proceed deterministically, while resolving overloading at run-time.