some citations

all.bib

@@ -2,13 +2,632 @@
 %% http://bibdesk.sourceforge.net/
 
 
-%% Created for Jeremy Siek at 2016-02-05 10:00:34 -0500 
+%% Created for Jeremy Siek at 2016-03-29 22:03:07 -0400 
 
 
 %% Saved with string encoding Unicode (UTF-8) 
 
 
 
+@inproceedings{Cardelli:1984aa,
+	Acmid = {802037},
+	Address = {New York, NY, USA},
+	Author = {Cardelli, Luca},
+	Booktitle = {Proceedings of the 1984 ACM Symposium on LISP and Functional Programming},
+	Date-Added = {2016-03-30 01:59:55 +0000},
+	Date-Modified = {2016-03-30 01:59:59 +0000},
+	Doi = {10.1145/800055.802037},
+	Isbn = {0-89791-142-3},
+	Location = {Austin, Texas, USA},
+	Numpages = {10},
+	Pages = {208--217},
+	Publisher = {ACM},
+	Series = {LFP '84},
+	Title = {Compiling a Functional Language},
+	Url = {http://doi.acm.org/10.1145/800055.802037},
+	Year = {1984},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QEXAyMDgtY2FyZGVsbGkucGRm0hcLGBlXTlMuZGF0YU8RAZYAAAAAAZYAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAM3IwOpIKwAAAL9t8RFwMjA4LWNhcmRlbGxpLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABXQMR0yCrg1BERiAAAAAAAAEAAgAACSAAAAAAAAAAAAAAAAAAAAADYmliAAAQAAgAAM3I+SoAAAARAAgAANMg48MAAAABABAAv23xAUNoPAAFwHIAAhIpAAIAP01hY2ludG9zaCBIRDpVc2VyczoAanNpZWs6AEdvb2dsZSBEcml2ZToAYmliOgBwMjA4LWNhcmRlbGxpLnBkZgAADgAkABEAcAAyADAAOAAtAGMAYQByAGQAZQBsAGwAaQAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIALlVzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvcDIwOC1jYXJkZWxsaS5wZGYAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCiAKcArwJJAksCUAJbAmQCcgJ2An0ChgKLApgCmwKtArACtQAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAK3},
+	Bdsk-Url-1 = {http://doi.acm.org/10.1145/800055.802037},
+	Bdsk-Url-2 = {http://dx.doi.org/10.1145/800055.802037}}
+
+@techreport{Dennis:1975aa,
+	Author = {Jack B. Dennis},
+	Date-Added = {2016-03-25 02:29:40 +0000},
+	Date-Modified = {2016-03-25 02:30:18 +0000},
+	Institution = {MIT},
+	Number = {MIT/LCS/TM-61},
+	Title = {First version of a data flow procedure language},
+	Year = {1975},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QEk1JVC1MQ1MtVE0tMDYxLnBkZtIXCxgZV05TLmRhdGFPEQGaAAAAAAGaAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfESTUlULUxDUy1UTS0wNjEucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAVvsEdMaGwRQREYgAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADTGlNEAAAAAQAQAL9t8QFDaDwABcByAAISKQACAEBNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoATUlULUxDUy1UTS0wNjEucGRmAA4AJgASAE0ASQBUAC0ATABDAFMALQBUAE0ALQAwADYAMQAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAL1VzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvTUlULUxDUy1UTS0wNjEucGRmAAATAAEvAAAVAAIADP//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAKMAqACwAk4CUAJVAmACaQJ3AnsCggKLApACnQKgArICtQK6AAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAArw=}}
+
+@inproceedings{Dennis:1974ab,
+	Acmid = {704865},
+	Address = {London, UK, UK},
+	Author = {Dennis, J. B. and Fosseen, J. B. and Linderman, J. P.},
+	Booktitle = {Proceedings of the International Sympoisum on Theoretical Programming},
+	Date-Added = {2016-03-25 02:27:37 +0000},
+	Date-Modified = {2016-03-25 02:27:41 +0000},
+	Isbn = {3-540-06720-5},
+	Numpages = {30},
+	Pages = {187--216},
+	Publisher = {Springer-Verlag},
+	Title = {Data Flow Schemas},
+	Url = {http://dl.acm.org/citation.cfm?id=646795.704865},
+	Year = {1974},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QITE5NzQtbG5jcy01LWRhdGEtZmxvdy1zY2hlbWFzLnBkZtIXCxgZV05TLmRhdGFPEQHUAAAAAAHUAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEfMTk3NC1sbmNzLTUtZGF0YS1mbCMxNUJFQkUwLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAVvr4NMaGmtQREYgAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADTGlKrAAAAAQAQAL9t8QFDaDwABcByAAISKQACAE1NYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAMTk3NC1sbmNzLTUtZGF0YS1mbCMxNUJFQkUwLnBkZgAADgBEACEAMQA5ADcANAAtAGwAbgBjAHMALQA1AC0AZABhAHQAYQAtAGYAbABvAHcALQBzAGMAaABlAG0AYQBzAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgA+VXNlcnMvanNpZWsvR29vZ2xlIERyaXZlL2JpYi8xOTc0LWxuY3MtNS1kYXRhLWZsb3ctc2NoZW1hcy5wZGYAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCyALcAvwKXApkCngKpArICwALEAssC1ALZAuYC6QL7Av4DAwAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAMF},
+	Bdsk-Url-1 = {http://dl.acm.org/citation.cfm?id=646795.704865}}
+
+@inproceedings{Rastogi:2015aa,
+	Acmid = {2676971},
+	Address = {New York, NY, USA},
+	Author = {Rastogi, Aseem and Swamy, Nikhil and Fournet, C{\'e}dric and Bierman, Gavin and Vekris, Panagiotis},
+	Booktitle = {Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+	Date-Added = {2016-03-21 18:01:31 +0000},
+	Date-Modified = {2016-03-21 18:01:38 +0000},
+	Doi = {10.1145/2676726.2676971},
+	Isbn = {978-1-4503-3300-9},
+	Keywords = {gradual typing, javascript, type safety, typescript},
+	Location = {Mumbai, India},
+	Numpages = {14},
+	Pages = {167--180},
+	Publisher = {ACM},
+	Series = {POPL '15},
+	Title = {Safe \&\#38; Efficient Gradual Typing for TypeScript},
+	Url = {http://doi.acm.org/10.1145/2676726.2676971},
+	Year = {2015},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QEHAxNjctcmFzdG9naS5wZGbSFwsYGVdOUy5kYXRhTxEBkgAAAAABkgACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xEHAxNjctcmFzdG9naS5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAFakc3TFa9fUERGIAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA0xXnnwAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgA+TWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6AHAxNjctcmFzdG9naS5wZGYADgAiABAAcAAxADYANwAtAHIAYQBzAHQAbwBnAGkALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAC1Vc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL3AxNjctcmFzdG9naS5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AoQCmAK4CRAJGAksCVgJfAm0CcQJ4AoEChgKTApYCqAKrArAAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAACsg==},
+	Bdsk-Url-1 = {http://doi.acm.org/10.1145/2676726.2676971},
+	Bdsk-Url-2 = {http://dx.doi.org/10.1145/2676726.2676971}}
+
+@article{Abadi:1995aa,
+	Author = {Abadi,M. and Cardelli,L. and Pierce,B. and R{\'e}my,D.},
+	Date-Added = {2016-03-16 03:37:16 +0000},
+	Date-Modified = {2016-03-16 03:37:21 +0000},
+	Doi = {10.1017/S095679680000126X},
+	Issn = {1469-7653},
+	Issue = {01},
+	Journal = {Journal of Functional Programming},
+	Numpages = {20},
+	Pages = {111--130},
+	Title = {Dynamic typing in polymorphic languages},
+	Url = {http://journals.cambridge.org/article_S095679680000126X},
+	Volume = {5},
+	Year = {1995},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV5TUkMtUlItMTIwLnBkZtIXCxgZV05TLmRhdGFPEQGKAAAAAAGKAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEOU1JDLVJSLTEyMC5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAVmxOdMOTlhQREYgAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADTDoaYAAAAAQAQAL9t8QFDaDwABcByAAISKQACADxNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAU1JDLVJSLTEyMC5wZGYADgAeAA4AUwBSAEMALQBSAFIALQAxADIAMAAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAK1VzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvU1JDLVJSLTEyMC5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AnQCiAKoCOAI6Aj8CSgJTAmECZQJsAnUCegKHAooCnAKfAqQAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAACpg==},
+	Bdsk-Url-1 = {http://journals.cambridge.org/article_S095679680000126X},
+	Bdsk-Url-2 = {http://dx.doi.org/10.1017/S095679680000126X}}
+
+@inproceedings{Vytiniotis:2005aa,
+	Acmid = {1040296},
+	Address = {New York, NY, USA},
+	Author = {Vytiniotis, Dimitrios and Washburn, Geoffrey and Weirich, Stephanie},
+	Booktitle = {Proceedings of the 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation},
+	Date-Added = {2016-03-14 13:56:34 +0000},
+	Date-Modified = {2016-03-14 13:56:37 +0000},
+	Doi = {10.1145/1040294.1040296},
+	Isbn = {1-58113-999-3},
+	Keywords = {ad-hoc polymorphism, generativity, intensional type analysis, reflexivity},
+	Location = {Long Beach, California, USA},
+	Numpages = {12},
+	Pages = {13--24},
+	Publisher = {ACM},
+	Series = {TLDI '05},
+	Title = {An Open and Shut Typecase},
+	Url = {http://doi.acm.org/10.1145/1040294.1040296},
+	Year = {2005},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QEnAxMy12eXRpbmlvdGlzLnBkZtIXCxgZV05TLmRhdGFPEQGaAAAAAAGaAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEScDEzLXZ5dGluaW90aXMucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAVlcTdMMO39QREYgAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADTDHO/AAAAAQAQAL9t8QFDaDwABcByAAISKQACAEBNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAcDEzLXZ5dGluaW90aXMucGRmAA4AJgASAHAAMQAzAC0AdgB5AHQAaQBuAGkAbwB0AGkAcwAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAL1VzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvcDEzLXZ5dGluaW90aXMucGRmAAATAAEvAAAVAAIADP//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAKMAqACwAk4CUAJVAmACaQJ3AnsCggKLApACnQKgArICtQK6AAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAArw=},
+	Bdsk-Url-1 = {http://doi.acm.org/10.1145/1040294.1040296},
+	Bdsk-Url-2 = {http://dx.doi.org/10.1145/1040294.1040296}}
+
+@article{Rossberg:2008aa,
+	Author = {Andreas Rossberg},
+	Date-Added = {2016-03-14 13:53:23 +0000},
+	Date-Modified = {2016-03-14 13:53:27 +0000},
+	Doi = {http://dx.doi.org/10.1016/j.entcs.2008.10.019},
+	Issn = {1571-0661},
+	Journal = {Electronic Notes in Theoretical Computer Science},
+	Keywords = {singleton kinds},
+	Note = {Proceedings of the 24th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIV)},
+	Pages = {313 - 336},
+	Title = {Dynamic Translucency with Abstraction Kinds and Higher-Order Coercions},
+	Url = {http://www.sciencedirect.com/science/article/pii/S1571066108004131},
+	Volume = {218},
+	Year = {2008},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QFGR5bi10cmFuc2x1Y2VuY3kucGRm0hcLGBlXTlMuZGF0YU8RAaIAAAAAAaIAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAM3IwOpIKwAAAL9t8RRkeW4tdHJhbnNsdWNlbmN5LnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABWVvJ0ww6tVBERiAAAAAAAAEAAgAACSAAAAAAAAAAAAAAAAAAAAADYmliAAAQAAgAAM3I+SoAAAARAAgAANMMcvUAAAABABAAv23xAUNoPAAFwHIAAhIpAAIAQk1hY2ludG9zaCBIRDpVc2VyczoAanNpZWs6AEdvb2dsZSBEcml2ZToAYmliOgBkeW4tdHJhbnNsdWNlbmN5LnBkZgAOACoAFABkAHkAbgAtAHQAcgBhAG4AcwBsAHUAYwBlAG4AYwB5AC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAxVXNlcnMvanNpZWsvR29vZ2xlIERyaXZlL2JpYi9keW4tdHJhbnNsdWNlbmN5LnBkZgAAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgClAKoAsgJYAloCXwJqAnMCgQKFAowClQKaAqcCqgK8Ar8CxAAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAALG},
+	Bdsk-Url-1 = {http://www.sciencedirect.com/science/article/pii/S1571066108004131},
+	Bdsk-Url-2 = {http://dx.doi.org/10.1016/j.entcs.2008.10.019}}
+
+@article{Sewell:2007aa,
+	Author = {Sewell, Peter and Leifer, James J. and Wansbrough, Keith and Nardelli, Francesco Zappa and Allen-Williams, Mair and Habouzit, Pierre and Vafeiadis, Viktor},
+	Date-Added = {2016-03-14 13:27:01 +0000},
+	Date-Modified = {2016-03-14 13:28:27 +0000},
+	Doi = {10.1017/S0956796807006442},
+	Issn = {1469-7653},
+	Issue = {4-5},
+	Journal = {Journal of Functional Programming},
+	Numpages = {66},
+	Pages = {547--612},
+	Title = {Acute: High-level programming language design for distributed computation},
+	Url = {http://journals.cambridge.org/article_S0956796807006442},
+	Volume = {17},
+	Year = {2007},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QEGFjdXRlMi1zaG9ydC5wZGbSFwsYGVdOUy5kYXRhTxEBkgAAAAABkgACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xEGFjdXRlMi1zaG9ydC5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAFZWSTTDDTQUERGIAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA0wxtEAAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgA+TWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6AGFjdXRlMi1zaG9ydC5wZGYADgAiABAAYQBjAHUAdABlADIALQBzAGgAbwByAHQALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAC1Vc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL2FjdXRlMi1zaG9ydC5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AoQCmAK4CRAJGAksCVgJfAm0CcQJ4AoEChgKTApYCqAKrArAAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAACsg==},
+	Bdsk-Url-1 = {http://journals.cambridge.org/article_S0956796807006442},
+	Bdsk-Url-2 = {http://dx.doi.org/10.1017/S0956796807006442}}
+
+@inproceedings{Sewell:2001aa,
+	Acmid = {360225},
+	Address = {New York, NY, USA},
+	Author = {Sewell, Peter},
+	Booktitle = {Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+	Date-Added = {2016-03-14 13:24:02 +0000},
+	Date-Modified = {2016-03-14 13:24:04 +0000},
+	Doi = {10.1145/360204.360225},
+	Isbn = {1-58113-336-7},
+	Location = {London, United Kingdom},
+	Numpages = {12},
+	Pages = {236--247},
+	Publisher = {ACM},
+	Series = {POPL '01},
+	Title = {Modules, Abstract Types, and Distributed Versioning},
+	Url = {http://doi.acm.org/10.1145/360204.360225},
+	Year = {2001},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QD3AyMzYtc2V3ZWxsLnBkZtIXCxgZV05TLmRhdGFPEQGOAAAAAAGOAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEPcDIzNi1zZXdlbGwucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAVllHNMMM8dQREYgAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADTDGwHAAAAAQAQAL9t8QFDaDwABcByAAISKQACAD1NYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAcDIzNi1zZXdlbGwucGRmAAAOACAADwBwADIAMwA2AC0AcwBlAHcAZQBsAGwALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASACxVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL3AyMzYtc2V3ZWxsLnBkZgATAAEvAAAVAAIADP//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAKAApQCtAj8CQQJGAlECWgJoAmwCcwJ8AoECjgKRAqMCpgKrAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAAq0=},
+	Bdsk-Url-1 = {http://doi.acm.org/10.1145/360204.360225},
+	Bdsk-Url-2 = {http://dx.doi.org/10.1145/360204.360225}}
+
+@inproceedings{Sumii:2004aa,
+	Acmid = {964015},
+	Address = {New York, NY, USA},
+	Author = {Sumii, Eijiro and Pierce, Benjamin C.},
+	Booktitle = {Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+	Date-Added = {2016-03-14 13:19:22 +0000},
+	Date-Modified = {2016-03-14 13:19:27 +0000},
+	Doi = {10.1145/964001.964015},
+	Isbn = {1-58113-729-X},
+	Location = {Venice, Italy},
+	Numpages = {12},
+	Pages = {161--172},
+	Publisher = {ACM},
+	Series = {POPL '04},
+	Title = {A Bisimulation for Dynamic Sealing},
+	Url = {http://doi.acm.org/10.1145/964001.964015},
+	Year = {2004},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV5wMTYxLXN1bWlpLnBkZtIXCxgZV05TLmRhdGFPEQGKAAAAAAGKAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEOcDE2MS1zdW1paS5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAL956dEPOO8AAAAAAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADRD38/AAAAAQAQAL9t8QFDaDwABcByAAISKQACADxNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAcDE2MS1zdW1paS5wZGYADgAeAA4AcAAxADYAMQAtAHMAdQBtAGkAaQAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAK1VzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvcDE2MS1zdW1paS5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AnQCiAKoCOAI6Aj8CSgJTAmECZQJsAnUCegKHAooCnAKfAqQAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAACpg==},
+	Bdsk-Url-1 = {http://doi.acm.org/10.1145/964001.964015},
+	Bdsk-Url-2 = {http://dx.doi.org/10.1145/964001.964015}}
+
+@inproceedings{Pitts:1993aa,
+	Acmid = {666533},
+	Address = {London, UK, UK},
+	Author = {Pitts, Andrew M. and Stark, Ian D. B.},
+	Booktitle = {Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science},
+	Date-Added = {2016-03-14 13:10:28 +0000},
+	Date-Modified = {2016-03-14 13:10:31 +0000},
+	Isbn = {3-540-57182-5},
+	Numpages = {20},
+	Pages = {122--141},
+	Publisher = {Springer-Verlag},
+	Series = {MFCS '93},
+	Title = {Observable Properties of Higher Order Functions That Dynamically Create Local Names, or What's New?},
+	Url = {http://dl.acm.org/citation.cfm?id=645722.666533},
+	Year = {1993},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YVxvYnMtcHJvcC5wZGbSFwsYGVdOUy5kYXRhTxEBggAAAAABggACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xDG9icy1wcm9wLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAFZVnvTDDCdUERGIAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA0wxo3QAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgA6TWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6AG9icy1wcm9wLnBkZgAOABoADABvAGIAcwAtAHAAcgBvAHAALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAClVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL29icy1wcm9wLnBkZgAAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCbAKAAqAIuAjACNQJAAkkCVwJbAmICawJwAn0CgAKSApUCmgAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAKc},
+	Bdsk-Url-1 = {http://dl.acm.org/citation.cfm?id=645722.666533}}
+
+@article{Morris:1973aa,
+	Acmid = {361937},
+	Address = {New York, NY, USA},
+	Author = {Morris,Jr., James H.},
+	Date-Added = {2016-03-14 12:54:46 +0000},
+	Date-Modified = {2016-03-14 12:54:50 +0000},
+	Doi = {10.1145/361932.361937},
+	Issn = {0001-0782},
+	Issue_Date = {Jan. 1973},
+	Journal = {Commun. ACM},
+	Keywords = {access control, access keys, authentication, environments, protection, seals, secrecy, trademarks, types},
+	Month = jan,
+	Number = {1},
+	Numpages = {7},
+	Pages = {15--21},
+	Publisher = {ACM},
+	Title = {Protection in Programming Languages},
+	Url = {http://doi.acm.org/10.1145/361932.361937},
+	Volume = {16},
+	Year = {1973},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV5wMTUtbW9ycmlzLnBkZtIXCxgZV05TLmRhdGFPEQGKAAAAAAGKAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEOcDE1LW1vcnJpcy5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAVlUw9MMLPxQREYgAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADTDGU8AAAAAQAQAL9t8QFDaDwABcByAAISKQACADxNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAcDE1LW1vcnJpcy5wZGYADgAeAA4AcAAxADUALQBtAG8AcgByAGkAcwAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAK1VzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvcDE1LW1vcnJpcy5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AnQCiAKoCOAI6Aj8CSgJTAmECZQJsAnUCegKHAooCnAKfAqQAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAACpg==},
+	Bdsk-Url-1 = {http://doi.acm.org/10.1145/361932.361937},
+	Bdsk-Url-2 = {http://dx.doi.org/10.1145/361932.361937}}
+
+@incollection{Amin:2016aa,
+	Author = {Nada Amin and Samuel Gr\"utter and Martin Odersky and Tiark Rompf and Sandro Stucki},
+	Booktitle = {A list of successes that can change the world},
+	Date-Added = {2016-02-27 16:59:18 +0000},
+	Date-Modified = {2016-02-27 17:01:51 +0000},
+	Publisher = {Springer},
+	Series = {LNCS},
+	Title = {The Essence of Dependent Object Types},
+	Year = {2016},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QGWVzc2VuY2UtZGVwLW9iai10eXBlcy5wZGbSFwsYGVdOUy5kYXRhTxEBtgAAAAABtgACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xGWVzc2VuY2UtZGVwLW9iai10eXBlcy5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAFUb3vS90B2UERGIAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA0veGxgAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgBHTWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6AGVzc2VuY2UtZGVwLW9iai10eXBlcy5wZGYAAA4ANAAZAGUAcwBzAGUAbgBjAGUALQBkAGUAcAAtAG8AYgBqAC0AdAB5AHAAZQBzAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgA2VXNlcnMvanNpZWsvR29vZ2xlIERyaXZlL2JpYi9lc3NlbmNlLWRlcC1vYmotdHlwZXMucGRmABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AqgCvALcCcQJzAngCgwKMApoCngKlAq4CswLAAsMC1QLYAt0AAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAAC3w==}}
+
+@inproceedings{Vekris:2016aa,
+	Author = {Panagiotis Vekris and Benjamin Cosman and Ranjit Jhala},
+	Booktitle = {PLDI '16: Proceedings of the ACM SIGPLAN 2016 conference on Programming language design and implementation},
+	Date-Added = {2016-02-25 14:12:41 +0000},
+	Date-Modified = {2016-02-25 14:13:59 +0000},
+	Title = {Refinement Types for TypeScript},
+	Year = {2016},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QFXJlZmluZS10eXBlc2NyaXB0LnBkZtIXCxgZV05TLmRhdGFPEQGmAAAAAAGmAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEVcmVmaW5lLXR5cGVzY3JpcHQucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAVP9K9L0dVoAAAAAAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADS9LuqAAAAAQAQAL9t8QFDaDwABcByAAISKQACAENNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAcmVmaW5lLXR5cGVzY3JpcHQucGRmAAAOACwAFQByAGUAZgBpAG4AZQAtAHQAeQBwAGUAcwBjAHIAaQBwAHQALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASADJVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL3JlZmluZS10eXBlc2NyaXB0LnBkZgATAAEvAAAVAAIADP//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAKYAqwCzAl0CXwJkAm8CeAKGAooCkQKaAp8CrAKvAsECxALJAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAAss=}}
+
+@inproceedings{Jaber:2016aa,
+	Author = {Guilhem Jaber and Nikos Tzevelekos},
+	Booktitle = {Games for Logic and Programming Languages XI},
+	Date-Added = {2016-02-25 14:07:41 +0000},
+	Date-Modified = {2016-02-25 14:09:10 +0000},
+	Title = {Trace semantics for polymorphic references},
+	Year = {2016},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV50cmFjZS1wb2x5LnBkZtIXCxgZV05TLmRhdGFPEQGKAAAAAAGKAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEOdHJhY2UtcG9seS5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAVP8+NL0dRVQREYgAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADS9LtlAAAAAQAQAL9t8QFDaDwABcByAAISKQACADxNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAdHJhY2UtcG9seS5wZGYADgAeAA4AdAByAGEAYwBlAC0AcABvAGwAeQAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAK1VzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvdHJhY2UtcG9seS5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AnQCiAKoCOAI6Aj8CSgJTAmECZQJsAnUCegKHAooCnAKfAqQAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAACpg==}}
+
+@inproceedings{Castellan:2016aa,
+	Author = {Simon Castellan},
+	Booktitle = {Games for Logic and Programming Languages XI},
+	Date-Added = {2016-02-25 11:11:26 +0000},
+	Date-Modified = {2016-02-25 11:12:35 +0000},
+	Series = {GaLoP},
+	Title = {Weak memory models using event structures},
+	Year = {2016},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QLVdlYWtfbWVtb3J5X21vZGVsc191c2luZ19ldmVudF9zdHJ1Y3R1cmVzLnBkZtIXCxgZV05TLmRhdGFPEQH4AAAAAAH4AAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEfV2Vha19tZW1vcnlfbW9kZWxzXyMxNTNFRkIyLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAVPvstL0S5pQREYgAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADS9JHqAAAAAQAQAL9t8QFDaDwABcByAAISKQACAE1NYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAV2Vha19tZW1vcnlfbW9kZWxzXyMxNTNFRkIyLnBkZgAADgBcAC0AVwBlAGEAawBfAG0AZQBtAG8AcgB5AF8AbQBvAGQAZQBsAHMAXwB1AHMAaQBuAGcAXwBlAHYAZQBuAHQAXwBzAHQAcgB1AGMAdAB1AHIAZQBzAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgBKVXNlcnMvanNpZWsvR29vZ2xlIERyaXZlL2JpYi9XZWFrX21lbW9yeV9tb2RlbHNfdXNpbmdfZXZlbnRfc3RydWN0dXJlcy5wZGYAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgC+AMMAywLHAskCzgLZAuIC8AL0AvsDBAMJAxYDGQMrAy4DMwAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAM1}}
+
+@book{Prawitz:2006aa,
+	Author = {Dag Prawitz},
+	Date-Added = {2016-02-13 16:57:22 +0000},
+	Date-Modified = {2016-02-13 16:58:07 +0000},
+	Publisher = {Dover Publications, Incorporated},
+	Title = {Natural Deduction: A Proof-Theoretic Study},
+	Year = {2006}}
+
+@book{Pierce:2015aa,
+	Author = {Benjamin C. Pierce and Chris Casinghino and Marco Gaboardi and Michael Greenberg and C\v{a}t\v{a}lin Hri\c{t}cu and Vilhelm Sjoberg and Brent Yorgey},
+	Bcp = {Yes},
+	Date-Added = {2016-02-11 16:38:16 +0000},
+	Date-Modified = {2016-02-11 16:38:19 +0000},
+	Ebook = {http://www.cis.upenn.edu/~bcpierce/sf},
+	Japanese = {http://proofcafe.org/sf},
+	Keys = {poplmark,books},
+	Note = {\URL{http://www.cis.upenn.edu/~bcpierce/sf}},
+	Plclub = {Yes},
+	Publisher = {Electronic textbook},
+	Title = {Software Foundations},
+	Year = {2015}}
+
+@phdthesis{Tofte:1988aa,
+	Author = {Mads Tofte},
+	Date-Added = {2016-02-11 16:29:40 +0000},
+	Date-Modified = {2016-02-11 16:30:29 +0000},
+	School = {University of Edinburgh},
+	Title = {Operational Semantics and Polymorphic Type Inference},
+	Year = {1988}}
+
+@article{Cook:1989aa,
+	Acmid = {73711},
+	Address = {Oxford, UK},
+	Author = {Cook, W. R.},
+	Date-Added = {2016-02-11 16:06:33 +0000},
+	Date-Modified = {2016-02-11 16:06:44 +0000},
+	Issn = {0010-4620},
+	Issue_Date = {Aug. 1989},
+	Journal = {Comput. J.},
+	Month = jul,
+	Number = {4},
+	Numpages = {7},
+	Pages = {305--311},
+	Publisher = {Oxford University Press},
+	Title = {A Proposal for Making Eiffel Type-safe},
+	Volume = {32},
+	Year = {1989},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QFGVpZmZlbC10eXBlLXNhZmUucGRm0hcLGBlXTlMuZGF0YU8RAaIAAAAAAaIAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAM3IwOpIKwAAAL9t8RRlaWZmZWwtdHlwZS1zYWZlLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABRulQ0uIb01BERiAAAAAAAAEAAgAACSAAAAAAAAAAAAAAAAAAAAADYmliAAAQAAgAAM3I+SoAAAARAAgAANLiYiMAAAABABAAv23xAUNoPAAFwHIAAhIpAAIAQk1hY2ludG9zaCBIRDpVc2VyczoAanNpZWs6AEdvb2dsZSBEcml2ZToAYmliOgBlaWZmZWwtdHlwZS1zYWZlLnBkZgAOACoAFABlAGkAZgBmAGUAbAAtAHQAeQBwAGUALQBzAGEAZgBlAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAxVXNlcnMvanNpZWsvR29vZ2xlIERyaXZlL2JpYi9laWZmZWwtdHlwZS1zYWZlLnBkZgAAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgClAKoAsgJYAloCXwJqAnMCgQKFAowClQKaAqcCqgK8Ar8CxAAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAALG},
+	Bdsk-Url-1 = {http://dx.doi.org/10.1093/comjnl/32.4.305}}
+
+@article{Grabowski:2015aa,
+	Abstract = {This special issue is dedicated to works related to Mizar, the theorem proving project started by Andrzej Trybulec in the 1970s, and other automated proof checking systems used for formalizing mathematics.},
+	Author = {Grabowski, Adam and Korni{\l}owicz, Artur and Naumowicz, Adam},
+	Date-Added = {2016-02-11 15:36:54 +0000},
+	Date-Modified = {2016-02-11 15:36:56 +0000},
+	Doi = {10.1007/s10817-015-9345-1},
+	Issn = {1573-0670},
+	Journal = {Journal of Automated Reasoning},
+	Number = {3},
+	Pages = {191--198},
+	Title = {Four Decades of Mizar},
+	Url = {http://dx.doi.org/10.1007/s10817-015-9345-1},
+	Volume = {55},
+	Year = {2015},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QFm1pemFyLWZvdXItZGVjYWRlcy5wZGbSFwsYGVdOUy5kYXRhTxEBqgAAAAABqgACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xFm1pemFyLWZvdXItZGVjYWRlcy5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAFG4z/S4hTzUERGIAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA0uJbQwAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgBETWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6AG1pemFyLWZvdXItZGVjYWRlcy5wZGYADgAuABYAbQBpAHoAYQByAC0AZgBvAHUAcgAtAGQAZQBjAGEAZABlAHMALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASADNVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL21pemFyLWZvdXItZGVjYWRlcy5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4ApwCsALQCYgJkAmkCdAJ9AosCjwKWAp8CpAKxArQCxgLJAs4AAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAAC0A==},
+	Bdsk-Url-1 = {http://dx.doi.org/10.1007/s10817-015-9345-1}}
+
+@article{Urban:2007aa,
+	Acmid = {1243822},
+	Address = {Amsterdam, The Netherlands, The Netherlands},
+	Author = {Urban, Josef and Bancerek, Grzegorz},
+	Date-Added = {2016-02-11 15:30:51 +0000},
+	Date-Modified = {2016-02-11 15:30:54 +0000},
+	Doi = {10.1016/j.entcs.2006.09.022},
+	Issn = {1571-0661},
+	Issue_Date = {May, 2007},
+	Journal = {Electron. Notes Theor. Comput. Sci.},
+	Keywords = {ATP, MML Query, MPTP, Mizar, proof objects, proof presentation},
+	Month = may,
+	Number = {2},
+	Numpages = {12},
+	Pages = {63--74},
+	Publisher = {Elsevier Science Publishers B. V.},
+	Title = {Presenting and Explaining Mizar},
+	Url = {http://dx.doi.org/10.1016/j.entcs.2006.09.022},
+	Volume = {174},
+	Year = {2007},
+	Bdsk-Url-1 = {http://dx.doi.org/10.1016/j.entcs.2006.09.022}}
+
+@book{Boyer:1988aa,
+	Address = {San Diego, CA, USA},
+	Author = {Boyer, Robert S. and Moore, J. Strother},
+	Date-Added = {2016-02-11 15:22:58 +0000},
+	Date-Modified = {2016-02-11 15:23:02 +0000},
+	Isbn = {0-12-122952-1},
+	Publisher = {Academic Press Professional, Inc.},
+	Title = {A Computational Logic Handbook},
+	Year = {1988}}
+
+@techreport{Newell:1956aa,
+	Author = {Allen Newell and Herbert A. Simon},
+	Date-Added = {2016-02-11 15:10:02 +0000},
+	Date-Modified = {2016-02-11 15:10:50 +0000},
+	Institution = {Rand Corporation},
+	Month = {June},
+	Number = {P-868},
+	Title = {The Logic Theory Machine: A Complex Information Processing System},
+	Year = {1956},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QFmxvZ2ljdGhlb3J5bWFjaGluZS5wZGbSFwsYGVdOUy5kYXRhTxEBqgAAAAABqgACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xFmxvZ2ljdGhlb3J5bWFjaGluZS5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAFG30XS4g60UERGIAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA0uJVBAAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgBETWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6AGxvZ2ljdGhlb3J5bWFjaGluZS5wZGYADgAuABYAbABvAGcAaQBjAHQAaABlAG8AcgB5AG0AYQBjAGgAaQBuAGUALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASADNVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL2xvZ2ljdGhlb3J5bWFjaGluZS5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4ApwCsALQCYgJkAmkCdAJ9AosCjwKWAp8CpAKxArQCxgLJAs4AAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAAC0A==}}
+
+@incollection{Davis:2001aa,
+	Address = {Amsterdam},
+	Author = {Martin Davis},
+	Booktitle = {Handbook of Automated Reasoning},
+	Date-Added = {2016-02-11 15:06:26 +0000},
+	Date-Modified = {2016-02-11 15:06:29 +0000},
+	Doi = {http://dx.doi.org/10.1016/B978-044450813-3/50003-5},
+	Editor = {Robinson, Alan and Voronkov, Andrei},
+	Isbn = {978-0-444-50813-3},
+	Pages = {3 - 15},
+	Publisher = {North-Holland},
+	Series = {Handbook of Automated Reasoning},
+	Title = {Chapter 1 - The Early History of Automated Deduction: Dedicated to the memory of Hao Wang},
+	Url = {http://www.sciencedirect.com/science/article/pii/B9780444508133500035},
+	Year = {2001},
+	Bdsk-Url-1 = {http://www.sciencedirect.com/science/article/pii/B9780444508133500035},
+	Bdsk-Url-2 = {http://dx.doi.org/10.1016/B978-044450813-3/50003-5}}
+
+@inbook{Brock:1996aa,
+	Address = {Berlin, Heidelberg},
+	Author = {Brock, Bishop and Kaufmann, Matt and Moore, J. Strother},
+	Chapter = {ACL2 theorems about commercial microprocessors},
+	Date-Added = {2016-02-11 14:59:02 +0000},
+	Date-Modified = {2016-02-11 14:59:05 +0000},
+	Doi = {10.1007/BFb0031816},
+	Editor = {Srivas, Mandayam and Camilleri, Albert},
+	Isbn = {978-3-540-49567-3},
+	Pages = {275--293},
+	Publisher = {Springer Berlin Heidelberg},
+	Title = {Formal Methods in Computer-Aided Design: First International Conference, FMCAD '96 Palo Alto, CA, USA, November 6--8, 1996 Proceedings},
+	Url = {http://dx.doi.org/10.1007/BFb0031816},
+	Year = {1996},
+	Bdsk-Url-1 = {http://dx.doi.org/10.1007/BFb0031816}}
+
+@techreport{Milner:1972aa,
+	Address = {Stanford, CA, USA},
+	Author = {Milner, Robin},
+	Date-Added = {2016-02-11 14:54:33 +0000},
+	Date-Modified = {2016-02-11 14:54:35 +0000},
+	Publisher = {Stanford University},
+	Source = {http://www.ncstrl.org:8900/ncstrl/servlet/search?formname=detail\&id=oai%3Ancstrlh%3Astan%3ASTAN%2F%2FCS-TR-72-288},
+	Title = {Logic for Computable Functions: Description of a Machine Implementation.},
+	Year = {1972}}
+
+@article{Boyer:1995aa,
+	Author = {R.S. Boyer and M. Kaufmann and J.S. Moore},
+	Date-Added = {2016-02-11 14:51:17 +0000},
+	Date-Modified = {2016-02-11 15:45:27 +0000},
+	Journal = {Computers \& Mathematics with Applications},
+	Keywords = {PC-Nqthm},
+	Number = {2},
+	Pages = {27 - 62},
+	Title = {The Boyer-Moore theorem prover and its interactive enhancement},
+	Volume = {29},
+	Year = {1995},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QD2JveWVyLW1vb3JlLnBkZtIXCxgZV05TLmRhdGFPEQGOAAAAAAGOAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEPYm95ZXItbW9vcmUucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAUbbqNLiCfpQREYgAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADS4lBKAAAAAQAQAL9t8QFDaDwABcByAAISKQACAD1NYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAYm95ZXItbW9vcmUucGRmAAAOACAADwBiAG8AeQBlAHIALQBtAG8AbwByAGUALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASACxVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL2JveWVyLW1vb3JlLnBkZgATAAEvAAAVAAIADP//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAKAApQCtAj8CQQJGAlECWgJoAmwCcwJ8AoECjgKRAqMCpgKrAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAAq0=},
+	Bdsk-Url-1 = {http://www.sciencedirect.com/science/article/pii/0898122194002157},
+	Bdsk-Url-2 = {http://dx.doi.org/10.1016/0898-1221(94)00215-7}}
+
+@article{Kaufmann:1997aa,
+	Acmid = {254807},
+	Address = {Piscataway, NJ, USA},
+	Author = {Kaufmann, Matt and Moore, J. S.},
+	Date-Added = {2016-02-11 14:48:06 +0000},
+	Date-Modified = {2016-02-11 14:48:09 +0000},
+	Doi = {10.1109/32.588534},
+	Issn = {0098-5589},
+	Issue_Date = {April 1997},
+	Journal = {IEEE Trans. Softw. Eng.},
+	Keywords = {Formal verification, automatic theorem proving, computational logic, partial functions, total functions, type checking, microcode verification, floating point division, digital signal processing.},
+	Month = apr,
+	Number = {4},
+	Numpages = {11},
+	Pages = {203--213},
+	Publisher = {IEEE Press},
+	Title = {An Industrial Strength Theorem Prover for a Logic Based on Common Lisp},
+	Url = {http://dx.doi.org/10.1109/32.588534},
+	Volume = {23},
+	Year = {1997},
+	Bdsk-Url-1 = {http://dx.doi.org/10.1109/32.588534}}
+
+@inbook{Gonthier:2013aa,
+	Address = {Berlin, Heidelberg},
+	Author = {Gonthier, Georges and Asperti, Andrea and Avigad, Jeremy and Bertot, Yves and Cohen, Cyril and Garillot, Fran{\c{c}}ois and Roux, St{\'e}phane and Mahboubi, Assia and O'Connor, Russell and Ould Biha, Sidi and Pasca, Ioana and Rideau, Laurence and Solovyev, Alexey and Tassi, Enrico and Th{\'e}ry, Laurent},
+	Chapter = {A Machine-Checked Proof of the Odd Order Theorem},
+	Date-Added = {2016-02-11 05:24:30 +0000},
+	Date-Modified = {2016-02-11 05:27:31 +0000},
+	Editor = {Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David},
+	Pages = {163--179},
+	Publisher = {Springer Berlin Heidelberg},
+	Title = {Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings},
+	Year = {2013},
+	Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-642-39634-2_14}}
+
+@book{Univalent-Foundations-Program:2013aa,
+	Address = {Institute for Advanced Study},
+	Author = {The {Univalent Foundations Program}},
+	Date-Added = {2016-02-11 05:16:39 +0000},
+	Date-Modified = {2016-02-11 05:16:42 +0000},
+	Publisher = {\url{http://homotopytypetheory.org/book}},
+	Title = {Homotopy Type Theory: Univalent Foundations of Mathematics},
+	Year = 2013}
+
+@inproceedings{Bove:2009aa,
+	Address = {Berlin, Heidelberg},
+	Author = {Bove, Ana and Dybjer, Peter and Norell, Ulf},
+	Booktitle = {Proceedings of the 22Nd International Conference on Theorem Proving in Higher Order Logics},
+	Date-Added = {2016-02-11 05:13:38 +0000},
+	Date-Modified = {2016-02-11 05:18:16 +0000},
+	Location = {Munich, Germany},
+	Numpages = {6},
+	Pages = {73--78},
+	Publisher = {Springer-Verlag},
+	Series = {TPHOLs '09},
+	Title = {A Brief Overview of Agda --- A Functional Language with Dependent Types},
+	Year = {2009},
+	Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-642-03359-9_6}}
+
+@article{Gonthier:2008aa,
+	Author = {Georges Gonthier},
+	Date-Added = {2016-02-11 05:06:19 +0000},
+	Date-Modified = {2016-02-11 05:07:34 +0000},
+	Journal = {Notices of the {AMS}},
+	Month = {December},
+	Number = {11},
+	Pages = {1382--1393},
+	Title = {Formal Proof -- The Four-Color Theorem},
+	Volume = {55},
+	Year = {2008}}
+
+@incollection{Gordon:2000aa,
+	Acmid = {345890},
+	Address = {Cambridge, MA, USA},
+	Author = {Gordon, Mike},
+	Chapter = {From LCF to HOL: A Short History},
+	Date-Added = {2016-02-11 04:58:02 +0000},
+	Date-Modified = {2016-02-11 04:58:06 +0000},
+	Editor = {Plotkin, Gordon and Stirling, Colin and Tofte, Mads},
+	Isbn = {0-262-16188-5},
+	Numpages = {17},
+	Pages = {169--185},
+	Publisher = {MIT Press},
+	Title = {Proof, Language, and Interaction},
+	Url = {http://dl.acm.org/citation.cfm?id=345868.345890},
+	Year = {2000},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV5Ib2xIaXN0b3J5LnBkZtIXCxgZV05TLmRhdGFPEQGKAAAAAAGKAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEOSG9sSGlzdG9yeS5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAUbMMdLhfzdQREYgAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADS4cWHAAAAAQAQAL9t8QFDaDwABcByAAISKQACADxNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoASG9sSGlzdG9yeS5wZGYADgAeAA4ASABvAGwASABpAHMAdABvAHIAeQAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAK1VzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvSG9sSGlzdG9yeS5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AnQCiAKoCOAI6Aj8CSgJTAmECZQJsAnUCegKHAooCnAKfAqQAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAACpg==},
+	Bdsk-Url-1 = {http://dl.acm.org/citation.cfm?id=345868.345890}}
+
+@article{Brat:2004aa,
+	Acmid = {1017111},
+	Address = {Hingham, MA, USA},
+	Author = {Brat, Guillaume and Drusinsky, Doron and Giannakopoulou, Dimitra and Goldberg, Allen and Havelund, Klaus and Lowry, Mike and Pasareanu, Corina and Venet, Arnaud and Visser, Willem and Washington, Rich},
+	Date-Added = {2016-02-11 04:43:08 +0000},
+	Date-Modified = {2016-02-11 04:43:11 +0000},
+	Doi = {10.1023/B:FORM.0000040027.28662.a4},
+	Issn = {0925-9856},
+	Issue_Date = {September-November 2004},
+	Journal = {Form. Methods Syst. Des.},
+	Keywords = {mars flight software, model checking, runtime analysis, static analysis, testing},
+	Month = sep,
+	Number = {2-3},
+	Numpages = {32},
+	Pages = {167--198},
+	Publisher = {Kluwer Academic Publishers},
+	Title = {Experimental Evaluation of Verification and Validation Tools on Martian Rover Software},
+	Url = {http://dx.doi.org/10.1023/B:FORM.0000040027.28662.a4},
+	Volume = {25},
+	Year = {2004},
+	Bdsk-Url-1 = {http://dx.doi.org/10.1023/B:FORM.0000040027.28662.a4}}
+
+@inbook{Behm:1999aa,
+	Address = {Berlin, Heidelberg},
+	Author = {Behm, Patrick and Benoit, Paul and Faivre, Alain and Meynadier, Jean-Marc},
+	Chapter = {M{\'e}t{\'e}or: A Successful Application of B in a Large Project},
+	Date-Added = {2016-02-11 04:41:40 +0000},
+	Date-Modified = {2016-02-11 04:51:35 +0000},
+	Editor = {Wing, Jeannette M. and Woodcock, Jim and Davies, Jim},
+	Pages = {369--387},
+	Publisher = {Springer Berlin Heidelberg},
+	Title = {FM'99 --- Formal Methods: World Congress on Formal Methods in the Development of Computing Systems Toulouse, France, September 20--24, 1999 Proceedings, Volume I},
+	Year = {1999},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YVptZXRlb3IucGRm0hcLGBlXTlMuZGF0YU8RAXoAAAAAAXoAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAM3IwOpIKwAAAL9t8QptZXRlb3IucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABRsoU0uF7VlBERiAAAAAAAAEAAgAACSAAAAAAAAAAAAAAAAAAAAADYmliAAAQAAgAAM3I+SoAAAARAAgAANLhwaYAAAABABAAv23xAUNoPAAFwHIAAhIpAAIAOE1hY2ludG9zaCBIRDpVc2VyczoAanNpZWs6AEdvb2dsZSBEcml2ZToAYmliOgBtZXRlb3IucGRmAA4AFgAKAG0AZQB0AGUAbwByAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAnVXNlcnMvanNpZWsvR29vZ2xlIERyaXZlL2JpYi9tZXRlb3IucGRmAAATAAEvAAAVAAIADP//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAJkAngCmAiQCJgIrAjYCPwJNAlECWAJhAmYCcwJ2AogCiwKQAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAApI=},
+	Bdsk-Url-1 = {http://dx.doi.org/10.1007/3-540-48119-2_22}}
+
+@article{Leroy:2009aa,
+	Acmid = {1538814},
+	Address = {New York, NY, USA},
+	Author = {Leroy, Xavier},
+	Date-Added = {2016-02-11 04:38:45 +0000},
+	Date-Modified = {2016-02-11 04:38:48 +0000},
+	Doi = {10.1145/1538788.1538814},
+	Issn = {0001-0782},
+	Issue_Date = {July 2009},
+	Journal = {Commun. ACM},
+	Month = jul,
+	Number = {7},
+	Numpages = {9},
+	Pages = {107--115},
+	Publisher = {ACM},
+	Title = {Formal Verification of a Realistic Compiler},
+	Url = {http://doi.acm.org/10.1145/1538788.1538814},
+	Volume = {52},
+	Year = {2009},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV5wMTA3LWxlcm95LnBkZtIXCxgZV05TLmRhdGFPEQGKAAAAAAGKAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEOcDEwNy1sZXJveS5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAUbI4dLhep9QREYgAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADS4cDvAAAAAQAQAL9t8QFDaDwABcByAAISKQACADxNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAcDEwNy1sZXJveS5wZGYADgAeAA4AcAAxADAANwAtAGwAZQByAG8AeQAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAK1VzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvcDEwNy1sZXJveS5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AnQCiAKoCOAI6Aj8CSgJTAmECZQJsAnUCegKHAooCnAKfAqQAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAACpg==},
+	Bdsk-Url-1 = {http://doi.acm.org/10.1145/1538788.1538814},
+	Bdsk-Url-2 = {http://dx.doi.org/10.1145/1538788.1538814}}
+
+@inproceedings{Klein:2009aa,
+	Acmid = {1629596},
+	Address = {New York, NY, USA},
+	Author = {Klein, Gerwin and Elphinstone, Kevin and Heiser, Gernot and Andronick, June and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and Sewell, Thomas and Tuch, Harvey and Winwood, Simon},
+	Booktitle = {Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles},
+	Date-Added = {2016-02-11 04:34:34 +0000},
+	Date-Modified = {2016-02-11 04:34:37 +0000},
+	Doi = {10.1145/1629575.1629596},
+	Isbn = {978-1-60558-752-3},
+	Keywords = {isabelle/hol, l4, microkernel, sel4},
+	Location = {Big Sky, Montana, USA},
+	Numpages = {14},
+	Pages = {207--220},
+	Publisher = {ACM},
+	Series = {SOSP '09},
+	Title = {seL4: Formal Verification of an OS Kernel},
+	Url = {http://doi.acm.org/10.1145/1629575.1629596},
+	Year = {2009},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV5wMjA3LWtsZWluLnBkZtIXCxgZV05TLmRhdGFPEQGKAAAAAAGKAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEOcDIwNy1rbGVpbi5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAUbIO9LheZxQREYgAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADS4b/sAAAAAQAQAL9t8QFDaDwABcByAAISKQACADxNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAcDIwNy1rbGVpbi5wZGYADgAeAA4AcAAyADAANwAtAGsAbABlAGkAbgAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAK1VzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvcDIwNy1rbGVpbi5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AnQCiAKoCOAI6Aj8CSgJTAmECZQJsAnUCegKHAooCnAKfAqQAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAACpg==},
+	Bdsk-Url-1 = {http://doi.acm.org/10.1145/1629575.1629596},
+	Bdsk-Url-2 = {http://dx.doi.org/10.1145/1629575.1629596}}
+
+@book{Stump:2016aa,
+	Author = {Aaron Stump},
+	Date-Added = {2016-02-10 03:17:12 +0000},
+	Date-Modified = {2016-02-10 03:19:02 +0000},
+	Editor = {M. Tamer Ozsu},
+	Publisher = {ACM and Morgan \& Claypool Publishers},
+	Series = {ACM Books},
+	Title = {Verified Functional Programming in Agda},
+	Year = {2016},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QK1ZlcmlmaWVkX0Z1bmN0aW9uYWxfUHJvZ3JhbW1pbmdfaW5fQWdkYS5wZGbSFwsYGVdOUy5kYXRhTxEB8gAAAAAB8gACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xH1ZlcmlmaWVkX0Z1bmN0aW9uYWwjMTQ2MUZBNS5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAFGH6XS4BW5UERGIAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA0uBcCQAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgBNTWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6AFZlcmlmaWVkX0Z1bmN0aW9uYWwjMTQ2MUZBNS5wZGYAAA4AWAArAFYAZQByAGkAZgBpAGUAZABfAEYAdQBuAGMAdABpAG8AbgBhAGwAXwBQAHIAbwBnAHIAYQBtAG0AaQBuAGcAXwBpAG4AXwBBAGcAZABhAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgBIVXNlcnMvanNpZWsvR29vZ2xlIERyaXZlL2JpYi9WZXJpZmllZF9GdW5jdGlvbmFsX1Byb2dyYW1taW5nX2luX0FnZGEucGRmABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AvADBAMkCvwLBAsYC0QLaAugC7ALzAvwDAQMOAxEDIwMmAysAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAADLQ==}}
+
 @inproceedings{Diwan:1992aa,
 	Acmid = {143140},
 	Address = {New York, NY, USA},
@@ -1043,9 +1662,9 @@
 @mastersthesis{Bharadwaj:2012aa,
 	Author = {Shashank Bharadwaj},
 	Date-Added = {2015-11-10 20:28:23 +0000},
-	Date-Modified = {2015-11-10 20:29:37 +0000},
+	Date-Modified = {2016-03-22 19:59:34 +0000},
 	School = {University of Colorado at Boulder},
-	Title = {Optimizing Jython using invokedynamic and Gradual Typing},
+	Title = {Optimizing {Jython} using invokedynamic and Gradual Typing},
 	Year = {2012},
 	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YVxzaGFzaGFuay5wZGbSFwsYGVdOUy5kYXRhTxEBggAAAAABggACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xDHNoYXNoYW5rLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAEgtafSZ73ZUERGIAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA0mgEKQAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgA6TWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6AHNoYXNoYW5rLnBkZgAOABoADABzAGgAYQBzAGgAYQBuAGsALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAClVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL3NoYXNoYW5rLnBkZgAAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCbAKAAqAIuAjACNQJAAkkCVwJbAmICawJwAn0CgAKSApUCmgAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAKc}}
 
@@ -1709,9 +2328,9 @@
 	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YVxpbmZvaGlkZS5wZGbSFwsYGVdOUy5kYXRhTxEBggAAAAABggACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xDGluZm9oaWRlLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAADyAyTSAGayUERGIAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA0gCe8gAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgA6TWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6AGluZm9oaWRlLnBkZgAOABoADABpAG4AZgBvAGgAaQBkAGUALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAClVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL2luZm9oaWRlLnBkZgAAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCbAKAAqAIuAjACNQJAAkkCVwJbAmICawJwAn0CgAKSApUCmgAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAKc}}
 
 @article{NEIS:2011aa,
-	Author = {NEIS,GEORG and DREYER,DEREK and ROSSBERG,ANDREAS},
+	Author = {Neis, Georg and Dreyer, Derek and Rossberg, Andreas},
 	Date-Added = {2015-08-24 09:52:34 +0000},
-	Date-Modified = {2015-08-24 09:52:38 +0000},
+	Date-Modified = {2016-03-14 22:59:05 +0000},
 	Doi = {10.1017/S0956796811000165},
 	Issn = {1469-7653},
 	Issue = {Special Issue 4-5},
@@ -15134,7 +15753,6 @@ semantics was validated.},
 	Title = {Mixin' up the {ML} module system},
 	Volume = {43},
 	Year = {2008},
-	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QRC4uL0Ryb3Bib3gvYmliL0RyZXllciwgUm9zc2JlcmcgLSBNaXhpbicgVXAgdGhlIE1MIE1vZHVsZSBTeXN0ZW0ucGRm0hcLGBlXTlMuZGF0YU8RAgYAAAAAAgYAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAM3IwOpIKwAAAA5q4R9EcmV5ZXIsIFJvc3NiZXJnIC0gTWkjRUVGRDUucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAADu/VzOWa4wAAAAAAAAAAAAEAAwAACSAAAAAAAAAAAAAAAAAAAAADYmliAAAQAAgAAM3I+SoAAAARAAgAAMzl4TMAAAABABAADmrhAA5p3QAFwHIAAhIpAAIASE1hY2ludG9zaCBIRDpVc2VyczoAanNpZWs6AERyb3Bib3g6AGJpYjoARHJleWVyLCBSb3NzYmVyZyAtIE1pI0VFRkQ1LnBkZgAOAGwANQBEAHIAZQB5AGUAcgAsACAAUgBvAHMAcwBiAGUAcgBnACAALQAgAE0AaQB4AGkAbgAnACAAVQBwACAAdABoAGUAIABNAEwAIABNAG8AZAB1AGwAZQAgAFMAeQBzAHQAZQBtAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgBNVXNlcnMvanNpZWsvRHJvcGJveC9iaWIvRHJleWVyLCBSb3NzYmVyZyAtIE1peGluJyBVcCB0aGUgTUwgTW9kdWxlIFN5c3RlbS5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4A1QDaAOIC7ALuAvMC/gMHAxUDGQMgAykDLgM7Az4DUANTA1gAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAADWg==},
 	Bdsk-Url-1 = {http://doi.acm.org/10.1145/1411203.1411248}}
 
 @article{Barrett:1996la,
@@ -28589,7 +29207,7 @@ on graph transformation.},
 	Month = {September},
 	Title = {The Comprehensive {LaTeX} Symbol List},
 	Year = {2005},
-	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV5zeW1ib2xzLWE0LnBkZtIXCxgZV05TLmRhdGFPEQGKAAAAAAGKAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEOc3ltYm9scy1hNC5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAL+KM9EPPJUAAAAAAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADRD4LlAAAAAQAQAL9t8QFDaDwABcByAAISKQACADxNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAc3ltYm9scy1hNC5wZGYADgAeAA4AcwB5AG0AYgBvAGwAcwAtAGEANAAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAK1VzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvc3ltYm9scy1hNC5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AnQCiAKoCOAI6Aj8CSgJTAmECZQJsAnUCegKHAooCnAKfAqQAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAACpg==}}
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV5zeW1ib2xzLWE0LnBkZtIXCxgZV05TLmRhdGFPEQGKAAAAAAGKAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEOc3ltYm9scy1hNC5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAVlR+NEPPJVQREYgAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADRD4LlAAAAAQAQAL9t8QFDaDwABcByAAISKQACADxNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAc3ltYm9scy1hNC5wZGYADgAeAA4AcwB5AG0AYgBvAGwAcwAtAGEANAAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAK1VzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvc3ltYm9scy1hNC5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AnQCiAKoCOAI6Aj8CSgJTAmECZQJsAnUCegKHAooCnAKfAqQAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAACpg==}}
 
 @incollection{Baader:2001uq,
 	Author = {F. Baader and W. Snyder},
@@ -29193,8 +29811,7 @@ on graph transformation.},
 	Publisher = {ACM Press},
 	Title = {Flexible representation analysis},
 	Year = {1997},
-	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QHC4uLy4uLy4uL3BhcGVycy9wODUtc2hhby5wZGbSFwsYGVdOUy5kYXRhTxEBZgAAAAABZgACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAwQ+lh0grAAAAT5kRDHA4NS1zaGFvLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAPKHvBCeksAAAAAAAAAAAAAwACAAAJIAAAAAAAAAAAAAAAAAAAAAZwYXBlcnMAEAAIAADBD/nnAAAAEQAIAADBCj2MAAAAAQAMAE+ZEQBOpFMARsk2AAIAK01hY2ludG9zaCBIRDpVc2VyczpzaWVrOnBhcGVyczpwODUtc2hhby5wZGYAAA4AGgAMAHAAOAA1AC0AcwBoAGEAbwAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAHlVzZXJzL3NpZWsvcGFwZXJzL3A4NS1zaGFvLnBkZgATAAEvAAAVAAIAC///AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAK0AsgC6AiQCJgIrAjYCPwJNAlECWAJhAmYCcwJ2AogCiwKQAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAApI=},
-	Bdsk-File-2 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YVxwODUtc2hhby5wZGbSFwsYGVdOUy5kYXRhTxEBggAAAAABggACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xDHA4NS1zaGFvLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAC/e6nRDzj0AAAAAAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA0Q9/RAAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgA6TWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6AHA4NS1zaGFvLnBkZgAOABoADABwADgANQAtAHMAaABhAG8ALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAClVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL3A4NS1zaGFvLnBkZgAAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCbAKAAqAIuAjACNQJAAkkCVwJbAmICawJwAn0CgAKSApUCmgAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAKc},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YVxwODUtc2hhby5wZGbSFwsYGVdOUy5kYXRhTxEBggAAAAABggACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xDHA4NS1zaGFvLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAC/e6nRDzj0AAAAAAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA0Q9/RAAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgA6TWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6AHA4NS1zaGFvLnBkZgAOABoADABwADgANQAtAHMAaABhAG8ALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAClVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL3A4NS1zaGFvLnBkZgAAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCbAKAAqAIuAjACNQJAAkkCVwJbAmICawJwAn0CgAKSApUCmgAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAKc},
 	Bdsk-Url-1 = {http://doi.acm.org/10.1145/258948.258958}}
 
 @article{Wright:1995cd,
@@ -29744,8 +30361,7 @@ over additional an arbitrary constraint system X.},
 	Institution = {Mathematics Unit Edinburgh University},
 	Title = {The Sharing of Structure in Resolution Programs},
 	Year = {1972},
-	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QKi4uLy4uLy4uL3BhcGVycy9zdHJ1Y3R1cmUtc2hhcmluZy1tZW1vLnBkZtIXCxgZV05TLmRhdGFPEQGeAAAAAAGeAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADBD6WHSCsAAABPmREac3RydWN0dXJlLXNoYXJpbmctbWVtby5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA8pJsEJ6TgAAAAAAAAAAAADAAIAAAkgAAAAAAAAAAAAAAAAAAAABnBhcGVycwAQAAgAAMEP+ecAAAARAAgAAMEKPZgAAAABAAwAT5kRAE6kUwBGyTYAAgA5TWFjaW50b3NoIEhEOlVzZXJzOnNpZWs6cGFwZXJzOnN0cnVjdHVyZS1zaGFyaW5nLW1lbW8ucGRmAAAOADYAGgBzAHQAcgB1AGMAdAB1AHIAZQAtAHMAaABhAHIAaQBuAGcALQBtAGUAbQBvAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAsVXNlcnMvc2llay9wYXBlcnMvc3RydWN0dXJlLXNoYXJpbmctbWVtby5wZGYAEwABLwAAFQACAAv//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgC7AMAAyAJqAmwCcQJ8AoUCkwKXAp4CpwKsArkCvALOAtEC1gAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAALY},
-	Bdsk-File-2 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QGnN0cnVjdHVyZS1zaGFyaW5nLW1lbW8ucGRm0hcLGBlXTlMuZGF0YU8RAboAAAAAAboAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAM3IwOpIKwAAAL9t8RpzdHJ1Y3R1cmUtc2hhcmluZy1tZW1vLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAv4ou0Q88lQAAAAAAAAAAAAEAAgAACSAAAAAAAAAAAAAAAAAAAAADYmliAAAQAAgAAM3I+SoAAAARAAgAANEPguUAAAABABAAv23xAUNoPAAFwHIAAhIpAAIASE1hY2ludG9zaCBIRDpVc2VyczoAanNpZWs6AEdvb2dsZSBEcml2ZToAYmliOgBzdHJ1Y3R1cmUtc2hhcmluZy1tZW1vLnBkZgAOADYAGgBzAHQAcgB1AGMAdAB1AHIAZQAtAHMAaABhAHIAaQBuAGcALQBtAGUAbQBvAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgA3VXNlcnMvanNpZWsvR29vZ2xlIERyaXZlL2JpYi9zdHJ1Y3R1cmUtc2hhcmluZy1tZW1vLnBkZgAAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCrALAAuAJ2AngCfQKIApECnwKjAqoCswK4AsUCyALaAt0C4gAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAALk}}
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QGnN0cnVjdHVyZS1zaGFyaW5nLW1lbW8ucGRm0hcLGBlXTlMuZGF0YU8RAboAAAAAAboAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAM3IwOpIKwAAAL9t8RpzdHJ1Y3R1cmUtc2hhcmluZy1tZW1vLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAv4ou0Q88lQAAAAAAAAAAAAEAAgAACSAAAAAAAAAAAAAAAAAAAAADYmliAAAQAAgAAM3I+SoAAAARAAgAANEPguUAAAABABAAv23xAUNoPAAFwHIAAhIpAAIASE1hY2ludG9zaCBIRDpVc2VyczoAanNpZWs6AEdvb2dsZSBEcml2ZToAYmliOgBzdHJ1Y3R1cmUtc2hhcmluZy1tZW1vLnBkZgAOADYAGgBzAHQAcgB1AGMAdAB1AHIAZQAtAHMAaABhAHIAaQBuAGcALQBtAGUAbQBvAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgA3VXNlcnMvanNpZWsvR29vZ2xlIERyaXZlL2JpYi9zdHJ1Y3R1cmUtc2hhcmluZy1tZW1vLnBkZgAAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCrALAAuAJ2AngCfQKIApECnwKjAqoCswK4AsUCyALaAt0C4gAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAALk}}
 
 @phdthesis{Choppella:2002in,
 	Address = {Bloomington, Indiana},
@@ -31565,8 +32181,7 @@ is used as an example.},
 	Series = {LNCS},
 	Title = {Structured proofs in {Isar}/{HOL}},
 	Year = {2002},
-	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QIS4uLy4uLy4uL3BhcGVycy9pc2FyLW92ZXJ2aWV3LnBkZtIXCxgZV05TLmRhdGFPEQF6AAAAAAF6AAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADBD6WHSCsAAABPmRERaXNhci1vdmVydmlldy5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA8l2MEJ6QgAAAAAAAAAAAADAAIAAAkgAAAAAAAAAAAAAAAAAAAABnBhcGVycwAQAAgAAMEP+ecAAAARAAgAAMEKPWgAAAABAAwAT5kRAE6kUwBGyTYAAgAwTWFjaW50b3NoIEhEOlVzZXJzOnNpZWs6cGFwZXJzOmlzYXItb3ZlcnZpZXcucGRmAA4AJAARAGkAcwBhAHIALQBvAHYAZQByAHYAaQBlAHcALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASACNVc2Vycy9zaWVrL3BhcGVycy9pc2FyLW92ZXJ2aWV3LnBkZgAAEwABLwAAFQACAAv//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCyALcAvwI9Aj8CRAJPAlgCZgJqAnECegJ/AowCjwKhAqQCqQAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAKr},
-	Bdsk-File-2 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QEWlzYXItb3ZlcnZpZXcucGRm0hcLGBlXTlMuZGF0YU8RAZYAAAAAAZYAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAM3IwOpIKwAAAL9t8RFpc2FyLW92ZXJ2aWV3LnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAv3Xk0Q83eAAAAAAAAAAAAAEAAgAACSAAAAAAAAAAAAAAAAAAAAADYmliAAAQAAgAAM3I+SoAAAARAAgAANEPfcgAAAABABAAv23xAUNoPAAFwHIAAhIpAAIAP01hY2ludG9zaCBIRDpVc2VyczoAanNpZWs6AEdvb2dsZSBEcml2ZToAYmliOgBpc2FyLW92ZXJ2aWV3LnBkZgAADgAkABEAaQBzAGEAcgAtAG8AdgBlAHIAdgBpAGUAdwAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIALlVzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvaXNhci1vdmVydmlldy5wZGYAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCiAKcArwJJAksCUAJbAmQCcgJ2An0ChgKLApgCmwKtArACtQAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAK3}}
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QEWlzYXItb3ZlcnZpZXcucGRm0hcLGBlXTlMuZGF0YU8RAZYAAAAAAZYAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAM3IwOpIKwAAAL9t8RFpc2FyLW92ZXJ2aWV3LnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAv3Xk0Q83eAAAAAAAAAAAAAEAAgAACSAAAAAAAAAAAAAAAAAAAAADYmliAAAQAAgAAM3I+SoAAAARAAgAANEPfcgAAAABABAAv23xAUNoPAAFwHIAAhIpAAIAP01hY2ludG9zaCBIRDpVc2VyczoAanNpZWs6AEdvb2dsZSBEcml2ZToAYmliOgBpc2FyLW92ZXJ2aWV3LnBkZgAADgAkABEAaQBzAGEAcgAtAG8AdgBlAHIAdgBpAGUAdwAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIALlVzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvaXNhci1vdmVydmlldy5wZGYAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCiAKcArwJJAksCUAJbAmQCcgJ2An0ChgKLApgCmwKtArACtQAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAK3}}
 
 @incollection{Moggi:1989pf,
 	Address = {Washington, DC},
@@ -32001,8 +32616,7 @@ software productivity and reliability },
 	Publisher = {ACM Press},
 	Title = {Unboxed objects and polymorphic typing},
 	Year = {1992},
-	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QHi4uLy4uLy4uL3BhcGVycy9wMTc3LWxlcm95LnBkZtIXCxgZV05TLmRhdGFPEQFuAAAAAAFuAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADBD6WHSCsAAABPmREOcDE3Ny1sZXJveS5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA8m3cEJ6RMAAAAAAAAAAAADAAIAAAkgAAAAAAAAAAAAAAAAAAAABnBhcGVycwAQAAgAAMEP+ecAAAARAAgAAMEKPXMAAAABAAwAT5kRAE6kUwBGyTYAAgAtTWFjaW50b3NoIEhEOlVzZXJzOnNpZWs6cGFwZXJzOnAxNzctbGVyb3kucGRmAAAOAB4ADgBwADEANwA3AC0AbABlAHIAbwB5AC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAgVXNlcnMvc2llay9wYXBlcnMvcDE3Ny1sZXJveS5wZGYAEwABLwAAFQACAAv//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCvALQAvAIuAjACNQJAAkkCVwJbAmICawJwAn0CgAKSApUCmgAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAKc},
-	Bdsk-File-2 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV5wMTc3LWxlcm95LnBkZtIXCxgZV05TLmRhdGFPEQGKAAAAAAGKAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEOcDE3Ny1sZXJveS5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAL96BdEPOPAAAAAAAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADRD39AAAAAAQAQAL9t8QFDaDwABcByAAISKQACADxNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAcDE3Ny1sZXJveS5wZGYADgAeAA4AcAAxADcANwAtAGwAZQByAG8AeQAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAK1VzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvcDE3Ny1sZXJveS5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AnQCiAKoCOAI6Aj8CSgJTAmECZQJsAnUCegKHAooCnAKfAqQAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAACpg==},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV5wMTc3LWxlcm95LnBkZtIXCxgZV05TLmRhdGFPEQGKAAAAAAGKAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEOcDE3Ny1sZXJveS5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAL96BdEPOPAAAAAAAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADRD39AAAAAAQAQAL9t8QFDaDwABcByAAISKQACADxNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAcDE3Ny1sZXJveS5wZGYADgAeAA4AcAAxADcANwAtAGwAZQByAG8AeQAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAK1VzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvcDE3Ny1sZXJveS5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AnQCiAKoCOAI6Aj8CSgJTAmECZQJsAnUCegKHAooCnAKfAqQAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAACpg==},
 	Bdsk-Url-1 = {http://doi.acm.org/10.1145/143165.143205}}
 
 @inproceedings{Lee:1999ry,

book.tex

@@ -2929,8 +2929,46 @@ the \code{and} operation is short-circuiting. That is, the second
 expression \code{e2} is not evaluated if \code{e1} evaluates to
 \code{\#f}.
 
+With the addition of the comparison operations, there are quite a few
+primitive operations and the interpreter code for them is somewhat
+repetitive. In Figure~\ref{fig:interp-R2} we factor out the different
+parts into the \code{interp-op} function and the similar parts into
+the one match clause shown in Figure~\ref{fig:interp-R2}. It is
+important for that match clause to come last because it matches
+\emph{any} compound S-expression.  We do not use \code{interp-op} for
+the \code{and} operation because of the short-circuiting behavior in
+the order of evaluation of its arguments.
+
+
 \begin{figure}[tbp]
 \begin{lstlisting}
+    (define primitives (set '+ '- 'eq? '< '<= '> '>= 'not 'read))
+
+    (define (interp-op op)
+      (match op
+         ['+ fx+]
+         ['- (lambda (n) (fx- 0 n))]
+         ['not (lambda (v) (match v [#t #f] [#f #t]))]
+	 ['read read-fixnum]
+         ['eq? (lambda (v1 v2)
+                 (cond [(or (and (fixnum? v1) (fixnum? v2))
+                            (and (boolean? v1) (boolean? v2))
+                            (and (vector? v1) (vector? v2)))
+                        (eq? v1 v2)]))]
+         ['< (lambda (v1 v2)
+                 (cond [(and (fixnum? v1) (fixnum? v2))
+                        (< v1 v2)]))]
+         ['<= (lambda (v1 v2)
+                 (cond [(and (fixnum? v1) (fixnum? v2))
+                        (<= v1 v2)]))]
+         ['> (lambda (v1 v2)
+                 (cond [(and (fixnum? v1) (fixnum? v2))
+                        (<= v1 v2)]))]
+         ['>= (lambda (v1 v2)
+                 (cond [(and (fixnum? v1) (fixnum? v2))
+                        (<= v1 v2)]))]
+	 [else (error 'interp-op "unknown operator")]))
+
    (define (interp-R2 env e)
      (match e
        ...
@@ -2945,10 +2983,8 @@ expression \code{e2} is not evaluated if \code{e1} evaluates to
          (match (interp-R2 env e1)
            [#t (match (interp-R2 env e2) [#t #t] [#f #f])]
            [#f #f])]
-       [`(eq? ,e1 ,e2)
-         (let ([v1 (interp-R2 env e1)] [v2 (interp-R2 env e2)])
-           (cond [(and (fixnum? v1) (fixnum? v2)) (eq? v1 v2)]
-                 [(and (boolean? v1) (boolean? v2)) (eq? v1 v2)]))]
+       [`(,op ,args ...) #:when (set-member? primitives op)
+         (apply (interp-op op) (map (interp-R2 env) args))]
        ))
 \end{lstlisting}
 \caption{Interpreter for the $R_2$ language.}
@@ -3233,8 +3269,8 @@ So $0011 \mathrel{\mathrm{XOR}} 0101 = 0110$.
        \mid (\key{cmpq} \; \Arg\; \Arg) \mid (\key{set}\;\itm{cc} \; \Arg) \\
        &\mid& (\key{movzbq}\;\Arg\;\Arg) 
        \mid  (\key{jmp} \; \itm{label}) 
-       \mid (\key{jmp-if}\; \itm{cc} \; \itm{label})
-       \mid (\key{label} \; \itm{label}) \\
+       \mid (\key{jmp-if}\; \itm{cc} \; \itm{label}) \\
+       &\mid& (\key{label} \; \itm{label}) \\
 x86_1 &::= & (\key{program} \;\itm{info} \;(\key{type}\;\itm{type})\; \Instr^{+})
 \end{array}
 \]
@@ -3726,6 +3762,9 @@ if_end21289:
   things to discuss in this chapter. \\ --Jeremy}
 \marginpar{\scriptsize To do: Flesh out this chapter, e.g., make sure
   all the IR grammars are spelled out! \\ --Jeremy}
+\marginpar{\scriptsize Introduce has-type, but after flatten, remove it,
+  but keep type annotations on vector creation and local variables, function
+  parameters, etc. \\ --Jeremy}
 
 In this chapter we study the implementation of mutable tuples (called
 ``vectors'' in Racket). This language feature is the first to require
@@ -3757,15 +3796,7 @@ which we add the $2$, the element at index $0$ of the 1-tuple.
 \end{lstlisting}
 
 Figure~\ref{fig:interp-R3} shows the interpreter for the $R_3$
-language. With the addition of the vector operations, there are quite
-a few primitive operations and the interpreter code for them is
-somewhat repetitive. In Figure~\ref{fig:interp-R3} we factor out the
-different parts into the \code{interp-op} function and the similar
-parts into the one match clause shown in
-Figure~\ref{fig:interp-R3}. It is important for that match clause to
-come last because it matches \emph{any} compound S-expression.  We do
-not use \code{interp-op} for the \code{and} operation because of the
-short-circuiting behavior in the order of evaluation of its arguments.
+language. 
 
 \begin{figure}[tp]
 \centering
@@ -3797,21 +3828,13 @@ short-circuiting behavior in the order of evaluation of its arguments.
 
 \begin{figure}[tbp]
 \begin{lstlisting}
-    (define primitives (set '+ '- 'eq? 'not 'read 
-                         'vector 'vector-ref 'vector-set!))
+    (define primitives (set ... 'vector 'vector-ref 'vector-set!))
 
     (define (interp-op op)
       (match op
-         ['+ fx+]
-         ['- (lambda (n) (fx- 0 n))]
-         ['eq? (lambda (v1 v2)
-                 (cond [(or (and (fixnum? v1) (fixnum? v2))
-                            (and (boolean? v1) (boolean? v2))
-                            (and (vector? v1) (vector? v2)))
-                        (eq? v1 v2)]))]
-         ['not (lambda (v) (match v [#t #f] [#f #t]))]
-	 ['read read-fixnum]
-         ['vector vector] ['vector-ref vector-ref]
+         ...
+         ['vector vector]
+         ['vector-ref vector-ref]
 	 ['vector-set! vector-set!]
 	 [else (error 'interp-op "unknown operator")]))
 
@@ -3819,8 +3842,6 @@ short-circuiting behavior in the order of evaluation of its arguments.
      (lambda (e)
        (match e
          ...
-         [`(,op ,args ...) #:when (set-member? primitives op)
-           (apply (interp-op op) (map (interp-R3 env) args))]
          [else (error 'interp-R3 "unrecognized expression")]
          )))
 \end{lstlisting}
@@ -4101,7 +4122,7 @@ via two vector references.
 \end{lstlisting}
 
 
-\subsection{Flatten}
+\subsection{Flatten and the $C_2$ intermediate language}
 
 \begin{figure}[tp]
 \fbox{
@@ -4325,9 +4346,6 @@ function in \code{runtime.c}.
 We translate the special \code{collection-needed?} predicate into code
 that compares the \code{free\_ptr} to the \code{fromspace\_end}.
 %
-\marginpar{\tiny To improve the code generation here, we should
- extend the 'if' form to all the relational operators.\\--Jeremy}
-%
 \begin{lstlisting}
    (if (collection-needed? |$\itm{bytes}$|) |$\itm{thn}$| |$\itm{els}$|)
    |$\Longrightarrow$|
@@ -4349,13 +4367,13 @@ least, we need to initialize the \itm{tag}. Refer to
 Figure~\ref{fig:tuple-rep} to see how the tag is organized. We
 recommend using the Racket operations \code{bitwise-ior} and
 \code{arithmetic-shift} to compute the tag.  The \itm{types} in the
-type annotation in the \code{allocate} form can be used to determine
+\code{has-type } annotation can be used to determine
 the pointer mask region of the tag. The move of $ \itm{lhs}^\prime $ to
 register \code{r11}, before the move to the offset of \code{r11}
 ensures that if $ \itm{lhs}^\prime $ offsets are only performed with
 register operands.
 \begin{lstlisting}
-   (assign |$\itm{lhs}$| (allocate |$\itm{len}$| (Vector |$\itm{types}$|)))
+   (assign |$\itm{lhs}$| (hash-type (allocate |$\itm{len}$|) (Vector |$\itm{types}$|)))
    |$\Longrightarrow$|
    (movq (global-value free_ptr) |$\itm{lhs}'$|)
    (addq (int |$8(\itm{len}+1)$|) (global-value free_ptr))
@@ -4389,8 +4407,9 @@ processing $\itm{vec}$ and $\itm{arg}$.
 \[
 \begin{array}{lcl}
 \Arg &::=&  \gray{  \INT{\Int} \mid \REG{\itm{register}}
-    \mid (\key{deref}\,\itm{register}\,\Int) \mid (\key{byte-reg}\; \itm{register})  } \\ 
-   &\mid& (\key{global-value}\; \itm{name}) \\
+    \mid (\key{deref}\,\itm{register}\,\Int) } \\
+   &\mid& \gray{ (\key{byte-reg}\; \itm{register})  } 
+   \mid (\key{global-value}\; \itm{name}) \\
 \itm{cc} & ::= & \gray{  \key{e} \mid \key{l} \mid \key{le} \mid \key{g} \mid \key{ge}  } \\
 \Instr &::=& \gray{(\key{addq} \; \Arg\; \Arg) \mid 
              (\key{subq} \; \Arg\; \Arg) \mid 
@@ -4628,6 +4647,7 @@ inside each other; they can only be defined at the top level.
 \begin{array}{lcl}
   \Type &::=& \gray{ \key{Integer} \mid \key{Boolean}
          \mid (\key{Vector}\;\Type^{+}) \mid \key{Void}  } \mid (\Type^{*} \; \key{->}\; \Type) \\
+\itm{cmp} &::= & \gray{  \key{eq?} \mid \key{<} \mid \key{<=} \mid \key{>} \mid \key{>=}  } \\
   \Exp &::=& \gray{ \Int \mid (\key{read}) \mid (\key{-}\;\Exp) \mid (\key{+} \; \Exp\;\Exp)}  \\
      &\mid&  \gray{ \Var \mid \LET{\Var}{\Exp}{\Exp} }\\
     &\mid& \gray{ \key{\#t} \mid \key{\#f} \mid
@@ -4673,8 +4693,36 @@ that does what its name suggests. The program then applies
 \label{fig:r4-function-example}
 \end{figure}
 
+The definitional interpreter for $R_4$ is in
+Figure~\ref{fig:interp-R4}.
+
+
+\begin{figure}[tp]
+\begin{lstlisting}
+   (define (interp-R4 env)
+     (lambda (e)
+       (match e
+          ....
+          [`(define (,f [,xs : ,ps] ...) : ,rt ,body)
+           (cons f `(lambda ,xs ,body))]
+          [`(program ,ds ... ,body)
+           (let ([top-level (map  (interp-R4 '()) ds)])
+	      ((interp-R4 top-level) body))]
+          [`(,fun ,args ...)
+	    (define arg-vals (map (interp-R4 env) args))
+            (define fun-val ((interp-R4 env) fun))
+            (match fun-val
+               [`(lambda (,xs ...) ,body)
+                 (define new-env (append (map cons xs arg-vals) env))
+ 		 ((interp-R4 new-env) body)]
+               [else (error "interp-R4, expected function, not" fun-val)]))]
+         [else (error 'interp-R4 "unrecognized expression")]
+         )))
+\end{lstlisting}
+\caption{Interpreter for the $R_4$ language.}
+\label{fig:interp-R4}
+\end{figure}
 
-\marginpar{\scriptsize to do: interpreter for $R_4$. \\ --Jeremy}
 
 \section{Functions in x86}
 \label{sec:fun-x86}
@@ -4806,7 +4854,7 @@ kinds of AST nodes to any of the intermediate languages?
   &\mid& \gray{(\key{vector}\;\Exp^{+}) \mid 
     (\key{vector-ref}\;\Exp\;\Int)} \\
   &\mid& \gray{(\key{vector-set!}\;\Exp\;\Int\;\Exp)\mid (\key{void})} \\
-      &\mid& (app\, \Exp \; \Exp^{*}) \\
+      &\mid& (\key{app}\, \Exp \; \Exp^{*}) \\
   \Def &::=& (\key{define}\; (\itm{label} \; [\Var \key{:} \Type]^{*}) \key{:} \Type \; \Exp) \\
   F_1 &::=& (\key{program} \; \Def^{*} \; \Exp)
 \end{array}
@@ -4855,7 +4903,7 @@ Figure~\ref{fig:c3-syntax} defines the syntax for $C_3$, the output of
    &\mid& \gray{  (\key{vector}\, \Arg^{+}) 
    \mid (\key{vector-ref}\, \Arg\, \Int)  } \\
    &\mid& \gray{  (\key{vector-set!}\,\Arg\,\Int\,\Arg)  } \\
-   &\mid& (app \,\Arg\,\Arg^{*}) \\
+   &\mid& (\key{app} \,\Arg\,\Arg^{*}) \\
 \Stmt &::=& \gray{ \ASSIGN{\Var}{\Exp} \mid \RETURN{\Arg} } \\
       &\mid& \gray{ \IF{(\itm{cmp}\, \Arg\,\Arg)}{\Stmt^{*}}{\Stmt^{*}} } \\
       &\mid& \gray{ (\key{initialize}\,\itm{int}\,\itm{int}) }\\
@@ -5294,26 +5342,27 @@ top-level environment.
 (define (interp-R5 env)
   (lambda (ast)
     (match ast
+       ...
        [`(lambda: ([,xs : ,Ts] ...) : ,rT ,body)
         `(lambda ,xs ,body ,env)]
-       [`(app ,fun ,args ...)
-        (define arg-vals (map (interp-R5 env) args))
-        (define fun-val ((interp-R5 env) fun))
-        (match fun-val
-           [`(lambda (,xs ...) ,body ,lam-env)
-            (define new-env (append (map cons xs arg-vals) lam-env))
-            ((interp-R5 new-env) body)]
-           [else (error "interp-R5, expected function, not" fun-val)])]
        [`(define (,f [,xs : ,ps] ...) : ,rt ,body)
         (mcons f `(lambda ,xs ,body))]
        [`(program ,defs ... ,body)
         (let ([top-level (map (interp-R5 '()) defs)])
           (for/list ([b top-level])
                     (set-mcdr! b (match (mcdr b)
-                                   [`(lambda ,xs ,body)
-                                    `(lambda ,xs ,body ,top-level)])))
+                                    [`(lambda ,xs ,body)
+                                     `(lambda ,xs ,body ,top-level)])))
           ((interp-R5 top-level) body))]
-       ...)))
+       [`(,fun ,args ...)
+        (define arg-vals (map (interp-R5 env) args))
+        (define fun-val ((interp-R5 env) fun))
+        (match fun-val
+           [`(lambda (,xs ...) ,body ,lam-env)
+            (define new-env (append (map cons xs arg-vals) lam-env))
+            ((interp-R5 new-env) body)]
+           [else (error "interp-R5, expected function, not" fun-val)])]
+       )))
 \end{lstlisting}
 \caption{Definitional interpreter for $R_5$.}
 \label{fig:interp-R5}
@@ -5586,12 +5635,13 @@ compilation of $R_6$ and $R_7$ in the remainder of this chapter.
     &\mid& \gray{(\Type^{*} \; \key{->}\; \Type)} \mid \key{Any} \\
   \FType &::=& \key{Integer} \mid \key{Boolean} \mid (\key{Vectorof}\;\key{Any})
      \mid (\key{Any}^{*} \; \key{->}\; \key{Any})\\
+  \itm{cmp} &::= & \key{eq?} \mid \key{<} \mid \key{<=} \mid \key{>} \mid \key{>=} \\
   \Exp &::=& \gray{\Int \mid (\key{read}) \mid (\key{-}\;\Exp) 
      \mid (\key{+} \; \Exp\;\Exp)}  \\
     &\mid&  \gray{\Var \mid \LET{\Var}{\Exp}{\Exp}} \\
     &\mid& \gray{\key{\#t} \mid \key{\#f} \mid
            (\key{and}\;\Exp\;\Exp) \mid (\key{not}\;\Exp)} \\
-    &\mid& \gray{(\key{eq?}\;\Exp\;\Exp) \mid \IF{\Exp}{\Exp}{\Exp}} \\
+    &\mid& \gray{(\itm{cmp}\;\Exp\;\Exp) \mid \IF{\Exp}{\Exp}{\Exp}} \\
     &\mid& \gray{(\key{vector}\;\Exp^{+}) \mid 
           (\key{vector-ref}\;\Exp\;\Int)} \\
     &\mid& \gray{(\key{vector-set!}\;\Exp\;\Int\;\Exp)\mid (\key{void})} \\
@@ -5710,11 +5760,12 @@ for $R_6$.
 \begin{minipage}{0.97\textwidth}
 \[
 \begin{array}{rcl}
+  \itm{cmp} &::= & \key{eq?} \mid \key{<} \mid \key{<=} \mid \key{>} \mid \key{>=} \\
 \Exp &::=& \Int \mid (\key{read}) \mid (\key{-}\;\Exp) \mid (\key{+} \; \Exp\;\Exp)  \\
      &\mid&  \Var \mid \LET{\Var}{\Exp}{\Exp} \\
      &\mid& \key{\#t} \mid \key{\#f} \mid
       (\key{and}\;\Exp\;\Exp) \mid (\key{not}\;\Exp) \\
-     &\mid& (\key{eq?}\;\Exp\;\Exp) \mid \IF{\Exp}{\Exp}{\Exp} \\
+     &\mid& (\itm{cmp}\;\Exp\;\Exp) \mid \IF{\Exp}{\Exp}{\Exp} \\
      &\mid& (\key{vector}\;\Exp^{+}) \mid 
       (\key{vector-ref}\;\Exp\;\Exp) \\
   &\mid& (\key{vector-set!}\;\Exp\;\Exp\;\Exp) \mid (\key{void}) \\
@@ -6021,16 +6072,26 @@ $\Rightarrow$
 \chapter{Gradual Typing}
 \label{ch:gradual-typing}
 
+This chapter will be based on the ideas of \citet{Siek:2006bh}.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \chapter{Parametric Polymorphism}
 \label{ch:parametric-polymorphism}
 
+This chapter may be based on ideas from \citet{Cardelli:1984aa},
+\citet{Leroy:1992qb}, \citet{Shao:1997uj}, or \citet{Harper:1995um}.
+
+
+
+
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \chapter{High-level Optimization}
 \label{ch:high-level-optimization}
 
+This chapter will present a procedure inlining pass based on the
+algorithm of \citet{Waddell:1997fk}.
+
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \chapter{Appendix}