  This paper presents a new approach for optimizing multitheaded programs with
pointer constructs. The approach has applications in the area of certified code
(proof-carrying code) where a justification or a proof for the correctness of
each optimization is required. The optimization meant here is that of dead code
elimination.
  Towards optimizing multithreaded programs the paper presents a new
operational semantics for parallel constructs like join-fork constructs,
parallel loops, and conditionally spawned threads. The paper also presents a
novel type system for flow-sensitive pointer analysis of multithreaded
programs. This type system is extended to obtain a new type system for
live-variables analysis of multithreaded programs. The live-variables type
system is extended to build the third novel type system, proposed in this
paper, which carries the optimization of dead code elimination. The
justification mentioned above takes the form of type derivation in our
approach.
