Many programming languages identify modular units with compilation units, while only few extend this to permit hierarchies of language-level modules within individual compilation units. But when the number of such compilation units is large, then it becomes increasingly important that they themselves can be grouped together and that explicit export interfaces can be used to control namespaces.
When there are many groups, then one may want to organize them into supergroups, and so on. I explain how the group model implemented in SML/NJ's compilation manager CM provides the necessary facilities to avoid unwanted interferences between unrelated parts of large programs. I also discuss the problem of automatic dependency analysis as well as its complexity and show ways of avoiding intractability.
This talk will describe the formal verification of EROS security. We constructed a formal model of the EROS kernel, called Agape. Agape specifies the behaviour of all the kernel calls available to EROS processes. We then formally defined the security policies of EROS and showed that these policies reflect the actual system executions. For example, if a process was not given permission to write to a certain disk page, there must be no execution in which that process did so, either directly or via intermediates.
In the process of this work we have uncovered some implementation errors. Our methodology has been designed to be applicable to any capability-based system, and to aid in the design of similar systems.
This is joint work with Jonathan Shapiro.
I present in this talk an ML library that simplifies the task of programming reactive systems. A reactive system can be viewed as a system that continuously react to its environment, a task traditionally not handled very well by transformational programming language. The library provides facilities for defining control points in expressions, and combinators to act on those expressions by directing the flow of control from control points to control points.
The library is currently used as a target language for an experimental higher-level synchronous language, part of a user interface toolkit John Reppy and I are developing.
We give a static semantics in which type checking is done once and for all before the first stage, and a dynamic semantics which introduces a new concept of cross-stage persistence, which requires that variables available in any stage are also available in all future stages.
We illustrate that staging is a manual form of binding time analysis. We explain why, even in the presence of automatic binding time analysis, explicit annotations are useful, especially for programs with more than two stages.
A thesis of this paper is that multi-stage languages are useful as programming languages in their own right, and should support features that make it possible for programmers to write staged computations without significantly changing their normal programming style. To illustrate this we provide a simple three stage example, and an extended two-stage example elaborating a number of practical issues.
This is joint work with my advisor Tim Sheard.