The Ruby Framework

This report describes a framework for the manipulation of Ruby expressions, regarded as terms, and their types. Ruby is here considered as a strongly-typed relational language with a type system which permits dependent types in a stratified system of type universes. The type system is closely related to that of Edinburgh LF, and uses the a similar division of entities into terms, types and kinds. The system is first presented in terms of a set of inference rules for deducing types and kinds from well-formed pseudo-terms. Then a more implementation-oriented formal description is given. This has formed the basis for an actual implementation, on which a number of practical tools have been built up