My research spans several domains involving the development of safe and secure software.

Enterprise Security

My most recent research has been looking at how to secure the ends of the "pipe" in a distributed application, by relating the use of cryptographic libraries to the end-to-end security policies that those libraries are enforcing during communication. This work has been done with Tom Chothia, a post-doctoral associate, and my Ph.D. student, Ye Wu. Compiler type-checking ensures that the code conforms with those end-to-end security policies. We developed the key-based decentralized label model (KDLM) as a framework for access control, information flow control and distributed declassification in distributed systems. The Jeddak language design extends Java with the ability to model security policies in the type system, using cryptographic keys as run-time witnesses. Essentially cryptographic entities such as keys are first-class modules in Jeddak. We have developed accountable noninterference as a correctness condition for secure distributed systems. We are currently llooking at concurrency and fault-tolerance aspects of such applications. More information on this research is given in the description of the Jeddak project.

D. Duggan. (2004). "Type-based cryptographic operations", Journal of Computer Security, 12 (3-4), 485-550.

Fault Tolerance in Global Computing

Tom Chothia and I worked on the engineering of application protocols in the modern internet. Although the original internet was a flat address space identified by IP addresses for machines, the modern internet is a discrete address space that has been partitioned by firewalls and network address translaters. We developed a model for decoupling the design of application protocols from the details of communication, providing an abstraction of logs to applications, and capabilities that can be extracted from such logs and used to communicate distributed state.

T. Chothia and D. Duggan. (2007). "Capability passing processes", Science of Computer Programming, Elsevier. (66), 184-204.

T. Chothia and D. Duggan. (2004). "Abstractions for fault-tolerant global computing", Theoretical Computer Science, Elsevier. 3 (322), 567-613.

DYNAMIC Software Update

My interest in dynamic software update started with Stephen Gilmore's Dynamic ML. The issue is ensuring that a running component can be guaranteed to safely adapt to changes in type formats e.g. changing packet headers in running network applications. Dynamic ML and related approaches require threads running old version code to stop (or terminate the threads). My approach was to allow old version code to adapt to new version values, as well as allowing new version code to adapt to old version values. Mike Hicks was also working on dynamic software update around the same time. Whereas he took an approach of "eager" software update, basically marshalling between old and new version values at abstraction boundaries, my approach is based on "lazy" software update, dispatching based on version tags when data is accessed. I believe that this approach has particular promise in distributed applications, since current approaches assume that there is a centralized controller that can immediately communicate changes to all running threads. As part of this work, I needed a type system for components and developed a foundation for component-based interfaces for languages such as Java and C#.

D. Duggan. (2005). "Type-based hot swapping of running libraries", Acta Informatica, Springer. 41 (4-5).

D. Duggan. (2002). "Type-safe dynamic linking with recursive DLLs and shared libraries", Transactions on Programming Languages and Systems, ACM. 24 (6), 711-804.

Type-Safe Marshalling

I developed the notion of refinement kinds for safe type-based dispatch. Typically type-based dispatch is based on some kind of "typecase" construct (with the Java constructs a particularly poor design from the viewpoint of safety and efficiency). A classic paper by Cardelli, Pierce and Plotkin proposed "dynamics" as a way of adding dynamic typing into a statically typed language. I proposed decoupling the run-time type check (a possible point of failure) from the manipulation of values of dynamic type (which should be safe). This work was particularly motivated by issues in safe marshalling for languages with type genericity. I developed self-extracting dynamics as a semantics for safe user-defined marshalling.

D. Duggan. (1999). "Dynamic typing for distributed programming in polymorphic languages", Transactions on Programming Languages and Systems, ACM. 21 (1), 11-45.

ObjecT Type Constructors

There are well-known problems with extending type inference to languages with impredicative type polymorphism, and this is important for object-oriented languages. Consider for example a list object with map and reduce methods: the types of these methods must be polymorphic in the result type, so their types must be instantiated when they are applied, not when an object is created. My approach of object type constructors was inspired by Mark Jones' work on type constructor classes, where type classes are defined over higher-rank type constructors and not just simple types. Whereas Mark's work considered universal quantification over higher-rank type constructors, my work considered existential type quantification (for object interfaces, where the witness type is a collection type). Basically object types are a form of datatypes in my approach, where the object type constructor specifies the required polymorphism of the methods injected into the object. The use of "iso-recursive" object interfaces also avoids the famous problem of checking equivalence of non-regular recursive types. Type inference required a combination of subtype polymorphism and constraint checking under a "mixed prefix," using ideas by Dale Miller for scoped unification with both free and bound variables.

D. Duggan. (2002). "Object type constructors", Acta Informatica, Springer. (38), 367-408.

Type Classes

With my colleague John Ophel, I did work in type-checking Haskell-style type classes aka parameteric overloading. Although we did some work for the single-parameter case, our "holy grail" was the multi-parameter case, and one of our results was an undecidability result for a useful case of multi-parameter type classes.

D. Duggan and J. Ophel. (2002). "Type checking multi-parameter type classes", Journal of Functional Programming, Academic Press. 12 (2), 133-158.

D. Duggan and J. Ophel. (2002). "Open and closed scopes for constrained genericity", Theoretical Computer Science, Elsevier. (275), 215-258.

D. Duggan, G. Cormack and J. Ophel. (1996). "Kinded type inference for parametric overloading", Acta Informatica, Springer. (33), 21-68.

Type Explanation

The ML language gained some prominence (in the research community) because of its facility for type inference: the programmer could leave out type declarations for variables, and the compiler would figure out the missing type declarations based on how the variables are used. The hard problem in type inference is the user interface issue of explaining inferred types, especially when variables may be aliased by unification. With my student Fred Bent, we developed a type explainer to explore these issues, especially how to keep the explanations short and intuitive.

D. Duggan and F. Bent. (1996). "Explaining type inference", Science of Computer Programming, Elsevier. 27 (1).


During my Ph.D. thesis work, I became interested in the work of Dale Miller and Frank Pfenning in meta-programming (programs that manipulate other programs). Their approach was based on the idea of higher-order abstract syntax: this automates proper handling of object language variables by representing them using metalanguage variables, using higher-order unification as the basic computational mechanism. The prominent first-order approach to manipulating abstract syntax was the calculus of explicit substitutions that was invented independently by Abadi, Cardelli, Curien, and Levy, and by Field. In seeing how explicit substitutions could be incorporated into higher-order abstract syntax, I discovered that the key obstacle was composing substutitions, and my "trick" to solving this problem identified an extension of Miller's beta0-unification that retained the decidability and deterministic properties of the latter.

D. Duggan. (2001). "Higher-order substitutions", Information and Computation, Academic Press. (164), 1-53.

D. Duggan. (1998). "Unification with extended patterns", Theoretical Computer Science, Elsevier. (206), 1-50.