Towards an MLstyle Polymorphic

USA email volpanocs nps navy mil Abstract Advanced polymorphic type systems have come to play an important role in the world of functional programming But curiously these type systems have so far had little impact upon widelyused imper ative programming languages like C and C We show that MLstyle polymorphism can be integrated smoothly into a dialect of C which we call Polymorphic C It has the same pointer operations as C includ ing the addressof operator the dereferencing operator and pointer arithmetic Our type system allows these operations in their full gen erality so that programmers need not give up the exibility of C to gain the benets of MLstyle polymorphism We prove a type soundness theorem that gives a rigorous and useful characterization of welltyped Polymorphic C programs in terms of what can go wrong when they are evaluate