Principia Narcissus: How to Avoid Being Caught by Your Reflection

Some modern, statically typed programming languages provide the capability for programs to reflect, or introspect, upon their type meta-data at runtime. Using type meta-data to determine program behavior is called type-directed programming (TDP). Type-directed programming allows many operations on data, such as serialization, cloning, structural equality, and general iteration, to be defined naturally, just once, for all types of data. Consequently, these operations continue to work as systems grow and software is extended with additional data types. Without TDP, programmers must constantly revise the code that implements these operations and scatter their implementations throughout their code-base. However, TDP conflicts with the use of abstract data types (ADTs), a fundamental technique in the practice of software engineering. The benefits of using ADTs derive from the fact that their definitions are hidden; however, with TDP, abstract type meta-data becomes no more hidden than abstracted values (often called variables) in standard programming. In this dissertation, I show how TDP and ADTs can be reconciled through the use of information-flow type and kind systems. I begin by introducing the problem as well as my definitions for the properties I call confidentiality and integrity. Next, I develop the theoretical foundation for reasoning statically about confidentiality and integrity in programs that use TDP, and show how information-flow type and kind systems generalize prior techniques. I then describe a realistic programming language, InforML, with an information-flow type and kind system. After introducing the InforML language, I describe idioms for programming in InforML and the reasoning principles for confidentiality and integrity that are a consequence of using these idioms. Finally, I discuss the implementation of InforML and the most important design decisions made while implementing InforML.