notes-computer-jasper-jasperIrrelevantNotes

http://tratt.net/laurie/research/pubs/html/berger_tratt__program_logics_for_homogeneous_meta_programming/

formal proofs of various tradeoffs in language design regarding expressibility vs. guaranteed properties that are intuitively true. i skimmed:

http://arxiv.org/pdf/cs/0512065.pdf