-
The Declarative Side of
Magic. Paolo Mascellani and Dino Pedreschi. 2002.
An excellent introduction to magic sets (page 9) and a
proof that well-moded prolog programs produce magic programs
that are Datalog safe, i.e. all variables in the head appear
in the body (Theorem 6).
-
Hoare Type Theory,
Polymorphism and Separation. Aleksandar Nanevski,
Greg Morrisett, and Lars Birkedal. 2006.
The original paper on Hoare Type Theory (HTT) that
reconciles dependent types with program
logics. Interesting because it cleans up the variable
binding mess that often exists in program logics. Also
a great example of the use of hereditary
substitutions.
-
Environmental
Bisimulations for Higher-Order Languages. Davide
Sangiorgi, Naoki Kobayashi, and Eijiro Sumii. 2007.
The introduction contains a beautiful, insightful
discussion of approaches that work and those that do
not work for higher-order bisimulations.
-
Secure Information Flow
as a Safety Property. Gérard Boudol. 2008.
A characterization of secrecy of information as a
safety property, a type system that enforces it, and a
proof that the property implies non-interference. Also
included is dynamic access control on secret
information.
|