Abstract

Our objective is to construct a suitable type system for the Erasmus language by understanding the notion of type in programming languages, present a model of typed, polymorphic programming language that reflects recent research in type theory. This type system gives us a strong tool to explain the behavior of this language in a consistent framework by modeling features such as cells, processes, ports, protocols, messages, and message passing, which are the main heart of this programming language. The Erasmus language belongs to process oriented programming languages which is being developed by Peter Grogono at Concordia University and Brian Shearing at The Software Factory in England. This language is mainly based on cells, processes and their interactions and like object oriented languages; it provides both a framework and a motivation for exploring the interaction among the concept of type, data abstraction, and polymorphism. We develop a n-calculus-based model for this type system that allows us to explore these interactions in the simple setting. The evolution of languages from untyped universes to monomorphic and polymorphic type systems is reviewed. Different type systems of different programming languages are discussed and the mechanism for polymorphism such as overloading, coercion, subtyping, protocols satisfaction, and parameterization are also described. The typed n-calculus is augmented to include binding of types by quantification as well as binding types by abstraction. This typed n-calculus is augmented by universal quantification to model generic functions with type parameters, bounded quantification to provide explicit subtype parameters. In this way we obtain a simple and precise characterization of a powerful type system that includes abstract data types, parametric polymorphism, and subtyping relations in a single consistent framework. This augmented typed n-calculus is then used for the type system of the Erasmus language with which we are able to describe the features of this language, and a proof technique that will let us reason about the model