History for Correctness of Multistage Notations

changed:
- Relevant work and people include: Staged computation (Joerring and Scherlis, Lisp/Scheme quasiquotation (backquote and comma), DynJava (Oiwa), MetaML (Sheard), MetaOCaml (Calcagno, Leroy, Taha), Metaphor (Neverov, Roe), dependent types (Martin-Lof, Coquand), the Coq system, Omega (Sheard), Pasalic, Linger, Pfenning, Davies, Nanevski, Pitts, Nielson, Batory, Czarnecki, Smaragdakis, Kamin, explicit substitutions, ... Some relation to model driven development.
 Relevant work and people include: Staged computation (Joerring and Scherlis, Lisp/Scheme quasiquotation (backquote and comma), DynJava (Oiwa), MetaML (Sheard), MetaOCaml (Calcagno, Leroy, Taha), Metaphor (Neverov, Roe), dependent types (Martin-Lof, Coquand), the Coq system, Omega (Sheard), Pasalic, Linger, Pfenning, Davies, Nanevski, Pitts, Nielson, Batory, Czarnecki, Smaragdakis, Kamin, explicit substitutions, ...

changed:
-Develop a theory of types for multistage languages that covers correctness levels (a), (b), (c) and (d).  The theory should support type notations and mechanized consistency checking.  Relevant existing theory includes dependent types (Martin-Lof) and nominal logic (Pitts).
(5 years) Develop a theory of types for multistage languages that covers correctness levels (a), (b), (c) and (d).  The theory should support type notations and mechanized consistency checking.  Relevant existing theory includes dependent types (Martin-Lof) and nominal logic (Pitts).

changed:
-Develop a theory of types to support safe runtime reflection.
(5 years) Develop a theory of types to support safe runtime reflection.

changed:
-Develop 
(5 years) Develop theory to support typesafe database access from a mainstream programming language.