Jeremy Siek 9 anni fa
parent
commit
1f3e15fa5c
6 ha cambiato i file con 701 aggiunte e 99 eliminazioni
  1. 538 27
      all.bib
  2. 163 72
      book.tex
  3. BIN
      copy-collect-1.graffle
  4. BIN
      copy-collect-1.pdf
  5. BIN
      copy-collect-2.graffle
  6. BIN
      copy-collect-2.pdf

+ 538 - 27
all.bib

@@ -2,13 +2,531 @@
 %% http://bibdesk.sourceforge.net/
 
 
-%% Created for Jeremy Siek at 2016-03-29 22:03:07 -0400 
+%% Created for Jeremy Siek at 2016-05-20 13:19:42 -0400 
 
 
 %% Saved with string encoding Unicode (UTF-8) 
 
 
 
+@techreport{Dijkstra:1982aa,
+	Author = {E. W. Dijkstra},
+	Date-Added = {2016-05-20 17:16:31 +0000},
+	Date-Modified = {2016-05-20 17:18:04 +0000},
+	Institution = {University of Texas at Austin},
+	Number = {EWD831},
+	Title = {Why numbering should start at zero},
+	Year = {1982},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YVpFV0Q4MzEucGRm0hcLGBlXTlMuZGF0YU8RAXoAAAAAAXoAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAM3IwOpIKwAAAL9t8QpFV0Q4MzEucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABfI6B02S/VVBERiAAAAAAAAEAAgAACSAAAAAAAAAAAAAAAAAAAAADYmliAAAQAAgAAM3I+SoAAAARAAgAANNk95UAAAABABAAv23xAUNoPAAFwHIAAhIpAAIAOE1hY2ludG9zaCBIRDpVc2VyczoAanNpZWs6AEdvb2dsZSBEcml2ZToAYmliOgBFV0Q4MzEucGRmAA4AFgAKAEUAVwBEADgAMwAxAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAnVXNlcnMvanNpZWsvR29vZ2xlIERyaXZlL2JpYi9FV0Q4MzEucGRmAAATAAEvAAAVAAIADP//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAJkAngCmAiQCJgIrAjYCPwJNAlECWAJhAmYCcwJ2AogCiwKQAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAApI=}}
+
+@inproceedings{Friedman:1976ab,
+	Author = {Daniel P. Friedman and David S. Wise},
+	Booktitle = {International Conference on Parallel Processing},
+	Date-Added = {2016-05-13 18:35:32 +0000},
+	Date-Modified = {2016-05-13 18:36:10 +0000},
+	Title = {The impact of applicative programming on multiprocessing},
+	Year = {1976}}
+
+@article{Hoare:1974aa,
+	Acmid = {361161},
+	Address = {New York, NY, USA},
+	Author = {Hoare, C. A. R.},
+	Date-Added = {2016-05-13 18:26:32 +0000},
+	Date-Modified = {2016-05-13 18:26:35 +0000},
+	Doi = {10.1145/355620.361161},
+	Issn = {0001-0782},
+	Issue_Date = {Oct. 1974},
+	Journal = {Commun. ACM},
+	Keywords = {monitors, mutual exclusion, operating systems, scheduling, structured multiprogramming, synchronization, system implementation languages},
+	Month = oct,
+	Number = {10},
+	Numpages = {9},
+	Pages = {549--557},
+	Publisher = {ACM},
+	Title = {Monitors: An Operating System Structuring Concept},
+	Url = {http://doi.acm.org/10.1145/355620.361161},
+	Volume = {17},
+	Year = {1974},
+	Bdsk-Url-1 = {http://doi.acm.org/10.1145/355620.361161},
+	Bdsk-Url-2 = {http://dx.doi.org/10.1145/355620.361161}}
+
+@book{Hansen:1973aa,
+	Address = {Upper Saddle River, NJ, USA},
+	Author = {Hansen, Per Brinch},
+	Date-Added = {2016-05-13 18:26:02 +0000},
+	Date-Modified = {2016-05-13 18:26:05 +0000},
+	Isbn = {0-13-637843-9},
+	Publisher = {Prentice-Hall, Inc.},
+	Title = {Operating System Principles},
+	Year = {1973}}
+
+@inproceedings{Sterling:2014ab,
+	Address = {Stockholm, Sweden},
+	Author = {Thomas Sterling and Matthew Anderson and P. Kevin Bohan and Maciej Brodowicz and Abhishek Kulkarni and Bo Zhang},
+	Booktitle = {Exascale Applications and Software Conference},
+	Date-Added = {2016-05-13 17:28:07 +0000},
+	Date-Modified = {2016-05-13 17:28:10 +0000},
+	Keywords = {HPX},
+	Month = {Apr},
+	Title = {Towards Exascale Co-design in a Runtime System},
+	Year = 2014}
+
+@inproceedings{Anderson:2014ab,
+	Address = {Leipzig, Germany},
+	Author = {Matthew Anderson and Maciej Brodowicz and Luke Dalessandro and Jackson DeBuhr and Thomas Sterling},
+	Booktitle = {29th International Supercomputing Conference (ISC), 2014},
+	Date-Added = {2016-05-13 17:27:36 +0000},
+	Date-Modified = {2016-05-13 17:27:39 +0000},
+	Keywords = {HPX},
+	Month = {Jun},
+	Title = {A dynamic execution model applied to distributed collision detection},
+	Year = 2014}
+
+@inproceedings{Zhang:2014aa,
+	Address = {Edmonton, Canada},
+	Author = {B. Zhang},
+	Booktitle = {Forth Workshop on Data-Flow Execution Models for Extreme Scale Computing},
+	Date-Added = {2016-05-13 17:26:52 +0000},
+	Date-Modified = {2016-05-13 17:26:55 +0000},
+	Keywords = {HPX},
+	Month = {August},
+	Pdf = {http://www.cs.ucy.ac.cy/dfmworkshop/wp-content/uploads/2014/08/DFM2014-4-Asynchronous-Task-Scheduling-of-the-Fast-Multipole-Method-using-various-Runtime-Systems.pdf},
+	Title = {Asynchronous task scheduling of the fast multipole method using various runtime systems},
+	Year = {2014}}
+
+@article{Luth:2009aa,
+	Annote = {graspable logic},
+	Author = {Christoph L{\"u}th},
+	Date-Added = {2016-05-13 12:27:54 +0000},
+	Date-Modified = {2016-05-13 12:29:02 +0000},
+	Journal = {Electronic Communications of the EASST},
+	Title = {User Interfaces for Theorem Provers: Necessary Nuisance or Unexplored Potential?},
+	Volume = {23},
+	Year = {2009},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QEDMyMi05NDgtMS1QQi5wZGbSFwsYGVdOUy5kYXRhTxEBkgAAAAABkgACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xEDMyMi05NDgtMS1QQi5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAF7F/PTW0DCUERGIAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA01t5AgAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgA+TWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6ADMyMi05NDgtMS1QQi5wZGYADgAiABAAMwAyADIALQA5ADQAOAAtADEALQBQAEIALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAC1Vc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliLzMyMi05NDgtMS1QQi5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AoQCmAK4CRAJGAksCVgJfAm0CcQJ4AoEChgKTApYCqAKrArAAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAACsg==}}
+
+@article{Bertot:1998aa,
+	Annote = {graspable logic},
+	Author = {Y. Bertot and L. Th{\'e}ry},
+	Date-Added = {2016-05-13 12:25:08 +0000},
+	Date-Modified = {2016-05-13 12:25:22 +0000},
+	Doi = {http://dx.doi.org/10.1006/jsco.1997.0171},
+	Issn = {0747-7171},
+	Journal = {Journal of Symbolic Computation},
+	Number = {2},
+	Pages = {161 - 194},
+	Title = {A Generic Approach to Building User Interfaces for Theorem Provers},
+	Url = {http://www.sciencedirect.com/science/article/pii/S0747717197901711},
+	Volume = {25},
+	Year = {1998},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QFWdlbmVyaWMtdWktcHJvdmVyLnBkZtIXCxgZV05TLmRhdGFPEQGmAAAAAAGmAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEVZ2VuZXJpYy11aS1wcm92ZXIucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAXsW7NNbP99QREYgAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADTW3gfAAAAAQAQAL9t8QFDaDwABcByAAISKQACAENNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAZ2VuZXJpYy11aS1wcm92ZXIucGRmAAAOACwAFQBnAGUAbgBlAHIAaQBjAC0AdQBpAC0AcAByAG8AdgBlAHIALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASADJVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL2dlbmVyaWMtdWktcHJvdmVyLnBkZgATAAEvAAAVAAIADP//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAKYAqwCzAl0CXwJkAm8CeAKGAooCkQKaAp8CrAKvAsECxALJAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAAss=},
+	Bdsk-Url-1 = {http://www.sciencedirect.com/science/article/pii/S0747717197901711},
+	Bdsk-Url-2 = {http://dx.doi.org/10.1006/jsco.1997.0171}}
+
+@article{Gast:2012aa,
+	Author = {Holger Gast},
+	Date-Added = {2016-05-13 12:21:59 +0000},
+	Date-Modified = {2016-05-13 12:22:03 +0000},
+	Doi = {http://dx.doi.org/10.1016/j.entcs.2012.06.002},
+	Issn = {1571-0661},
+	Journal = {Electronic Notes in Theoretical Computer Science},
+	Keywords = {software quality},
+	Note = {Proceedings of the 9th International Workshop On User Interfaces for Theorem Provers (UITP10)},
+	Pages = {3 - 16},
+	Title = {Engineering the Prover Interface},
+	Url = {http://www.sciencedirect.com/science/article/pii/S1571066112000229},
+	Volume = {285},
+	Year = {2012},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QGGVuZy1wcm92ZXItaW50ZXJmYWNlLnBkZtIXCxgZV05TLmRhdGFPEQGyAAAAAAGyAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEYZW5nLXByb3Zlci1pbnRlcmZhY2UucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAXsWIdNbPwRQREYgAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADTW3dEAAAAAQAQAL9t8QFDaDwABcByAAISKQACAEZNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAZW5nLXByb3Zlci1pbnRlcmZhY2UucGRmAA4AMgAYAGUAbgBnAC0AcAByAG8AdgBlAHIALQBpAG4AdABlAHIAZgBhAGMAZQAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIANVVzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvZW5nLXByb3Zlci1pbnRlcmZhY2UucGRmAAATAAEvAAAVAAIADP//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAKkArgC2AmwCbgJzAn4ChwKVApkCoAKpAq4CuwK+AtAC0wLYAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAAto=},
+	Bdsk-Url-1 = {http://www.sciencedirect.com/science/article/pii/S1571066112000229},
+	Bdsk-Url-2 = {http://dx.doi.org/10.1016/j.entcs.2012.06.002}}
+
+@article{Pham:2012aa,
+	Acmid = {2372038},
+	Address = {Amsterdam, The Netherlands, The Netherlands},
+	Annote = {related to graspable math and logic, and geogebra},
+	Author = {Pham, Tuan Minh and Bertot, Yves},
+	Date-Added = {2016-05-13 12:17:59 +0000},
+	Date-Modified = {2016-05-13 12:19:24 +0000},
+	Doi = {10.1016/j.entcs.2012.06.005},
+	Issn = {1571-0661},
+	Issue_Date = {September, 2012},
+	Journal = {Electron. Notes Theor. Comput. Sci.},
+	Keywords = {Coq, dynamic geometry, interactive geometric proofs, proof assistant},
+	Month = sep,
+	Numpages = {13},
+	Pages = {43--55},
+	Publisher = {Elsevier Science Publishers B. V.},
+	Title = {A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs},
+	Url = {http://dx.doi.org/10.1016/j.entcs.2012.06.005},
+	Volume = {285},
+	Year = {2012},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QFmR5bi1nZW9tZXRyeS1wcm9vZi5wZGbSFwsYGVdOUy5kYXRhTxEBqgAAAAABqgACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xFmR5bi1nZW9tZXRyeS1wcm9vZi5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAF7FXLTWz5jUERGIAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA01t2owAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgBETWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6AGR5bi1nZW9tZXRyeS1wcm9vZi5wZGYADgAuABYAZAB5AG4ALQBnAGUAbwBtAGUAdAByAHkALQBwAHIAbwBvAGYALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASADNVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL2R5bi1nZW9tZXRyeS1wcm9vZi5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4ApwCsALQCYgJkAmkCdAJ9AosCjwKWAp8CpAKxArQCxgLJAs4AAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAAC0A==},
+	Bdsk-Url-1 = {http://dx.doi.org/10.1016/j.entcs.2012.06.005}}
+
+@article{Stoutemyer:2014aa,
+	Acmid = {2576827},
+	Address = {New York, NY, USA},
+	Annote = {related to graspable math},
+	Author = {Stoutemyer, David R.},
+	Date-Added = {2016-05-13 12:13:52 +0000},
+	Date-Modified = {2016-05-13 12:14:28 +0000},
+	Doi = {10.1145/2576802.2576827},
+	Issn = {1932-2240},
+	Issue_Date = {September/December 2013},
+	Journal = {ACM Commun. Comput. Algebra},
+	Month = jan,
+	Number = {3/4},
+	Numpages = {36},
+	Pages = {130--165},
+	Publisher = {ACM},
+	Title = {A Computer Algebra User Interface Manifesto},
+	Url = {http://doi.acm.org/10.1145/2576802.2576827},
+	Volume = {47},
+	Year = {2014},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QE3AxMzAtc3RvdXRlbXllci5wZGbSFwsYGVdOUy5kYXRhTxEBngAAAAABngACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xE3AxMzAtc3RvdXRlbXllci5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAF7En/TWz1WUERGIAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA01t1lgAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgBBTWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6AHAxMzAtc3RvdXRlbXllci5wZGYAAA4AKAATAHAAMQAzADAALQBzAHQAbwB1AHQAZQBtAHkAZQByAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAwVXNlcnMvanNpZWsvR29vZ2xlIERyaXZlL2JpYi9wMTMwLXN0b3V0ZW15ZXIucGRmABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4ApACpALECUwJVAloCZQJuAnwCgAKHApAClQKiAqUCtwK6Ar8AAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAACwQ==},
+	Bdsk-Url-1 = {http://doi.acm.org/10.1145/2576802.2576827},
+	Bdsk-Url-2 = {http://dx.doi.org/10.1145/2576802.2576827}}
+
+@inbook{Chaudhuri:2013aa,
+	Address = {Berlin, Heidelberg},
+	Annote = {related to graspable logic},
+	Author = {Chaudhuri, Kaustuv},
+	Chapter = {Subformula Linking as an Interaction Method},
+	Date-Added = {2016-05-13 12:10:55 +0000},
+	Date-Modified = {2016-05-13 12:11:38 +0000},
+	Doi = {10.1007/978-3-642-39634-2_28},
+	Editor = {Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David},
+	Isbn = {978-3-642-39634-2},
+	Pages = {386--401},
+	Publisher = {Springer Berlin Heidelberg},
+	Title = {Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings},
+	Url = {http://dx.doi.org/10.1007/978-3-642-39634-2_28},
+	Year = {2013},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV1pdHAxM2xpbmsucGRm0hcLGBlXTlMuZGF0YU8RAYYAAAAAAYYAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAM3IwOpIKwAAAL9t8Q1pdHAxM2xpbmsucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABexHv01s8nVBERiAAAAAAAAEAAgAACSAAAAAAAAAAAAAAAAAAAAADYmliAAAQAAgAAM3I+SoAAAARAAgAANNbdN0AAAABABAAv23xAUNoPAAFwHIAAhIpAAIAO01hY2ludG9zaCBIRDpVc2VyczoAanNpZWs6AEdvb2dsZSBEcml2ZToAYmliOgBpdHAxM2xpbmsucGRmAAAOABwADQBpAHQAcAAxADMAbABpAG4AawAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAKlVzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvaXRwMTNsaW5rLnBkZgATAAEvAAAVAAIADP//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAJwAoQCpAjMCNQI6AkUCTgJcAmACZwJwAnUCggKFApcCmgKfAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAAqE=},
+	Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-642-39634-2_28}}
+
+@inproceedings{Thery:1992aa,
+	Acmid = {143760},
+	Address = {New York, NY, USA},
+	Annote = {related to graspable logic},
+	Author = {Th{\'e}ry, Laurent and Bertot, Yves and Kahn, Gilles},
+	Booktitle = {Proceedings of the Fifth ACM SIGSOFT Symposium on Software Development Environments},
+	Date-Added = {2016-05-13 12:07:02 +0000},
+	Date-Modified = {2016-05-13 12:11:56 +0000},
+	Doi = {10.1145/142868.143760},
+	Isbn = {0-89791-554-2},
+	Location = {Tyson's Corner, Virginia, USA},
+	Numpages = {10},
+	Pages = {120--129},
+	Publisher = {ACM},
+	Series = {SDE 5},
+	Title = {Real Theorem Provers Deserve Real User-interfaces},
+	Url = {http://doi.acm.org/10.1145/142868.143760},
+	Year = {1992},
+	Bdsk-Url-1 = {http://doi.acm.org/10.1145/142868.143760},
+	Bdsk-Url-2 = {http://dx.doi.org/10.1145/142868.143760}}
+
+@inbook{Bertot:1994aa,
+	Address = {Berlin, Heidelberg},
+	Annote = {related to graspable logic},
+	Author = {Bertot, Yves and Kahn, Gilles and Th{\'e}ry, Laurent},
+	Chapter = {Proof by pointing},
+	Date-Added = {2016-05-13 12:02:49 +0000},
+	Date-Modified = {2016-05-13 12:05:32 +0000},
+	Doi = {10.1007/3-540-57887-0_94},
+	Editor = {Hagiya, Masami and Mitchell, John C.},
+	Isbn = {978-3-540-48383-0},
+	Pages = {141--160},
+	Publisher = {Springer Berlin Heidelberg},
+	Title = {Theoretical Aspects of Computer Software: International Symposium TACS '94 Sendai, Japan, April 19--22, 1994 Proceedings},
+	Url = {http://dx.doi.org/10.1007/3-540-57887-0_94},
+	Year = {1994},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QFXByb29mLWJ5LXBvaW50aW5nLnBkZtIXCxgZV05TLmRhdGFPEQGmAAAAAAGmAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEVcHJvb2YtYnktcG9pbnRpbmcucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAXsQadNbOsVQREYgAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADTW3MFAAAAAQAQAL9t8QFDaDwABcByAAISKQACAENNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAcHJvb2YtYnktcG9pbnRpbmcucGRmAAAOACwAFQBwAHIAbwBvAGYALQBiAHkALQBwAG8AaQBuAHQAaQBuAGcALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASADJVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL3Byb29mLWJ5LXBvaW50aW5nLnBkZgATAAEvAAAVAAIADP//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAKYAqwCzAl0CXwJkAm8CeAKGAooCkQKaAp8CrAKvAsECxALJAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAAss=},
+	Bdsk-Url-1 = {http://dx.doi.org/10.1007/3-540-57887-0_94}}
+
+@phdthesis{Bohm:1954aa,
+	Author = {Corrado B{\"o}hm},
+	Date-Added = {2016-05-05 02:00:53 +0000},
+	Date-Modified = {2016-05-05 02:02:20 +0000},
+	School = {ETH Zurich},
+	Title = {Digital Computers: On encoding logical-mathematical formulas using the machine itself during program conception},
+	Year = {1954},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YVlib2VobS5wZGbSFwsYGVdOUy5kYXRhTxEBdgAAAAABdgACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xCWJvZWhtLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAFjq3fTUCH2UERGIAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA01BaNgAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgA3TWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6AGJvZWhtLnBkZgAADgAUAAkAYgBvAGUAaABtAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAmVXNlcnMvanNpZWsvR29vZ2xlIERyaXZlL2JpYi9ib2VobS5wZGYAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCYAJ0ApQIfAiECJgIxAjoCSAJMAlMCXAJhAm4CcQKDAoYCiwAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAKN}}
+
+@inbook{Bonnaire-Sergeant2016,
+	Address = {Berlin, Heidelberg},
+	Author = {Bonnaire-Sergeant, Ambrose and Davies, Rowan and Tobin-Hochstadt, Sam},
+	Chapter = {Practical Optional Types for Clojure},
+	Date-Added = {2016-05-03 14:41:23 +0000},
+	Date-Modified = {2016-05-03 14:41:23 +0000},
+	Doi = {10.1007/978-3-662-49498-1_4},
+	Editor = {Thiemann, Peter},
+	Isbn = {978-3-662-49498-1},
+	Pages = {68--94},
+	Publisher = {Springer Berlin Heidelberg},
+	Title = {Programming Languages and Systems: 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings},
+	Url = {http://dx.doi.org/10.1007/978-3-662-49498-1_4},
+	Year = {2016},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QFHByYWMtb3B0LWNsb2p1cmUucGRm0hcLGBlXTlMuZGF0YU8RAaIAAAAAAaIAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAM3IwOpIKwAAAL9t8RRwcmFjLW9wdC1jbG9qdXJlLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABYyQD004w9FBERiAAAAAAAAEAAgAACSAAAAAAAAAAAAAAAAAAAAADYmliAAAQAAgAAM3I+SoAAAARAAgAANNOaTQAAAABABAAv23xAUNoPAAFwHIAAhIpAAIAQk1hY2ludG9zaCBIRDpVc2VyczoAanNpZWs6AEdvb2dsZSBEcml2ZToAYmliOgBwcmFjLW9wdC1jbG9qdXJlLnBkZgAOACoAFABwAHIAYQBjAC0AbwBwAHQALQBjAGwAbwBqAHUAcgBlAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAxVXNlcnMvanNpZWsvR29vZ2xlIERyaXZlL2JpYi9wcmFjLW9wdC1jbG9qdXJlLnBkZgAAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgClAKoAsgJYAloCXwJqAnMCgQKFAowClQKaAqcCqgK8Ar8CxAAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAALG},
+	Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-662-49498-1_4}}
+
+@electronic{Verlaguet:aa,
+	Author = {Julien Verlaguet and Alok Menghrajani},
+	Date-Added = {2016-05-03 14:29:44 +0000},
+	Date-Modified = {2016-05-03 14:30:57 +0000},
+	Title = {Hack: a new programming langauge for {HHVM}},
+	Url = {https://code.facebook.com/posts/264544830379293/hack-a-new-programming-language-for-hhvm/},
+	Urldate = {March 20, 2014},
+	Bdsk-Url-1 = {https://code.facebook.com/posts/264544830379293/hack-a-new-programming-language-for-hhvm/}}
+
+@inbook{Hoare:1997aa,
+	Address = {Berlin, Heidelberg},
+	Author = {Hoare, C. A. R.},
+	Chapter = {Unified Theories of Programming},
+	Date-Added = {2016-05-03 14:16:26 +0000},
+	Date-Modified = {2016-05-03 14:16:44 +0000},
+	Doi = {10.1007/978-3-642-60858-2_21},
+	Editor = {Broy, Manfred and Schieder, Birgit},
+	Isbn = {978-3-642-60858-2},
+	Pages = {313--367},
+	Publisher = {Springer Berlin Heidelberg},
+	Title = {Mathematical Methods in Program Development},
+	Url = {http://dx.doi.org/10.1007/978-3-642-60858-2_21},
+	Year = {1997},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QFHVuaWZpZWRfdGhlb3JpZXMucGRm0hcLGBlXTlMuZGF0YU8RAaIAAAAAAaIAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAM3IwOpIKwAAAL9t8RR1bmlmaWVkX3RoZW9yaWVzLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABYxvY004rFVBERiAAAAAAAAEAAgAACSAAAAAAAAAAAAAAAAAAAAADYmliAAAQAAgAAM3I+SoAAAARAAgAANNOY1UAAAABABAAv23xAUNoPAAFwHIAAhIpAAIAQk1hY2ludG9zaCBIRDpVc2VyczoAanNpZWs6AEdvb2dsZSBEcml2ZToAYmliOgB1bmlmaWVkX3RoZW9yaWVzLnBkZgAOACoAFAB1AG4AaQBmAGkAZQBkAF8AdABoAGUAbwByAGkAZQBzAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAxVXNlcnMvanNpZWsvR29vZ2xlIERyaXZlL2JpYi91bmlmaWVkX3RoZW9yaWVzLnBkZgAAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgClAKoAsgJYAloCXwJqAnMCgQKFAowClQKaAqcCqgK8Ar8CxAAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAALG},
+	Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-642-60858-2_21}}
+
+@inproceedings{Steele:1977aa,
+	Acmid = {810196},
+	Address = {New York, NY, USA},
+	Author = {Steele,Jr., Guy Lewis},
+	Booktitle = {Proceedings of the 1977 Annual Conference},
+	Date-Added = {2016-05-02 20:39:13 +0000},
+	Date-Modified = {2016-05-02 20:39:16 +0000},
+	Doi = {10.1145/800179.810196},
+	Isbn = {978-1-4503-3921-6},
+	Location = {Seattle, Washington},
+	Numpages = {10},
+	Pages = {153--162},
+	Publisher = {ACM},
+	Series = {ACM '77},
+	Title = {Debunking the \&Ldquo;Expensive Procedure Call\&Rdquo; Myth or, Procedure Call Implementations Considered Harmful or, LAMBDA: The Ultimate GOTO},
+	Url = {http://doi.acm.org/10.1145/800179.810196},
+	Year = {1977},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QD3AxNTMtc3RlZWxlLnBkZtIXCxgZV05TLmRhdGFPEQGOAAAAAAGOAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEPcDE1My1zdGVlbGUucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAWMTa9NNM0VQREYgAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADTTWuFAAAAAQAQAL9t8QFDaDwABcByAAISKQACAD1NYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAcDE1My1zdGVlbGUucGRmAAAOACAADwBwADEANQAzAC0AcwB0AGUAZQBsAGUALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASACxVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL3AxNTMtc3RlZWxlLnBkZgATAAEvAAAVAAIADP//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAKAApQCtAj8CQQJGAlECWgJoAmwCcwJ8AoECjgKRAqMCpgKrAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAAq0=},
+	Bdsk-Url-1 = {http://doi.acm.org/10.1145/800179.810196},
+	Bdsk-Url-2 = {http://dx.doi.org/10.1145/800179.810196}}
+
+@inproceedings{Pitts:1998ab,
+	Author = {Andrew M. Pitts},
+	Bibsource = {dblp computer science bibliography, http://dblp.org},
+	Biburl = {http://dblp.uni-trier.de/rec/bib/conf/icalp/Pitts98},
+	Booktitle = {Automata, Languages and Programming, 25th International Colloquium, ICALP'98, Aalborg, Denmark, July 13-17, 1998, Proceedings},
+	Date-Added = {2016-05-02 18:44:21 +0000},
+	Date-Modified = {2016-05-02 18:44:34 +0000},
+	Doi = {10.1007/BFb0055063},
+	Pages = {309--326},
+	Timestamp = {Thu, 16 Jun 2011 15:52:43 +0200},
+	Title = {Existential Types: Logical Relations and Operational Equivalence},
+	Url = {http://dx.doi.org/10.1007/BFb0055063},
+	Year = {1998},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QEWV4aXN0LWxvZy1yZWwucGRm0hcLGBlXTlMuZGF0YU8RAZYAAAAAAZYAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAM3IwOpIKwAAAL9t8RFleGlzdC1sb2ctcmVsLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABYwNo000YmVBERiAAAAAAAAEAAgAACSAAAAAAAAAAAAAAAAAAAAADYmliAAAQAAgAAM3I+SoAAAARAAgAANNNUNkAAAABABAAv23xAUNoPAAFwHIAAhIpAAIAP01hY2ludG9zaCBIRDpVc2VyczoAanNpZWs6AEdvb2dsZSBEcml2ZToAYmliOgBleGlzdC1sb2ctcmVsLnBkZgAADgAkABEAZQB4AGkAcwB0AC0AbABvAGcALQByAGUAbAAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIALlVzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvZXhpc3QtbG9nLXJlbC5wZGYAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCiAKcArwJJAksCUAJbAmQCcgJ2An0ChgKLApgCmwKtArACtQAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAK3},
+	Bdsk-Url-1 = {http://dx.doi.org/10.1007/BFb0055063}}
+
+@inproceedings{Hieb:1990aa,
+	Acmid = {93554},
+	Address = {New York, NY, USA},
+	Author = {Hieb, R. and Dybvig, R. Kent and Bruggeman, Carl},
+	Booktitle = {Proceedings of the ACM SIGPLAN 1990 Conference on Programming Language Design and Implementation},
+	Date-Added = {2016-05-02 18:41:58 +0000},
+	Date-Modified = {2016-05-02 18:42:00 +0000},
+	Doi = {10.1145/93542.93554},
+	Isbn = {0-89791-364-7},
+	Location = {White Plains, New York, USA},
+	Numpages = {12},
+	Pages = {66--77},
+	Publisher = {ACM},
+	Series = {PLDI '90},
+	Title = {Representing Control in the Presence of First-class Continuations},
+	Url = {http://doi.acm.org/10.1145/93542.93554},
+	Year = {1990},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YVxwNjYtaGllYi5wZGbSFwsYGVdOUy5kYXRhTxEBggAAAAABggACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xDHA2Ni1oaWViLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAFjAlnTTRfLUERGIAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA001QCwAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgA6TWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6AHA2Ni1oaWViLnBkZgAOABoADABwADYANgAtAGgAaQBlAGIALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAClVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL3A2Ni1oaWViLnBkZgAAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCbAKAAqAIuAjACNQJAAkkCVwJbAmICawJwAn0CgAKSApUCmgAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAKc},
+	Bdsk-Url-1 = {http://doi.acm.org/10.1145/93542.93554},
+	Bdsk-Url-2 = {http://dx.doi.org/10.1145/93542.93554}}
+
+@techreport{Milner:1971aa,
+	Address = {Stanford, CA, USA},
+	Author = {Milner, Robin},
+	Date-Added = {2016-04-26 03:08:19 +0000},
+	Date-Modified = {2016-04-26 03:08:23 +0000},
+	Publisher = {Stanford University},
+	Source = {http://www.ncstrl.org:8900/ncstrl/servlet/search?formname=detail\&id=oai%3Ancstrlh%3Astan%3ASTAN%2F%2FCS-TR-71-205},
+	Title = {An Algebraic Definition of Simulation Between Programs},
+	Year = {1971},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QEENTLVRSLTcxLTIwNS5wZGbSFwsYGVdOUy5kYXRhTxEBkgAAAAABkgACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xEENTLVRSLTcxLTIwNS5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAFhqu3TRFP4UERGIAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA00SMOAAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgA+TWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6AENTLVRSLTcxLTIwNS5wZGYADgAiABAAQwBTAC0AVABSAC0ANwAxAC0AMgAwADUALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAC1Vc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL0NTLVRSLTcxLTIwNS5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AoQCmAK4CRAJGAksCVgJfAm0CcQJ4AoEChgKTApYCqAKrArAAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAACsg==}}
+
+@incollection{Jacobs:2011aa,
+	Author = {Bart Jacobs and Jan Rutten},
+	Booktitle = {Advanced Topics in Bisimulation and Coinduction},
+	Date-Added = {2016-04-26 03:07:14 +0000},
+	Date-Modified = {2016-04-26 03:07:19 +0000},
+	Editor = {Davide Sangiorgi and Jan Rutten},
+	Isbn = {9780511792588},
+	Note = {Cambridge Books Online},
+	Pages = {38--99},
+	Publisher = {Cambridge University Press},
+	Title = {An introduction to (co)algebra and (co)induction},
+	Url = {http://dx.doi.org/10.1017/CBO9780511792588.003},
+	Year = {2011},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QGjIwMTFfSmFjb2JzX1J1dHRlbl9uZXcucGRm0hcLGBlXTlMuZGF0YU8RAboAAAAAAboAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAM3IwOpIKwAAAL9t8RoyMDExX0phY29ic19SdXR0ZW5fbmV3LnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABYap800RTs1BERiAAAAAAAAEAAgAACSAAAAAAAAAAAAAAAAAAAAADYmliAAAQAAgAAM3I+SoAAAARAAgAANNEi/MAAAABABAAv23xAUNoPAAFwHIAAhIpAAIASE1hY2ludG9zaCBIRDpVc2VyczoAanNpZWs6AEdvb2dsZSBEcml2ZToAYmliOgAyMDExX0phY29ic19SdXR0ZW5fbmV3LnBkZgAOADYAGgAyADAAMQAxAF8ASgBhAGMAbwBiAHMAXwBSAHUAdAB0AGUAbgBfAG4AZQB3AC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgA3VXNlcnMvanNpZWsvR29vZ2xlIERyaXZlL2JpYi8yMDExX0phY29ic19SdXR0ZW5fbmV3LnBkZgAAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCrALAAuAJ2AngCfQKIApECnwKjAqoCswK4AsUCyALaAt0C4gAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAALk},
+	Bdsk-Url-1 = {http://dx.doi.org/10.1017/CBO9780511792588.003}}
+
+@article{Jacobs:1997aa,
+	Author = {Bart Jacobs and Jan Rutten},
+	Date-Added = {2016-04-26 03:04:26 +0000},
+	Date-Modified = {2016-04-26 03:11:29 +0000},
+	Journal = {EATCS Bulletin},
+	Pages = {222--259},
+	Title = {A Tutorial on (Co)Algebras and (Co)Induction},
+	Volume = {62},
+	Year = {1997},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YVZKUi5wZGbSFwsYGVdOUy5kYXRhTxEBagAAAAABagACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xBkpSLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAFhq6zTRFSsUERGIAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA00SM7AAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgA0TWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6AEpSLnBkZgAOAA4ABgBKAFIALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASACNVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL0pSLnBkZgAAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCVAJoAogIQAhICFwIiAisCOQI9AkQCTQJSAl8CYgJ0AncCfAAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAJ+}}
+
+@inbook{Park:1981aa,
+	Address = {Berlin, Heidelberg},
+	Author = {Park, David},
+	Chapter = {Concurrency and automata on infinite sequences},
+	Date-Added = {2016-04-26 02:13:06 +0000},
+	Date-Modified = {2016-04-26 02:13:09 +0000},
+	Doi = {10.1007/BFb0017309},
+	Editor = {Deussen, Peter},
+	Isbn = {978-3-540-38561-5},
+	Pages = {167--183},
+	Publisher = {Springer Berlin Heidelberg},
+	Title = {Theoretical Computer Science: 5th GI-Conference Karlsruhe, March 23--25, 1981},
+	Url = {http://dx.doi.org/10.1007/BFb0017309},
+	Year = {1981},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YVxwYXJrMTk4MS5wZGbSFwsYGVdOUy5kYXRhTxEBggAAAAABggACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xDHBhcmsxOTgxLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAFhpYrTREcJUERGIAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA00R/SQAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgA6TWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6AHBhcmsxOTgxLnBkZgAOABoADABwAGEAcgBrADEAOQA4ADEALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAClVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL3BhcmsxOTgxLnBkZgAAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCbAKAAqAIuAjACNQJAAkkCVwJbAmICawJwAn0CgAKSApUCmgAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAKc},
+	Bdsk-Url-1 = {http://dx.doi.org/10.1007/BFb0017309}}
+
+@article{Lassen1999346,
+	Author = {S.B. Lassen},
+	Date-Added = {2016-04-25 13:52:28 +0000},
+	Date-Modified = {2016-04-25 13:52:28 +0000},
+	Doi = {http://dx.doi.org/10.1016/S1571-0661(04)80083-5},
+	Issn = {1571-0661},
+	Journal = {Electronic Notes in Theoretical Computer Science},
+	Note = {\{MFPS\} XV, Mathematical Foundations of Progamming Semantics, Fifteenth Conference},
+	Pages = {346 - 374},
+	Title = {Bisimulation in Untyped Lambda Calculus:: B{\"o}hm Trees and Bisimulation up to Context},
+	Url = {http://www.sciencedirect.com/science/article/pii/S1571066104800835},
+	Volume = {20},
+	Year = {1999},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QGGJpc2ltLXVudHlwZWQtbGFtYmRhLnBkZtIXCxgZV05TLmRhdGFPEQGyAAAAAAGyAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEYYmlzaW0tdW50eXBlZC1sYW1iZGEucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAWFrntNDmXNQREYgAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADTQ9GzAAAAAQAQAL9t8QFDaDwABcByAAISKQACAEZNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAYmlzaW0tdW50eXBlZC1sYW1iZGEucGRmAA4AMgAYAGIAaQBzAGkAbQAtAHUAbgB0AHkAcABlAGQALQBsAGEAbQBiAGQAYQAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIANVVzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvYmlzaW0tdW50eXBlZC1sYW1iZGEucGRmAAATAAEvAAAVAAIADP//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAKkArgC2AmwCbgJzAn4ChwKVApkCoAKpAq4CuwK+AtAC0wLYAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAAto=},
+	Bdsk-Url-1 = {http://www.sciencedirect.com/science/article/pii/S1571066104800835},
+	Bdsk-Url-2 = {http://dx.doi.org/10.1016/S1571-0661(04)80083-5}}
+
+@article{Gordon:1995aa,
+	Author = {Andrew D. Gordon},
+	Date-Added = {2016-04-23 18:38:58 +0000},
+	Date-Modified = {2016-04-23 18:39:02 +0000},
+	Doi = {http://dx.doi.org/10.1016/S1571-0661(04)80013-6},
+	Issn = {1571-0661},
+	Journal = {Electronic Notes in Theoretical Computer Science},
+	Note = {\{MFPS\} XI, Mathematical Foundations of Programming Semantics, Eleventh Annual Conference},
+	Pages = {232 - 252},
+	Title = {Bisimilarity as a Theory of Functional Programming},
+	Url = {http://www.sciencedirect.com/science/article/pii/S1571066104800136},
+	Volume = {1},
+	Year = {1995},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QFGJpc2ltLXRoZW9yeS1mdW4ucGRm0hcLGBlXTlMuZGF0YU8RAaIAAAAAAaIAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAM3IwOpIKwAAAL9t8RRiaXNpbS10aGVvcnktZnVuLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABYUCS00E5vFBERiAAAAAAAAEAAgAACSAAAAAAAAAAAAAAAAAAAAADYmliAAAQAAgAAM3I+SoAAAARAAgAANNBcfwAAAABABAAv23xAUNoPAAFwHIAAhIpAAIAQk1hY2ludG9zaCBIRDpVc2VyczoAanNpZWs6AEdvb2dsZSBEcml2ZToAYmliOgBiaXNpbS10aGVvcnktZnVuLnBkZgAOACoAFABiAGkAcwBpAG0ALQB0AGgAZQBvAHIAeQAtAGYAdQBuAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAxVXNlcnMvanNpZWsvR29vZ2xlIERyaXZlL2JpYi9iaXNpbS10aGVvcnktZnVuLnBkZgAAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgClAKoAsgJYAloCXwJqAnMCgQKFAowClQKaAqcCqgK8Ar8CxAAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAALG},
+	Bdsk-Url-1 = {http://www.sciencedirect.com/science/article/pii/S1571066104800136},
+	Bdsk-Url-2 = {http://dx.doi.org/10.1016/S1571-0661(04)80013-6}}
+
+@incollection{Walker:2005aa,
+	Author = {David Walker},
+	Booktitle = {Advanced Topics in Types and Programming Languages},
+	Chapter = 1,
+	Date-Added = {2016-04-21 20:31:05 +0000},
+	Date-Modified = {2016-04-21 20:31:10 +0000},
+	Editor = {Benjamin C. Pierce},
+	Publisher = {MIT Press},
+	Title = {{Substructural Type Systems}},
+	Year = {2005}}
+
+@techreport{Greenberg:2016aa,
+	Author = {Michael Greenberg},
+	Date-Added = {2016-04-17 10:52:03 +0000},
+	Date-Modified = {2016-04-17 10:53:46 +0000},
+	Institution = {Pomona College},
+	Number = {http://arxiv.org/abs/1604.02474},
+	Title = {Space-Efficient Latent Contracts},
+	Year = {2016},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV4xNjA0LjAyNDc0LnBkZtIXCxgZV05TLmRhdGFPEQGKAAAAAAGKAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEOMTYwNC4wMjQ3NC5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAWA8UdM444dQREYgAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADTORvHAAAAAQAQAL9t8QFDaDwABcByAAISKQACADxNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAMTYwNC4wMjQ3NC5wZGYADgAeAA4AMQA2ADAANAAuADAAMgA0ADcANAAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAK1VzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvMTYwNC4wMjQ3NC5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AnQCiAKoCOAI6Aj8CSgJTAmECZQJsAnUCegKHAooCnAKfAqQAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAACpg==}}
+
+@article{Jones:1983aa,
+	Acmid = {69577},
+	Address = {New York, NY, USA},
+	Author = {Jones, C. B.},
+	Date-Added = {2016-04-14 14:10:04 +0000},
+	Date-Modified = {2016-04-14 14:10:10 +0000},
+	Doi = {10.1145/69575.69577},
+	Issn = {0164-0925},
+	Issue_Date = {Oct. 1983},
+	Journal = {ACM Trans. Program. Lang. Syst.},
+	Month = oct,
+	Number = {4},
+	Numpages = {24},
+	Pages = {596--619},
+	Publisher = {ACM},
+	Title = {Tentative Steps Toward a Development Method for Interfering Programs},
+	Url = {http://doi.acm.org/10.1145/69575.69577},
+	Volume = {5},
+	Year = {1983},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV5wNTk2LWpvbmVzLnBkZtIXCxgZV05TLmRhdGFPEQGKAAAAAAGKAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEOcDU5Ni1qb25lcy5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAV/rHdM1HSdQREYgAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADTNVVnAAAAAQAQAL9t8QFDaDwABcByAAISKQACADxNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAcDU5Ni1qb25lcy5wZGYADgAeAA4AcAA1ADkANgAtAGoAbwBuAGUAcwAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAK1VzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvcDU5Ni1qb25lcy5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AnQCiAKoCOAI6Aj8CSgJTAmECZQJsAnUCegKHAooCnAKfAqQAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAACpg==},
+	Bdsk-Url-1 = {http://doi.acm.org/10.1145/69575.69577},
+	Bdsk-Url-2 = {http://dx.doi.org/10.1145/69575.69577}}
+
+@inbook{Thiemann:2016aa,
+	Address = {Cham},
+	Author = {Thiemann, Peter},
+	Chapter = {A Delta for Hybrid Type Checking},
+	Date-Added = {2016-04-09 21:11:27 +0000},
+	Date-Modified = {2016-04-09 21:11:31 +0000},
+	Doi = {10.1007/978-3-319-30936-1_22},
+	Editor = {Lindley, Sam and McBride, Conor and Trinder, Phil and Sannella, Don},
+	Isbn = {978-3-319-30936-1},
+	Pages = {411--432},
+	Publisher = {Springer International Publishing},
+	Title = {A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday},
+	Url = {http://dx.doi.org/10.1007/978-3-319-30936-1_22},
+	Year = {2016},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QEGRlbHRhLWh5YnJpZC5wZGbSFwsYGVdOUy5kYXRhTxEBkgAAAAABkgACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xEGRlbHRhLWh5YnJpZC5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAFe4kjTLumEUERGIAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA0y8hxAAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgA+TWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6AGRlbHRhLWh5YnJpZC5wZGYADgAiABAAZABlAGwAdABhAC0AaAB5AGIAcgBpAGQALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAC1Vc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL2RlbHRhLWh5YnJpZC5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AoQCmAK4CRAJGAksCVgJfAm0CcQJ4AoEChgKTApYCqAKrArAAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAACsg==},
+	Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-319-30936-1_22}}
+
+@inproceedings{Garcia:2016aa,
+	Acmid = {2837670},
+	Address = {New York, NY, USA},
+	Author = {Garcia, Ronald and Clark, Alison M. and Tanter, \'{E}ric},
+	Booktitle = {Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+	Date-Added = {2016-04-08 23:24:54 +0000},
+	Date-Modified = {2016-04-08 23:25:00 +0000},
+	Doi = {10.1145/2837614.2837670},
+	Isbn = {978-1-4503-3549-2},
+	Keywords = {abstract interpretation, gradual typing, subtyping},
+	Location = {St. Petersburg, FL, USA},
+	Numpages = {14},
+	Pages = {429--442},
+	Publisher = {ACM},
+	Series = {POPL 2016},
+	Title = {Abstracting Gradual Typing},
+	Url = {http://doi.acm.org/10.1145/2837614.2837670},
+	Year = {2016},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QD3A0MjktZ2FyY2lhLnBkZtIXCxgZV05TLmRhdGFPEQGOAAAAAAGOAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEPcDQyOS1nYXJjaWEucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAV6dOdMttlZQREYgAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADTLe6WAAAAAQAQAL9t8QFDaDwABcByAAISKQACAD1NYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAcDQyOS1nYXJjaWEucGRmAAAOACAADwBwADQAMgA5AC0AZwBhAHIAYwBpAGEALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASACxVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL3A0MjktZ2FyY2lhLnBkZgATAAEvAAAVAAIADP//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAKAApQCtAj8CQQJGAlECWgJoAmwCcwJ8AoECjgKRAqMCpgKrAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAAq0=},
+	Bdsk-Url-1 = {http://doi.acm.org/10.1145/2837614.2837670},
+	Bdsk-Url-2 = {http://dx.doi.org/10.1145/2837614.2837670}}
+
 @inproceedings{Cardelli:1984aa,
 	Acmid = {802037},
 	Address = {New York, NY, USA},
@@ -63,7 +581,7 @@
 	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},
+	Date-Modified = {2016-03-30 02:07:40 +0000},
 	Doi = {10.1145/2676726.2676971},
 	Isbn = {978-1-4503-3300-9},
 	Keywords = {gradual typing, javascript, type safety, typescript},
@@ -72,7 +590,7 @@
 	Pages = {167--180},
 	Publisher = {ACM},
 	Series = {POPL '15},
-	Title = {Safe \&\#38; Efficient Gradual Typing for TypeScript},
+	Title = {Safe \& Efficient Gradual Typing for TypeScript},
 	Url = {http://doi.acm.org/10.1145/2676726.2676971},
 	Year = {2015},
 	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QEHAxNjctcmFzdG9naS5wZGbSFwsYGVdOUy5kYXRhTxEBkgAAAAABkgACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xEHAxNjctcmFzdG9naS5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAFakc3TFa9fUERGIAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA0xXnnwAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgA+TWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6AHAxNjctcmFzdG9naS5wZGYADgAiABAAcAAxADYANwAtAHIAYQBzAHQAbwBnAGkALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAC1Vc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL3AxNjctcmFzdG9naS5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AoQCmAK4CRAJGAksCVgJfAm0CcQJ4AoEChgKTApYCqAKrArAAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAACsg==},
@@ -2741,10 +3259,10 @@
 	Year = {2015},
 	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YVtwYXBlcjExLnBkZtIXCxgZV05TLmRhdGFPEQF+AAAAAAF+AAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfELcGFwZXIxMS5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAOuUvtHNKz9QREYgAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADRzWN/AAAAAQAQAL9t8QFDaDwABcByAAISKQACADlNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAcGFwZXIxMS5wZGYAAA4AGAALAHAAYQBwAGUAcgAxADEALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAChVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL3BhcGVyMTEucGRmABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AmgCfAKcCKQIrAjACOwJEAlICVgJdAmYCawJ4AnsCjQKQApUAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAAClw==}}
 
-@techreport{Jr.:1977aa,
-	Author = {Guy L. Steele Jr.},
+@techreport{Steele:1977ab,
+	Author = {Steele, Jr., Guy L. },
 	Date-Added = {2015-07-14 14:37:03 +0000},
-	Date-Modified = {2015-07-14 14:37:45 +0000},
+	Date-Modified = {2016-05-20 16:01:06 +0000},
 	Institution = {MIT Artificial Intelligence Lab},
 	Month = {September},
 	Number = {420},
@@ -7605,9 +8123,9 @@
 	Author = {Nikhil Swamy and Cedric Fournet and Aseem Rastogi and Karthikeyan Bhargavan and Juan Chen and Pierre-Yves Strub and Gavin Bierman},
 	Booktitle = {ACM Conference on Principles of Programming Languages (POPL)},
 	Date-Added = {2013-12-02 19:01:31 +0000},
-	Date-Modified = {2013-12-02 19:02:37 +0000},
+	Date-Modified = {2016-05-03 15:13:06 +0000},
 	Month = {January},
-	Title = {Gradual Typing Embedded Securely in JavaScript},
+	Title = {Gradual Typing Embedded Securely in {JavaScript}},
 	Year = {2014},
 	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YVl0c3Rhci5wZGbSFwsYGVdOUy5kYXRhTxEBdgAAAAABdgACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xCXRzdGFyLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAC/ilrRDzyaUERGIAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA0Q+C6gAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgA3TWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6AHRzdGFyLnBkZgAADgAUAAkAdABzAHQAYQByAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAmVXNlcnMvanNpZWsvR29vZ2xlIERyaXZlL2JpYi90c3Rhci5wZGYAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCYAJ0ApQIfAiECJgIxAjoCSAJMAlMCXAJhAm4CcQKDAoYCiwAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAKN}}
 
@@ -8159,8 +8677,8 @@
 	Author = {Brianna M. Ren and John Toman and T. Stephen Strickland and Jeffrey S. Foster},
 	Booktitle = {SAC'13 (OOPS)},
 	Date-Added = {2012-12-16 10:39:59 -0700},
-	Date-Modified = {2012-12-16 10:41:02 -0700},
-	Title = {The Ruby Type Checker},
+	Date-Modified = {2016-05-03 15:12:45 +0000},
+	Title = {The {Ruby} Type Checker},
 	Year = {2013},
 	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YVxvb3BzMjAxMy5wZGbSFwsYGVdOUy5kYXRhTxEBggAAAAABggACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xDG9vcHMyMDEzLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAC/eVXRDzjrAAAAAAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA0Q9/OwAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgA6TWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6AG9vcHMyMDEzLnBkZgAOABoADABvAG8AcABzADIAMAAxADMALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAClVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL29vcHMyMDEzLnBkZgAAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCbAKAAqAIuAjACNQJAAkkCVwJbAmICawJwAn0CgAKSApUCmgAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAKc}}
 
@@ -13329,8 +13847,7 @@ semantics was validated.},
 	Pages = {280},
 	Publisher = {IEEE Computer Society},
 	Title = {Towards a Mathematical Operational Semantics},
-	Year = {1997},
-	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QHi4uL0Ryb3Bib3gvYmliL01hdGhfT3BfU2VtLnBkZtIXCxgZV05TLmRhdGFPEQGEAAAAAAGEAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAAOauEPTWF0aF9PcF9TZW0ucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA7vl8zlmwkAAAAAAAAAAAABAAMAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADM5eFZAAAAAQAQAA5q4QAOad0ABcByAAISKQACADhNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBEcm9wYm94OgBiaWI6AE1hdGhfT3BfU2VtLnBkZgAOACAADwBNAGEAdABoAF8ATwBwAF8AUwBlAG0ALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASACdVc2Vycy9qc2llay9Ecm9wYm94L2JpYi9NYXRoX09wX1NlbS5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4ArwC0ALwCRAJGAksCVgJfAm0CcQJ4AoEChgKTApYCqAKrArAAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAACsg==}}
+	Year = {1997}}
 
 @article{Sangiorgi:2009kx,
 	Address = {New York, NY, USA},
@@ -13986,8 +14503,7 @@ semantics was validated.},
 	Institution = {BRICS},
 	Number = {NS-95-3},
 	Title = {Bisimilarity as a Theory of Functional Programming},
-	Year = {1995},
-	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QIC4uL0Ryb3Bib3gvYmliL0JSSUNTLU5TLTk1LTMucGRm0hcLGBlXTlMuZGF0YU8RAYwAAAAAAYwAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAM3IwOpIKwAAAA5q4RFCUklDUy1OUy05NS0zLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAADwmkzOWayQAAAAAAAAAAAAEAAwAACSAAAAAAAAAAAAAAAAAAAAADYmliAAAQAAgAAM3I+SoAAAARAAgAAMzl4RkAAAABABAADmrhAA5p3QAFwHIAAhIpAAIAOk1hY2ludG9zaCBIRDpVc2VyczoAanNpZWs6AERyb3Bib3g6AGJpYjoAQlJJQ1MtTlMtOTUtMy5wZGYADgAkABEAQgBSAEkAQwBTAC0ATgBTAC0AOQA1AC0AMwAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAKVVzZXJzL2pzaWVrL0Ryb3Bib3gvYmliL0JSSUNTLU5TLTk1LTMucGRmAAATAAEvAAAVAAIADP//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOALEAtgC+Ak4CUAJVAmACaQJ3AnsCggKLApACnQKgArICtQK6AAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAArw=}}
+	Year = {1995}}
 
 @inproceedings{Aceto:1992ao,
 	Author = {Aceto, L. and Bloom, B. and Vaandrager, F.},
@@ -15138,7 +15654,7 @@ semantics was validated.},
 	Title = {Proving congruence of bisimulation in functional programming languages},
 	Volume = {124},
 	Year = {1996},
-	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QIS4uL0Ryb3Bib3gvYmliLzEwLjEuMS4zNi42NjAxLnBkZtIXCxgZV05TLmRhdGFPEQGQAAAAAAGQAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAAOauESMTAuMS4xLjM2LjY2MDEucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA7t/szlmrAAAAAAAAAAAAABAAMAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADM5eEAAAAAAQAQAA5q4QAOad0ABcByAAISKQACADtNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBEcm9wYm94OgBiaWI6ADEwLjEuMS4zNi42NjAxLnBkZgAADgAmABIAMQAwAC4AMQAuADEALgAzADYALgA2ADYAMAAxAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAqVXNlcnMvanNpZWsvRHJvcGJveC9iaWIvMTAuMS4xLjM2LjY2MDEucGRmABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AsgC3AL8CUwJVAloCZQJuAnwCgAKHApAClQKiAqUCtwK6Ar8AAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAACwQ==},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QD3Byb3ZlLWNvbmdyLnBkZtIXCxgZV05TLmRhdGFPEQGOAAAAAAGOAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEPcHJvdmUtY29uZ3IucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAWFsYtNDmfhQREYgAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADTQ9I4AAAAAQAQAL9t8QFDaDwABcByAAISKQACAD1NYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAcHJvdmUtY29uZ3IucGRmAAAOACAADwBwAHIAbwB2AGUALQBjAG8AbgBnAHIALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASACxVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL3Byb3ZlLWNvbmdyLnBkZgATAAEvAAAVAAIADP//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAKAApQCtAj8CQQJGAlECWgJoAmwCcwJ8AoECjgKRAqMCpgKrAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAAq0=},
 	Bdsk-Url-1 = {http://dx.doi.org/10.1006/inco.1996.0008}}
 
 @inproceedings{Howe:1989ph,
@@ -15151,7 +15667,7 @@ semantics was validated.},
 	Pages = {198-203},
 	Title = {Equality in lazy computation systems},
 	Year = {1989},
-	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QIC4uL0Ryb3Bib3gvYmliL0lFRUVYcGxvcmUoOCkucGRm0hcLGBlXTlMuZGF0YU8RAYwAAAAAAYwAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAM3IwOpIKwAAAA5q4RFJRUVFWHBsb3JlKDgpLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAADwCbzOWa+gAAAAAAAAAAAAEAAwAACSAAAAAAAAAAAAAAAAAAAAADYmliAAAQAAgAAM3I+SoAAAARAAgAAMzl4UoAAAABABAADmrhAA5p3QAFwHIAAhIpAAIAOk1hY2ludG9zaCBIRDpVc2VyczoAanNpZWs6AERyb3Bib3g6AGJpYjoASUVFRVhwbG9yZSg4KS5wZGYADgAkABEASQBFAEUARQBYAHAAbABvAHIAZQAoADgAKQAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAKVVzZXJzL2pzaWVrL0Ryb3Bib3gvYmliL0lFRUVYcGxvcmUoOCkucGRmAAATAAEvAAAVAAIADP//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOALEAtgC+Ak4CUAJVAmACaQJ3AnsCggKLApACnQKgArICtQK6AAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAArw=},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QGUVxdWFsaXR5aW5MYXp5X0xJQ1M4OS5wZGbSFwsYGVdOUy5kYXRhTxEBtgAAAAABtgACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xGUVxdWFsaXR5aW5MYXp5X0xJQ1M4OS5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAFhbOzTQ5o1UERGIAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA00PSdQAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgBHTWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6AEVxdWFsaXR5aW5MYXp5X0xJQ1M4OS5wZGYAAA4ANAAZAEUAcQB1AGEAbABpAHQAeQBpAG4ATABhAHoAeQBfAEwASQBDAFMAOAA5AC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgA2VXNlcnMvanNpZWsvR29vZ2xlIERyaXZlL2JpYi9FcXVhbGl0eWluTGF6eV9MSUNTODkucGRmABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AqgCvALcCcQJzAngCgwKMApoCngKlAq4CswLAAsMC1QLYAt0AAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAAC3w==},
 	Bdsk-Url-1 = {http://dx.doi.org/10.1109/LICS.1989.39174}}
 
 @article{Hoste:2007zl,
@@ -16644,7 +17160,7 @@ semantics was validated.},
 	Title = {The Mechanical Evaluation of Expressions},
 	Volume = {6},
 	Year = {1964},
-	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QFi4uL0Ryb3Bib3gvYmliLzMwOC5wZGbSFwsYGVdOUy5kYXRhTxEBZAAAAAABZAACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAADmrhBzMwOC5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAPI8vM5Zq3AAAAAAAAAAAAAQADAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAAzOXhBwAAAAEAEAAOauEADmndAAXAcgACEikAAgAwTWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoARHJvcGJveDoAYmliOgAzMDgucGRmAA4AEAAHADMAMAA4AC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAfVXNlcnMvanNpZWsvRHJvcGJveC9iaWIvMzA4LnBkZgAAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCnAKwAtAIcAh4CIwIuAjcCRQJJAlACWQJeAmsCbgKAAoMCiAAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAKK}}
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YVxMYW5kaW42NC5wZGbSFwsYGVdOUy5kYXRhTxEBggAAAAABggACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAAv23xDExhbmRpbjY0LnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAFhtZ/TRO84UERGIAAAAAAAAQACAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAA00UneAAAAAEAEAC/bfEBQ2g8AAXAcgACEikAAgA6TWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoAR29vZ2xlIERyaXZlOgBiaWI6AExhbmRpbjY0LnBkZgAOABoADABMAGEAbgBkAGkAbgA2ADQALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAClVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL0xhbmRpbjY0LnBkZgAAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCbAKAAqAIuAjACNQJAAkkCVwJbAmICawJwAn0CgAKSApUCmgAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAKc}}
 
 @book{Meyer:1997hb,
 	Address = {Upper Saddle River, NJ, USA},
@@ -30609,8 +31125,7 @@ over additional an arbitrary constraint system X.},
 	Publisher = {ACM Press},
 	Title = {Tridirectional typechecking},
 	Year = {2004},
-	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QIS4uLy4uLy4uL3BhcGVycy9wMjgxLWR1bmZpZWxkLnBkZtIXCxgZV05TLmRhdGFPEQF6AAAAAAF6AAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADBD6WHSCsAAABPmRERcDI4MS1kdW5maWVsZC5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA8necEJ6RwAAAAAAAAAAAADAAIAAAkgAAAAAAAAAAAAAAAAAAAABnBhcGVycwAQAAgAAMEP+ecAAAARAAgAAMEKPXwAAAABAAwAT5kRAE6kUwBGyTYAAgAwTWFjaW50b3NoIEhEOlVzZXJzOnNpZWs6cGFwZXJzOnAyODEtZHVuZmllbGQucGRmAA4AJAARAHAAMgA4ADEALQBkAHUAbgBmAGkAZQBsAGQALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASACNVc2Vycy9zaWVrL3BhcGVycy9wMjgxLWR1bmZpZWxkLnBkZgAAEwABLwAAFQACAAv//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCyALcAvwI9Aj8CRAJPAlgCZgJqAnECegJ/AowCjwKhAqQCqQAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAKr},
-	Bdsk-File-2 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QEXAyODEtZHVuZmllbGQucGRm0hcLGBlXTlMuZGF0YU8RAZYAAAAAAZYAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAM3IwOpIKwAAAL9t8RFwMjgxLWR1bmZpZWxkLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAv3qL0Q848QAAAAAAAAAAAAEAAgAACSAAAAAAAAAAAAAAAAAAAAADYmliAAAQAAgAAM3I+SoAAAARAAgAANEPf0EAAAABABAAv23xAUNoPAAFwHIAAhIpAAIAP01hY2ludG9zaCBIRDpVc2VyczoAanNpZWs6AEdvb2dsZSBEcml2ZToAYmliOgBwMjgxLWR1bmZpZWxkLnBkZgAADgAkABEAcAAyADgAMQAtAGQAdQBuAGYAaQBlAGwAZAAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIALlVzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvcDI4MS1kdW5maWVsZC5wZGYAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCiAKcArwJJAksCUAJbAmQCcgJ2An0ChgKLApgCmwKtArACtQAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAK3},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QEXAyODEtZHVuZmllbGQucGRm0hcLGBlXTlMuZGF0YU8RAZYAAAAAAZYAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAM3IwOpIKwAAAL9t8RFwMjgxLWR1bmZpZWxkLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAv3qL0Q848QAAAAAAAAAAAAEAAgAACSAAAAAAAAAAAAAAAAAAAAADYmliAAAQAAgAAM3I+SoAAAARAAgAANEPf0EAAAABABAAv23xAUNoPAAFwHIAAhIpAAIAP01hY2ludG9zaCBIRDpVc2VyczoAanNpZWs6AEdvb2dsZSBEcml2ZToAYmliOgBwMjgxLWR1bmZpZWxkLnBkZgAADgAkABEAcAAyADgAMQAtAGQAdQBuAGYAaQBlAGwAZAAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIALlVzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvcDI4MS1kdW5maWVsZC5wZGYAEwABLwAAFQACAAz//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCiAKcArwJJAksCUAJbAmQCcgJ2An0ChgKLApgCmwKtArACtQAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAK3},
 	Bdsk-Url-1 = {http://doi.acm.org/10.1145/964001.964025}}
 
 @inproceedings{Chlipala:2005da,
@@ -30721,8 +31236,7 @@ over additional an arbitrary constraint system X.},
 	Publisher = {ACM Press},
 	Title = {A simple applicative language: {Mini}-{ML}},
 	Year = {1986},
-	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QHy4uLy4uLy4uL3BhcGVycy9wMTMtY2xlbWVudC5wZGbSFwsYGVdOUy5kYXRhTxEBcgAAAAABcgACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAwQ+lh0grAAAAT5kRD3AxMy1jbGVtZW50LnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAPJpLBCekPAAAAAAAAAAAAAwACAAAJIAAAAAAAAAAAAAAAAAAAAAZwYXBlcnMAEAAIAADBD/nnAAAAEQAIAADBCj1vAAAAAQAMAE+ZEQBOpFMARsk2AAIALk1hY2ludG9zaCBIRDpVc2VyczpzaWVrOnBhcGVyczpwMTMtY2xlbWVudC5wZGYADgAgAA8AcAAxADMALQBjAGwAZQBtAGUAbgB0AC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAhVXNlcnMvc2llay9wYXBlcnMvcDEzLWNsZW1lbnQucGRmAAATAAEvAAAVAAIAC///AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOALAAtQC9AjMCNQI6AkUCTgJcAmACZwJwAnUCggKFApcCmgKfAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAAqE=},
-	Bdsk-File-2 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QD3AxMy1jbGVtZW50LnBkZtIXCxgZV05TLmRhdGFPEQGOAAAAAAGOAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEPcDEzLWNsZW1lbnQucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAL95rNEPOO8AAAAAAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADRD38/AAAAAQAQAL9t8QFDaDwABcByAAISKQACAD1NYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAcDEzLWNsZW1lbnQucGRmAAAOACAADwBwADEAMwAtAGMAbABlAG0AZQBuAHQALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASACxVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL3AxMy1jbGVtZW50LnBkZgATAAEvAAAVAAIADP//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAKAApQCtAj8CQQJGAlECWgJoAmwCcwJ8AoECjgKRAqMCpgKrAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAAq0=},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QD3AxMy1jbGVtZW50LnBkZtIXCxgZV05TLmRhdGFPEQGOAAAAAAGOAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEPcDEzLWNsZW1lbnQucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAL95rNEPOO8AAAAAAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADRD38/AAAAAQAQAL9t8QFDaDwABcByAAISKQACAD1NYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAcDEzLWNsZW1lbnQucGRmAAAOACAADwBwADEAMwAtAGMAbABlAG0AZQBuAHQALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASACxVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL3AxMy1jbGVtZW50LnBkZgATAAEvAAAVAAIADP//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAKAApQCtAj8CQQJGAlECWgJoAmwCcwJ8AoECjgKRAqMCpgKrAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAAq0=},
 	Bdsk-Url-1 = {http://doi.acm.org/10.1145/319838.319847}}
 
 @incollection{Reynolds:1969uh,
@@ -31392,8 +31906,7 @@ parametric, as opposed to ad hoc, polymorphism.},
 	Publisher = {Addison-Welsey},
 	Title = {The Lazy Lambda Calculus},
 	Year = {1990},
-	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QIi4uLy4uLy4uL3BhcGVycy9hYnJhbXNreTkwbGF6eS5wZGbSFwsYGVdOUy5kYXRhTxEBfgAAAAABfgACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAwQ+lh0grAAAAT5kREmFicmFtc2t5OTBsYXp5LnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAPJNPBCej7AAAAAAAAAAAAAwACAAAJIAAAAAAAAAAAAAAAAAAAAAZwYXBlcnMAEAAIAADBD/nnAAAAEQAIAADBCj1bAAAAAQAMAE+ZEQBOpFMARsk2AAIAMU1hY2ludG9zaCBIRDpVc2VyczpzaWVrOnBhcGVyczphYnJhbXNreTkwbGF6eS5wZGYAAA4AJgASAGEAYgByAGEAbQBzAGsAeQA5ADAAbABhAHoAeQAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAJFVzZXJzL3NpZWsvcGFwZXJzL2FicmFtc2t5OTBsYXp5LnBkZgATAAEvAAAVAAIAC///AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOALMAuADAAkICRAJJAlQCXQJrAm8CdgJ/AoQCkQKUAqYCqQKuAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAArA=},
-	Bdsk-File-2 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QEmFicmFtc2t5OTBsYXp5LnBkZtIXCxgZV05TLmRhdGFPEQGaAAAAAAGaAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfESYWJyYW1za3k5MGxhenkucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAL9ujdEPNSYAAAAAAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADRD3t2AAAAAQAQAL9t8QFDaDwABcByAAISKQACAEBNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAYWJyYW1za3k5MGxhenkucGRmAA4AJgASAGEAYgByAGEAbQBzAGsAeQA5ADAAbABhAHoAeQAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAL1VzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvYWJyYW1za3k5MGxhenkucGRmAAATAAEvAAAVAAIADP//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAKMAqACwAk4CUAJVAmACaQJ3AnsCggKLApACnQKgArICtQK6AAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAArw=},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QEmFicmFtc2t5OTBsYXp5LnBkZtIXCxgZV05TLmRhdGFPEQGaAAAAAAGaAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfESYWJyYW1za3k5MGxhenkucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAL9ujdEPNSYAAAAAAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADRD3t2AAAAAQAQAL9t8QFDaDwABcByAAISKQACAEBNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAYWJyYW1za3k5MGxhenkucGRmAA4AJgASAGEAYgByAGEAbQBzAGsAeQA5ADAAbABhAHoAeQAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAL1VzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvYWJyYW1za3k5MGxhenkucGRmAAATAAEvAAAVAAIADP//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAKMAqACwAk4CUAJVAmACaQJ3AnsCggKLApACnQKgArICtQK6AAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAArw=},
 	Bdsk-Url-1 = {citeseer.ist.psu.edu/abramsky90lazy.html}}
 
 @inproceedings{Breazu-Tannen:1990vc,
@@ -31438,8 +31951,7 @@ parametric, as opposed to ad hoc, polymorphism.},
 	Publisher = {ACM Press},
 	Title = {Bisimilarity for a first-order calculus of objects with subtyping},
 	Year = {1996},
-	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QHy4uLy4uLy4uL3BhcGVycy9wMzg2LWdvcmRvbi5wZGbSFwsYGVdOUy5kYXRhTxEBcgAAAAABcgACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAwQ+lh0grAAAAT5kRD3AzODYtZ29yZG9uLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAPJ8HBCekhAAAAAAAAAAAAAwACAAAJIAAAAAAAAAAAAAAAAAAAAAZwYXBlcnMAEAAIAADBD/nnAAAAEQAIAADBCj2BAAAAAQAMAE+ZEQBOpFMARsk2AAIALk1hY2ludG9zaCBIRDpVc2VyczpzaWVrOnBhcGVyczpwMzg2LWdvcmRvbi5wZGYADgAgAA8AcAAzADgANgAtAGcAbwByAGQAbwBuAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAhVXNlcnMvc2llay9wYXBlcnMvcDM4Ni1nb3Jkb24ucGRmAAATAAEvAAAVAAIAC///AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOALAAtQC9AjMCNQI6AkUCTgJcAmACZwJwAnUCggKFApcCmgKfAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAAqE=},
-	Bdsk-File-2 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QD3AzODYtZ29yZG9uLnBkZtIXCxgZV05TLmRhdGFPEQGOAAAAAAGOAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEPcDM4Ni1nb3Jkb24ucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAL964dEPOPIAAAAAAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADRD39CAAAAAQAQAL9t8QFDaDwABcByAAISKQACAD1NYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAcDM4Ni1nb3Jkb24ucGRmAAAOACAADwBwADMAOAA2AC0AZwBvAHIAZABvAG4ALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASACxVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL3AzODYtZ29yZG9uLnBkZgATAAEvAAAVAAIADP//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAKAApQCtAj8CQQJGAlECWgJoAmwCcwJ8AoECjgKRAqMCpgKrAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAAq0=},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QD3AzODYtZ29yZG9uLnBkZtIXCxgZV05TLmRhdGFPEQGOAAAAAAGOAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEPcDM4Ni1nb3Jkb24ucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAL964dEPOPIAAAAAAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADRD39CAAAAAQAQAL9t8QFDaDwABcByAAISKQACAD1NYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAcDM4Ni1nb3Jkb24ucGRmAAAOACAADwBwADMAOAA2AC0AZwBvAHIAZABvAG4ALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASACxVc2Vycy9qc2llay9Hb29nbGUgRHJpdmUvYmliL3AzODYtZ29yZG9uLnBkZgATAAEvAAAVAAIADP//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAKAApQCtAj8CQQJGAlECWgJoAmwCcwJ8AoECjgKRAqMCpgKrAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAAq0=},
 	Bdsk-Url-1 = {http://doi.acm.org/10.1145/237721.237807}}
 
 @techreport{Nipkow:2005sa,
@@ -32535,8 +33047,7 @@ software productivity and reliability },
 	Publisher = {ACM Press},
 	Title = {Principal type-schemes for functional programs},
 	Year = {1982},
-	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QHi4uLy4uLy4uL3BhcGVycy9wMjA3LWRhbWFzLnBkZtIXCxgZV05TLmRhdGFPEQFuAAAAAAFuAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADBD6WHSCsAAABPmREOcDIwNy1kYW1hcy5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA8nCsEJ6RYAAAAAAAAAAAADAAIAAAkgAAAAAAAAAAAAAAAAAAAABnBhcGVycwAQAAgAAMEP+ecAAAARAAgAAMEKPXYAAAABAAwAT5kRAE6kUwBGyTYAAgAtTWFjaW50b3NoIEhEOlVzZXJzOnNpZWs6cGFwZXJzOnAyMDctZGFtYXMucGRmAAAOAB4ADgBwADIAMAA3AC0AZABhAG0AYQBzAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAgVXNlcnMvc2llay9wYXBlcnMvcDIwNy1kYW1hcy5wZGYAEwABLwAAFQACAAv//wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgCvALQAvAIuAjACNQJAAkkCVwJbAmICawJwAn0CgAKSApUCmgAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAKc},
-	Bdsk-File-2 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV5wMjA3LWRhbWFzLnBkZtIXCxgZV05TLmRhdGFPEQGKAAAAAAGKAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEOcDIwNy1kYW1hcy5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAL96MdEPOPAAAAAAAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADRD39AAAAAAQAQAL9t8QFDaDwABcByAAISKQACADxNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAcDIwNy1kYW1hcy5wZGYADgAeAA4AcAAyADAANwAtAGQAYQBtAGEAcwAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAK1VzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvcDIwNy1kYW1hcy5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AnQCiAKoCOAI6Aj8CSgJTAmECZQJsAnUCegKHAooCnAKfAqQAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAACpg==},
+	Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV5wMjA3LWRhbWFzLnBkZtIXCxgZV05TLmRhdGFPEQGKAAAAAAGKAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADNyMDqSCsAAAC/bfEOcDIwNy1kYW1hcy5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAL96MdEPOPAAAAAAAAAAAAABAAIAAAkgAAAAAAAAAAAAAAAAAAAAA2JpYgAAEAAIAADNyPkqAAAAEQAIAADRD39AAAAAAQAQAL9t8QFDaDwABcByAAISKQACADxNYWNpbnRvc2ggSEQ6VXNlcnM6AGpzaWVrOgBHb29nbGUgRHJpdmU6AGJpYjoAcDIwNy1kYW1hcy5wZGYADgAeAA4AcAAyADAANwAtAGQAYQBtAGEAcwAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAK1VzZXJzL2pzaWVrL0dvb2dsZSBEcml2ZS9iaWIvcDIwNy1kYW1hcy5wZGYAABMAAS8AABUAAgAM//8AAIAG0hscHR5aJGNsYXNzbmFtZVgkY2xhc3Nlc11OU011dGFibGVEYXRhox0fIFZOU0RhdGFYTlNPYmplY3TSGxwiI1xOU0RpY3Rpb25hcnmiIiBfEA9OU0tleWVkQXJjaGl2ZXLRJidUcm9vdIABAAgAEQAaACMALQAyADcAQABGAE0AVQBgAGcAagBsAG4AcQBzAHUAdwCEAI4AnQCiAKoCOAI6Aj8CSgJTAmECZQJsAnUCegKHAooCnAKfAqQAAAAAAAACAQAAAAAAAAAoAAAAAAAAAAAAAAAAAAACpg==},
 	Bdsk-Url-1 = {http://doi.acm.org/10.1145/582153.582176}}
 
 @article{Tarjan:1975bo,

+ 163 - 72
book.tex

@@ -672,7 +672,7 @@ In the next section we see our first example of a compiler, which is
 another example of structural recursion.
 
 
-\section{Partial Evaluation}
+\section{Example Compiler: a Partial Evaluator}
 \label{sec:partial-evaluation}
 
 In this section we consider a compiler that translates $R_0$
@@ -932,6 +932,9 @@ values. Figure~\ref{fig:x86-a} defines the syntax for the subset of
 the x86 assembly language needed for this chapter.  (We use the
 AT\&T syntax expected by the GNU assembler inside \key{gcc}.)
 
+% to do: finish treatment of imulq
+% it's needed for vector's in R6/R7
+
 \begin{figure}[tp]
 \fbox{
 \begin{minipage}{0.96\textwidth}
@@ -945,7 +948,7 @@ AT\&T syntax expected by the GNU assembler inside \key{gcc}.)
 \Arg &::=&  \key{\$}\Int \mid \key{\%}\Reg \mid \Int(\key{\%}\Reg) \\ 
 \Instr &::=& \key{addq} \; \Arg, \Arg \mid 
       \key{subq} \; \Arg, \Arg \mid 
-%      \key{imulq} \; \Arg,\Arg \mid 
+      \key{imulq} \; \Arg,\Arg \mid 
       \key{negq} \; \Arg \mid \key{movq} \; \Arg, \Arg \mid \\
   &&  \key{callq} \; \mathit{label} \mid
       \key{pushq}\;\Arg \mid \key{popq}\;\Arg \mid \key{retq} \\
@@ -2525,9 +2528,9 @@ shown in Figure~\ref{fig:reg-alloc-passes}.
 \path[->,bend left=15] (R1) edge [above] node {\ttfamily\footnotesize uniquify} (R1-2);
 \path[->,bend left=15] (R1-2) edge [right] node {\ttfamily\footnotesize flatten} (C0-1);
 \path[->,bend right=15] (C0-1) edge [left] node {\ttfamily\footnotesize select-instr.} (x86-2);
-\path[->,bend left=15] (x86-2) edge [right] node {\ttfamily\footnotesize uncover-live} (x86-2-1);
-\path[->,bend right=15] (x86-2-1) edge [below] node {\ttfamily\footnotesize build-inter.} (x86-2-2);
-\path[->,bend right=15] (x86-2-2) edge [right] node {\ttfamily\footnotesize allocate-reg.} (x86-3);
+\path[->,bend left=15] (x86-2) edge [right] node {\ttfamily\footnotesize\color{red} uncover-live} (x86-2-1);
+\path[->,bend right=15] (x86-2-1) edge [below] node {\ttfamily\footnotesize\color{red} build-inter.} (x86-2-2);
+\path[->,bend right=15] (x86-2-2) edge [right] node {\ttfamily\footnotesize\color{red} allocate-reg.} (x86-3);
 \path[->,bend left=15] (x86-3) edge [above] node {\ttfamily\footnotesize patch-instr.} (x86-4);
 \path[->,bend left=15] (x86-4) edge [above] node {\ttfamily\footnotesize print-x86} (x86-5);
 \end{tikzpicture}
@@ -3610,7 +3613,7 @@ if_end21289:
 \node (R1) at (0,2)  {\large $R_1$};
 \node (R1-2) at (3,2)  {\large $R_1$};
 \node (R1-3) at (6,2)  {\large $R_1$};
-\node (C0-1) at (3,0)  {\large $C_0$};
+\node (C1-1) at (3,0)  {\large $C_1$};
 
 \node (x86-2) at (3,-2)  {\large $\text{x86}^{*}$};
 \node (x86-3) at (6,-2)  {\large $\text{x86}^{*}$};
@@ -3621,18 +3624,18 @@ if_end21289:
 \node (x86-2-1) at (3,-4)  {\large $\text{x86}^{*}$};
 \node (x86-2-2) at (6,-4)  {\large $\text{x86}^{*}$};
 
-\path[->,bend left=15] (R1) edge [above] node {\ttfamily\footnotesize typecheck} (R1-2);
+\path[->,bend left=15] (R1) edge [above] node {\ttfamily\footnotesize\color{red} typecheck} (R1-2);
 \path[->,bend left=15] (R1-2) edge [above] node {\ttfamily\footnotesize uniquify} (R1-3);
-\path[->,bend left=15] (R1-3) edge [right] node {\ttfamily\footnotesize flatten} (C0-1);
-\path[->,bend right=15] (C0-1) edge [left] node {\ttfamily\footnotesize select-instr.} (x86-2);
-\path[->,bend left=15] (x86-2) edge [right] node {\ttfamily\footnotesize uncover-live} (x86-2-1);
+\path[->,bend left=15] (R1-3) edge [right] node {\ttfamily\footnotesize\color{red} flatten} (C1-1);
+\path[->,bend right=15] (C1-1) edge [left] node {\ttfamily\footnotesize\color{red} select-instr.} (x86-2);
+\path[->,bend left=15] (x86-2) edge [right] node {\ttfamily\footnotesize\color{red} uncover-live} (x86-2-1);
 \path[->,bend right=15] (x86-2-1) edge [below] node {\ttfamily\footnotesize build-inter.} (x86-2-2);
 \path[->,bend right=15] (x86-2-2) edge [right] node {\ttfamily\footnotesize allocate-reg.} (x86-3);
-\path[->,bend left=15] (x86-3) edge [above] node {\ttfamily\footnotesize lower-cond.} (x86-4);
-\path[->,bend left=15] (x86-4) edge [above] node {\ttfamily\footnotesize patch-instr.} (x86-5);
+\path[->,bend left=15] (x86-3) edge [above] node {\ttfamily\footnotesize\color{red} lower-cond.} (x86-4);
+\path[->,bend left=15] (x86-4) edge [above] node {\ttfamily\footnotesize\color{red} patch-instr.} (x86-5);
 \path[->,bend right=15] (x86-5) edge [left] node {\ttfamily\footnotesize print-x86} (x86-6);
 \end{tikzpicture}
-\caption{Diagram of the passes for $R_2$.}
+\caption{Diagram of the passes for $R_2$, a language with conditionals.}
 \label{fig:R2-passes}
 \end{figure}
 
@@ -3773,7 +3776,7 @@ if_end21289:
 
 In this chapter we study the implementation of mutable tuples (called
 ``vectors'' in Racket). This language feature is the first to require
-use of the ``heap'' because the lifetime of a Racket tuple is
+use the of the ``heap'' because the lifetime of a Racket tuple is
 indefinite, that is, the lifetime of a tuple does not follow a stack
 (FIFO) discipline but they instead live forever from the programmer's
 viewpoint. Of course, from an implementor's viewpoint, it is important
@@ -3909,7 +3912,7 @@ variables can refer to the same tuple, i.e., the variables can be
 \emph{aliases} for the same thing. Consider the following example in
 which both \code{t1} and \code{t2} refer to the same tuple.  Thus, the
 mutation through \code{t2} is visible when referencing the tuple from
-\code{t1} and the result of the program is therefore \code{42}.
+\code{t1}, so the result of the program is \code{42}.
 \begin{lstlisting}
 (let ([t1 (vector 3 7)])
   (let ([t2 t1])
@@ -3920,10 +3923,10 @@ mutation through \code{t2} is visible when referencing the tuple from
 The next issue concerns the lifetime of tuples. Of course, they are
 created by the \code{vector} form, but when does their lifetime end?
 Notice that the grammar in Figure~\ref{fig:r3-syntax} does not include
-an operation for deallocating tuples. Furthermore, the lifetime of a
-tuple is not tied to any notion of static scoping. For example, the
+an operation for deleting tuples. Furthermore, the lifetime of a tuple
+is not tied to any notion of static scoping. For example, the
 following program returns \code{3} even though the variable \code{t}
-goes out of scope prior to the reference.
+goes out of scope prior to accessing the vector.
 \begin{lstlisting}
 (vector-ref
   (let ([t (vector 3 7)])
@@ -3963,14 +3966,16 @@ not enough room for the next allocation request. At that point, the
 garbage collector goes to work to make more room.
 
 A running program has direct access to registers and the procedure
-call stack, and those may contain pointers into the heap. Those
+call stack, and they may contain pointers into the heap. Those
 pointers are called the \emph{root set}. In
 Figure~\ref{fig:copying-collector} there are three pointers in the
-root set, one in a register and two on the stack. 
+root set, one in a register and two on the stack.
 %
-\marginpar{\tiny We can't actually write a program that produces
-the heap structure in the Figure because there is no recursion. Once we
-have the dynamic type, we will be able to.\\ --Jeremy}
+\footnote{The sitation in Figure~\ref{fig:copying-collector}, with a
+  cycle, cannot be created by a well-typed program in $R_3$. However,
+  creating cycles will be possible once we get to $R_6$.
+  We design the garbage collector to deal with cycles 
+  to begin with, so we will not need to revisit this issue.}
 %
 The goal of the
 garbage collector is to 1) preserve all objects that are reachable
@@ -3999,16 +4004,16 @@ and second element is a 2-tuple.
 Let us take a closer look at how the copy works. The allocated objects
 and pointers essentially form a graph and we need to copy the part of
 the graph that is reachable from the root set. To make sure we copy
-all of the reachable nodes, we need an exhaustive traversal algorithm,
-such as depth-first search or breadth-first
+all of the reachable nodes, we need an exhaustive graph traversal
+algorithm, such as depth-first search or breadth-first
 search~\citep{Moore:1959aa,Cormen:2001uq}. Recall that such algorithms
 take into account the possibility of cycles by marking which objects
 have already been visited, so as to ensure termination of the
 algorithm. These search algorithms also use a data structure such as a
 stack or queue as a to-do list to keep track of the objects that need
-to be visited. Here we shall use breadth-first search and a trick due
-to Cheney~\citep{Cheney:1970aa} for simultaneously representing the
-queue and compacting the objects as they are copied into the ToSpace.
+to be visited. We shall use breadth-first search and a trick due to
+Cheney~\citep{Cheney:1970aa} for simultaneously representing the queue
+and copying the objects into the ToSpace.
 
 Figure~\ref{fig:cheney} shows several snapshots of the ToSpace as the
 copy progresses. The queue is represented by a chunk of contiguous
@@ -4019,20 +4024,22 @@ ToSpace to form the initial queue.  When we copy an object, we mark
 the old object to indicate that it has been visited. (We discuss the
 marking in Section~\ref{sec:data-rep-gc}.) Note that any pointers
 inside the copied objects in the queue still point back to the
-FromSpace. The algorithm then pops the object at the front of the
-queue and copies all the objects that are directly reachable from it
-to the ToSpace, at the back of the queue. The algorithm then updates
-the pointers in the popped object so they point to the newly copied
-objects. So getting back to Figure~\ref{fig:cheney}, in the first step
-we copy the tuple whose second element is $42$ to the back of the
-queue. The other pointer goes to a tuple that has already been copied,
-so we do not need to copy it again, but we do need to update the
-pointer to the new location. This can be accomplished by storing a
-\emph{forwarding} pointer to the new location in the old object, back
-when we initially copied the object into the ToSpace. This completes
-one step of the algorithm. The algorithm continues in this way until
-the front of the queue is empty, that is, until the front catches up
-with the back.
+FromSpace. Once the initial queue has been created, the algorithm
+enters a loop in which it repeatedly processes the object at the front
+of the queue and pops it off the queue.  To process an object, the
+algorithm copies all the objects that are directly reachable from it
+to the ToSpace, placing them at the back of the queue. The algorithm
+then updates the pointers in the popped object so they point to the
+newly copied objects. So getting back to Figure~\ref{fig:cheney}, in
+the first step we copy the tuple whose second element is $42$ to the
+back of the queue. The other pointer goes to a tuple that has already
+been copied, so we do not need to copy it again, but we do need to
+update the pointer to the new location. This can be accomplished by
+storing a \emph{forwarding} pointer to the new location in the old
+object, back when we initially copied the object into the
+ToSpace. This completes one step of the algorithm. The algorithm
+continues in this way until the front of the queue is empty, that is,
+until the front catches up with the back.
 
 
 \begin{figure}[tbp]
@@ -4043,7 +4050,7 @@ with the back.
 \end{figure}
 
 
-\section{Data Representation}
+\subsection{Data Representation}
 \label{sec:data-rep-gc}
 
 The garbage collector places some requirements on the data
@@ -4054,7 +4061,7 @@ are several ways to accomplish this.
 \item Attached a tag to each object that says what kind of object it
   is~\citep{Jones:1996aa}.
 \item Store different kinds of objects in different regions of
-  memory~\citep{Jr.:1977aa}.
+  memory~\citep{Steele:1977ab}.
 \item Use type information from the program to either generate
   type-specific code for collecting or to generate tables that can
   guide the
@@ -4071,20 +4078,19 @@ a relatively high implementation complexity. To keep this chapter to a
 with separate strategies used for the stack and the heap.
 
 Regarding the stack, we recommend using a separate stack for
-pointers~\citep{Siebert:2001aa,Henderson:2002aa,Baker:2009aa} (i.e., a
-``shadow stack''), which we call a \emph{root stack}. That is, when a
-local variable needs to be spilled and is of type \code{(Vector
-  $\Type_1 \ldots \Type_n$)}, then we put it on the root stack
-instead of the normal procedure call stack.
-Figure~\ref{fig:shadow-stack} reproduces the example from
-Figure~\ref{fig:copying-collector} and contrasts it with the data
-layout using a root stack. The root stack contains the two
-pointers from the regular stack and also the pointer in the second
-register. Prior to invoking the garbage collector, we shall push all
-pointers in local variables (resident in registers or spilled to the
-stack) onto the root stack.  After the collection, the pointers must
-be popped back into the local variables because the locations of the
-pointed-to objects will have changed.
+pointers~\citep{Siebert:2001aa,Henderson:2002aa,Baker:2009aa} , which
+we call a \emph{root stack} (a.k.a a ``shadow stack''). That is, when
+a local variable needs to be spilled and is of type \code{(Vector
+  $\Type_1 \ldots \Type_n$)}, then we put it on the root stack instead
+of the normal procedure call stack.  Figure~\ref{fig:shadow-stack}
+reproduces the example from Figure~\ref{fig:copying-collector} and
+contrasts it with the data layout using a root stack. The root stack
+contains the two pointers from the regular stack and also the pointer
+in the second register. Prior to invoking the garbage collector, we
+shall push all pointers in local variables (resident in registers or
+spilled to the stack) onto the root stack.  After the collection, the
+pointers must be popped back into the local variables because the
+locations of the pointed-to objects will have changed.
 
 \begin{figure}[tbp]
 \centering \includegraphics[width=0.7\textwidth]{root-stack}
@@ -4116,7 +4122,7 @@ are always zero anyways because our tuples are 8-byte aligned.)
 \label{fig:tuple-rep}
 \end{figure}
 
-\section{Implementation of the Garbage Collector}
+\subsection{Implementation of the Garbage Collector}
 \label{sec:organize-gz}
 
 The implementation of the garbage collector needs to do a lot of
@@ -4124,27 +4130,31 @@ bit-level data manipulation and we will need to link it with our
 compiler-generated x86 code. Thus, we recommend implementing the
 garbage collector in C~\citep{Kernighan:1988nx} and putting the code
 in the \code{runtime.c} file. Figure~\ref{fig:gc-header} shows the
-interface to the garbage collector. The function \code{initialize}
-should create the FromSpace, ToSpace, and root stack. The
-\code{initialize} function is meant to be called near the beginning of
-\code{main}, before the body of the program executes.  The
-\code{initialize} function should put the address of the beginning of
-the FromSpace into the global variable \code{free\_ptr}. The global
-\code{fromspace\_end} should point to the address that is 1-past the
-last element of the FromSpace. (We use half-open intervals to
-represent chunks of memory.)  The \code{rootstack\_begin} global
+interface to the garbage collector. The \code{initialize} function
+creates the FromSpace, ToSpace, and root stack. The \code{initialize}
+function is meant to be called near the beginning of \code{main},
+before the body of the program executes.  The \code{initialize}
+function puts the address of the beginning of the FromSpace into the
+global variable \code{free\_ptr}. The global \code{fromspace\_end}
+points to the address that is 1-past the last element of the
+FromSpace. (We use half-open intervals to represent chunks of
+memory~\citep{Dijkstra:1982aa}.)  The \code{rootstack\_begin} global
 should point to the first element of the root stack.
 
 As long as there is room left in the FromSpace, your generated code
 can allocate tuples simply by moving the \code{free\_ptr} forward.
+%
+\marginpar{\tiny Should we dedicate a register to the free pointer? \\
+--Jeremy}
+%
 The amount of room left in FromSpace is the difference between the
 \code{fromspace\_end} and the \code{free\_ptr}.  The \code{collect}
 function should be called when there is not enough room left in the
 FromSpace for the next allocation.  The \code{collect} function takes
 a pointer to the current top of the root stack (one past the last item
 that was pushed) and the number of bytes that need to be
-allocated. The \code{collect} should perform the copying collection
-and leave the heap in a state such that the next allocation will
+allocated. The \code{collect} function performs the copying collection
+and leaves the heap in a state such that the next allocation will
 succeed.
 
 \begin{figure}[tbp]
@@ -4152,13 +4162,49 @@ succeed.
    void initialize(uint64_t rootstack_size, uint64_t heap_size);
    void collect(int64_t** rootstack_ptr, uint64_t bytes_requested);
    int64_t* free_ptr;
+   int64_t* fromspace_begin;
    int64_t* fromspace_end;
    int64_t** rootstack_begin;
 \end{lstlisting}
-\caption{Interface to the garbage collector.}
+\caption{The compiler's interface to the garbage collector.}
 \label{fig:gc-header}
 \end{figure}
 
+\begin{exercise}
+  In the file \code{runtime.c} you will find the implementation of
+  \code{initialize} and a partial implementation of \code{collect}.
+  The \code{collect} function calls another function, \code{cheney},
+  to perform the actual copy, and that function is left to the reader
+  to implement. The following is the prototype for \code{cheney}.
+\begin{lstlisting}  
+   static void cheney(int64_t** rootstack_ptr);
+\end{lstlisting}
+  The parameter \code{rootstack\_ptr} is a pointer to the top of the
+  rootstack (which is array of pointers).  The \code{cheney} function
+  also communicates with \code{collect} through several global
+  variables, the \code{framespace\_begin} and \code{framespace\_end}
+  mentioned in Figure~\ref{fig:gc-header} as well as the pointers for
+  the ToSpace:
+\begin{lstlisting}
+   static int64_t* tospace_begin;
+   static int64_t* tospace_end;
+\end{lstlisting}
+  The job of the \code{cheney} function is to copy all the live
+  objects (reachable from the root stack) into the ToSpace, update
+  \code{free\_ptr} to point to the next unused spot in the ToSpace,
+  update the root stack so that it points to the objects in the
+  ToSpace, and finally to swap the global pointers for the FromSpace
+  and ToSpace.
+
+  [to do: talk about the \code{copy\_vector} auxilliary
+    function. --Jeremy]
+
+\end{exercise}
+
+
+
+
+
 \section{Compiler Passes}
 \label{sec:code-generation-gc}
 
@@ -4660,6 +4706,45 @@ if_end30967:
   implement the GC. \\ --Jeremy}
 
 
+\begin{figure}[p]
+\begin{tikzpicture}[baseline=(current  bounding  box.center)]
+\node (R1) at (0,2)  {\large $R_1$};
+\node (R1-2) at (3,2)  {\large $R_1$};
+\node (R1-3) at (6,2)  {\large $R_1$};
+\node (C1-1) at (9,0)  {\large $C_1$};
+\node (C1-2) at (6,0)  {\large $C_1$};
+\node (C1-3) at (3,0)  {\large $C_1$};
+
+\node (x86-2) at (3,-2)  {\large $\text{x86}^{*}$};
+\node (x86-3) at (6,-2)  {\large $\text{x86}^{*}$};
+\node (x86-4) at (9,-2) {\large $\text{x86}^{*}$};
+\node (x86-5) at (12,-2) {\large $\text{x86}$};
+\node (x86-6) at (12,-4) {\large $\text{x86}^{\dagger}$};
+
+\node (x86-2-1) at (3,-4)  {\large $\text{x86}^{*}$};
+\node (x86-2-2) at (6,-4)  {\large $\text{x86}^{*}$};
+
+\path[->,bend left=15] (R1) edge [above] node {\ttfamily\footnotesize typecheck} (R1-2);
+\path[->,bend left=15] (R1-2) edge [above] node {\ttfamily\footnotesize uniquify} (R1-3);
+\path[->,bend left=15] (R1-3) edge [right] node {\ttfamily\footnotesize flatten} (C1-1);
+\path[->,bend left=15] (C1-1) edge [below] node {\ttfamily\footnotesize\color{red} expose-alloc.} (C1-2);
+\path[->,bend left=15] (C1-2) edge [below] node {\ttfamily\footnotesize\color{red} uncover...roots} (C1-3);
+\path[->,bend right=15] (C1-3) edge [left] node {\ttfamily\footnotesize\color{red} select-instr.} (x86-2);
+\path[->,bend left=15] (x86-2) edge [right] node {\ttfamily\footnotesize uncover-live} (x86-2-1);
+\path[->,bend right=15] (x86-2-1) edge [below] node {\ttfamily\footnotesize build-inter.} (x86-2-2);
+\path[->,bend right=15] (x86-2-2) edge [right] node {\ttfamily\footnotesize allocate-reg.} (x86-3);
+\path[->,bend left=15] (x86-3) edge [above] node {\ttfamily\footnotesize lower-cond.} (x86-4);
+\path[->,bend left=15] (x86-4) edge [above] node {\ttfamily\footnotesize patch-instr.} (x86-5);
+\path[->,bend right=15] (x86-5) edge [left] node {\ttfamily\footnotesize print-x86} (x86-6);
+\end{tikzpicture}
+\caption{Diagram of the passes for $R_3$, a language with tuples.}
+\label{fig:R3-passes}
+\end{figure}
+
+Figure~\ref{fig:R3-passes} gives an overview of all the passes needed
+for the compilation of $R_3$.
+
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \chapter{Functions}
 \label{ch:functions}
@@ -4781,6 +4866,12 @@ Figure~\ref{fig:interp-R4}.
 \section{Functions in x86}
 \label{sec:fun-x86}
 
+\marginpar{\tiny Make sure callee save registers are discussed
+   in enough depth, especially updating Fig 6.4 \\ --Jeremy }
+
+\marginpar{\tiny Talk about the return address on the
+   stack and what callq  and retq does.\\ --Jeremy }
+
 The x86 architecture provides a few features to support the
 implementation of functions. We have already seen that x86 provides
 labels so that one can refer to the location of an instruction, as is
@@ -5707,7 +5798,7 @@ compilation of $R_6$ and $R_7$ in the remainder of this chapter.
     \mid (\key{lambda:}\; ([\Var \key{:} \Type]^{*}) \key{:} \Type \; \Exp)} \\
   & \mid & (\key{inject}\; \Exp \; \FType) \mid (\key{project}\;\Exp\;\FType) \\
   & \mid & (\key{boolean?}\;\Exp) \mid (\key{integer?}\;\Exp)\\
-  & \mid & (\key{vector?}\;\Exp) \mid (\key{procedure?}\;\Exp) \\
+  & \mid & (\key{vector?}\;\Exp) \mid (\key{procedure?}\;\Exp) \mid (\key{void?}\;\Exp) \\
   \Def &::=& \gray{(\key{define}\; (\Var \; [\Var \key{:} \Type]^{*}) \key{:} \Type \; \Exp)} \\
   R_6 &::=& \gray{(\key{program} \; \Def^{*} \; \Exp)}
 \end{array}

BIN
copy-collect-1.graffle


BIN
copy-collect-1.pdf


BIN
copy-collect-2.graffle


BIN
copy-collect-2.pdf