Dynamic DCC Related Reading

Access Control in a Core Calculus of Dependency (Abadi)
A Core Calculus of Dependency (Abadi, Banerjee, Heintze, Riecke)
These papers describe two versions of DCC, the immediate inspiration for the Dynamic DCC language we would like to implement. The single author was published later, but I think is an easier read and a better place to start. The four author paper is more general and explains how DCC can be used to model a variety of analyses.
A Type Discipline for Authorization Polices (Fournet, Gordon, and Maffeis)
This paper gives a pi-calculus with the special type constructor OK. The type OK(S) has the intended semantics that policy S holds, where S is a datalog term. Their terms give only a single inhabitant of OK(S) for any S; this means that they do not actually pass proofs at runtime. There is a later paper which expresses policies in dcc, but it's not publicly available yet.

Proofs are Programs: 19th Century Logic and 21st Century Computing (Wadler)
In Dynamic DCC, we plan to use digital signatures as verifiable assertion which can be used as part of a proof. The remainder of a proof will be constructed with lambda calculus like terms. This paper gives a succinct overview of Curry-Howard isomorphism, which says that "programs are proofs."

Dependent Types (David Aspinall and Martin Hofmann—Chapter 2 in Advanced Types and Programming Languages edited B.C. Pierce)
Dependent types allow types to mention terms. Dependent types are essential for fully exploiting the Curry-Howard isomorphism.

The Haskell Programmer's Guide to the IO Monad (Klinger)
The "P says" type constructor in DCC is (almost) a monad. This paper discusses monads in Haskell with some lightweight category theory. I've only skimmed this, but it looks cool and there's good buzz on Lambda the Ultimate.
The Marriage of Effects and Monads (Wadler and Thiemann)
A little dense, but looks like a good starting point for learning about the monads and effects-types.

An Idealized MetaML Simpler, and More Expressivei (Moggi, Taha, Benaissa, and Sheard)
A Modal Analysis of Staged Computation (Davies and Pfenning)
Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection (Calcagno, Taha, Huang, and Leory)
I haven't read these yet. The first two appear to address staged computation along the lines of Context Modal Type Theory (below). The latter takes a different tact.

Run-time principals in information flow type systems (Tse and Zdancewic)
An information flow language the ability the run dynamic queries on principals and branch to code in which the query has been statically assumed to be true (or false). This similar to the dynamic typecheck we want for dynamic dcc.
Language-Based Information-Flow Security (Sabelfeld and Myers)
A thorough survey of information flow security papers.

A Standard ML Compiler (Appel and MacQueen)
A light description of the first SML compiler implemented in Standard ML. This highlights pattern compilation and the use of simple lambda calculus as an intermediate representation language.
Implementing Functional Languages: A Tutorial (Peyton Jones and Lester)
This book is much for in depth than the above paper and gives a Miranda implementation or a compiler for a core functional language. Peyton Jones has an earlier book, "The Implementation of Functional Programming Languages," but, he says, it is less practically oriented.