finished poly chapter, added diagram to gradual typing

all.bib

@@ -2,13 +2,237 @@
 %% http://bibdesk.sourceforge.net/
 
 
-%% Created for Jeremy Siek at 2020-11-15 13:28:39 -0500 
+%% Created for Jeremy Siek at 2020-12-24 11:32:40 -0500 
 
 
 %% Saved with string encoding Unicode (UTF-8) 
 
 
 
+@inproceedings{Weeks:2006aa,
+	Abstract = {MLton is a stable, robust, widely ported, Standard ML (SML) compiler that generates efficient executables. Whole-program compilation is the key to MLton's success, significantly improving both correctness and efficiency. Whole-program compilation makes possible a number of optimizations that reduce or eliminate the cost of SML's powerful abstraction mechanisms, such as parametric modules, polymorphism, and higher-order functions. It also allows MLton to use a simply-typed, first-order, intermediate language. By structuring the bulk of MLton's optimizer as small passes on whole programs in this simple intermediate language, it is easy to implement and debug new optimizations. This intermediate language uses a variant of standard control-flow graphs and static single assignment form, which makes it easy to implement traditional local optimizations as well. Having the whole program also enables standard data representations such as unboxed integers and arrays, as well as efficient representations for user-defined data structures.This talk will describe MLton's approach to whole-program compilation, covering the optimizations and the intermediate languages, as well as some of the engineering challenges that were overcome to make it feasible to use MLton on programs with over one hundred thousand lines. It will also cover the history of the MLton project from its inception in 1997 until now, and give some lessons learned and thoughts on the future of MLton.},
+	Address = {New York, NY, USA},
+	Author = {Weeks, Stephen},
+	Booktitle = {Proceedings of the 2006 Workshop on ML},
+	Date-Added = {2020-12-24 11:32:36 -0500},
+	Date-Modified = {2020-12-24 11:32:37 -0500},
+	Doi = {10.1145/1159876.1159877},
+	Isbn = {1595934839},
+	Location = {Portland, Oregon, USA},
+	Numpages = {1},
+	Pages = {1},
+	Publisher = {Association for Computing Machinery},
+	Series = {ML '06},
+	Title = {Whole-Program Compilation in MLton},
+	Url = {https://doi.org/10.1145/1159876.1159877},
+	Year = {2006},
+	Bdsk-Url-1 = {https://doi.org/10.1145/1159876.1159877}}
+
+@inproceedings{Blelloch:1993aa,
+	Abstract = {This paper gives an overview of the implementation of NESL, a portable nested data-parallel language. This language and its implementation are the first to fully support nested data structures as well as nested data-parallel function calls. These features allow the concise description of parallel algorithms on irregular data, such as sparse matrices and graphs. In addition, they maintain the advantages of data-parallel languages: a simple programming model and portability. The current NESL implementation is based on an intermediate language called VCODE and a library of vector routines called CVL. It runs on the Connection Machine CM-2, the Cray Y-MP C90, and serial machines. We compare initial benchmark results of NESL with those of machine-specific code on these machines for three algorithms: least-squares line-fitting, median finding, and a sparse-matrix vector product. These results show that NESL's performance is competitive with that of machine-specific codes for regular dense data, and is often superior for irregular data.},
+	Address = {New York, NY, USA},
+	Author = {Blelloch, Guy E. and Hardwick, Jonathan C. and Chatterjee, Siddhartha and Sipelstein, Jay and Zagha, Marco},
+	Booktitle = {Proceedings of the Fourth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming},
+	Date-Added = {2020-12-24 11:30:46 -0500},
+	Date-Modified = {2020-12-24 11:30:47 -0500},
+	Doi = {10.1145/155332.155343},
+	Isbn = {0897915895},
+	Location = {San Diego, California, USA},
+	Numpages = {10},
+	Pages = {102--111},
+	Publisher = {Association for Computing Machinery},
+	Series = {PPOPP '93},
+	Title = {Implementation of a Portable Nested Data-Parallel Language},
+	Url = {https://doi.org/10.1145/155332.155343},
+	Year = {1993},
+	Bdsk-Url-1 = {https://doi.org/10.1145/155332.155343}}
+
+@inproceedings{Roe:1997aa,
+	Abstract = {Strongly typed polymorphism is necessary for expressing safe reusable code. Two orthogonal forms of polymorphism exist: inclusion and parametric, the Oberon language only supports the former. We describe a simple extension to Oberon to support parametric polymorphism. The extension is in keeping with the Oberon language: it is simple and has an explicit cost. In the paper we motivate the need for parametric polymorphism and describe an implementation in terms of translating extended Oberon to standard Oberon.},
+	Address = {Berlin, Heidelberg},
+	Author = {Roe, Paul and Szyperski, Clemens},
+	Booktitle = {Modular Programming Languages},
+	Date-Added = {2020-12-24 10:38:05 -0500},
+	Date-Modified = {2020-12-24 10:38:07 -0500},
+	Editor = {M{\"o}ssenb{\"o}ck, Hanspeter},
+	Isbn = {978-3-540-68328-5},
+	Pages = {140--154},
+	Publisher = {Springer Berlin Heidelberg},
+	Title = {Lightweight parametric polymorphism for Oberon},
+	Year = {1997},
+	Bdsk-File-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxA8Um9lLVN6eXBlcnNraTE5OTdfQ2hhcHRlcl9MaWdodHdlaWdodFBhcmFtZXRyaWNQb2x5bW9ycGgucGRmTxECAAAAAAACAAACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////H1JvZS1TenlwZXJza2kxOTk3XyNGRkZGRkZGRi5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAUERGIAAAAAAAAQACAAAKIGN1AAAAAAAAAAAAAAAAAANiaWIAAAIAWC86VXNlcnM6anNpZWs6RG9jdW1lbnRzOmJpYjpSb2UtU3p5cGVyc2tpMTk5N19DaGFwdGVyX0xpZ2h0d2VpZ2h0UGFyYW1ldHJpY1BvbHltb3JwaC5wZGYADgB6ADwAUgBvAGUALQBTAHoAeQBwAGUAcgBzAGsAaQAxADkAOQA3AF8AQwBoAGEAcAB0AGUAcgBfAEwAaQBnAGgAdAB3AGUAaQBnAGgAdABQAGEAcgBhAG0AZQB0AHIAaQBjAFAAbwBsAHkAbQBvAHIAcABoAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgBWVXNlcnMvanNpZWsvRG9jdW1lbnRzL2JpYi9Sb2UtU3p5cGVyc2tpMTk5N19DaGFwdGVyX0xpZ2h0d2VpZ2h0UGFyYW1ldHJpY1BvbHltb3JwaC5wZGYAEwABLwAAFQACAAz//wAAAAgADQAaACQAYwAAAAAAAAIBAAAAAAAAAAUAAAAAAAAAAAAAAAAAAAJn}}
+
+@article{Vliet:1985aa,
+	Address = {USA},
+	Author = {van Vliet, J. C. and Gladney, H. M.},
+	Date-Added = {2020-12-23 12:25:12 -0500},
+	Date-Modified = {2020-12-23 12:25:15 -0500},
+	Doi = {10.1002/spe.4380150902},
+	Issn = {0038-0644},
+	Issue_Date = {Sept. 1985},
+	Journal = {Softw. Pract. Exper.},
+	Month = sep,
+	Number = {9},
+	Numpages = {15},
+	Pages = {823--837},
+	Publisher = {John Wiley & Sons, Inc.},
+	Title = {An Evaluation of Tagging},
+	Url = {https://doi.org/10.1002/spe.4380150902},
+	Volume = {15},
+	Year = {1985},
+	Bdsk-File-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxASc3BlLjQzODAxNTA5MDIucGRmTxEBWAAAAAABWAACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////EnNwZS40MzgwMTUwOTAyLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAUERGIAAAAAAAAQACAAAKIGN1AAAAAAAAAAAAAAAAAANiaWIAAAIALi86VXNlcnM6anNpZWs6RG9jdW1lbnRzOmJpYjpzcGUuNDM4MDE1MDkwMi5wZGYADgAmABIAcwBwAGUALgA0ADMAOAAwADEANQAwADkAMAAyAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAsVXNlcnMvanNpZWsvRG9jdW1lbnRzL2JpYi9zcGUuNDM4MDE1MDkwMi5wZGYAEwABLwAAFQACAAz//wAAAAgADQAaACQAOQAAAAAAAAIBAAAAAAAAAAUAAAAAAAAAAAAAAAAAAAGV},
+	Bdsk-Url-1 = {https://doi.org/10.1002/spe.4380150902}}
+
+@article{Stefan:2011ab,
+	Abstract = {We describe a new, dynamic, floating-label approach to language-based information flow control, and present an implementation in Haskell. A labeled IO monad, LIO, keeps track of a current label and permits restricted access to IO functionality, while ensuring that the current label exceeds the labels of all data observed and restricts what can be modified. Unlike other language-based work, LIO also bounds the current label with a current clearance that provides a form of discretionary access control. In addition, programs may encapsulate and pass around the results of computations with different labels. We give precise semantics and prove confidentiality and integrity properties of the system.},
+	Address = {New York, NY, USA},
+	Author = {Stefan, Deian and Russo, Alejandro and Mitchell, John C. and Mazi\`{e}res, David},
+	Date-Added = {2020-12-10 14:17:48 -0500},
+	Date-Modified = {2020-12-10 14:17:50 -0500},
+	Doi = {10.1145/2096148.2034688},
+	Issn = {0362-1340},
+	Issue_Date = {December 2011},
+	Journal = {SIGPLAN Not.},
+	Keywords = {monad, information flow control, library},
+	Month = sep,
+	Number = {12},
+	Numpages = {12},
+	Pages = {95--106},
+	Publisher = {Association for Computing Machinery},
+	Title = {Flexible Dynamic Information Flow Control in Haskell},
+	Url = {https://doi.org/10.1145/2096148.2034688},
+	Volume = {46},
+	Year = {2011},
+	Bdsk-File-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxATMjA5NjE0OC4yMDM0Njg4LnBkZk8RAV4AAAAAAV4AAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAAAAAABCRAAB/////xMyMDk2MTQ4LjIwMzQ2ODgucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAD/////AAAAAFBERiAAAAAAAAEAAgAACiBjdQAAAAAAAAAAAAAAAAADYmliAAACAC8vOlVzZXJzOmpzaWVrOkRvY3VtZW50czpiaWI6MjA5NjE0OC4yMDM0Njg4LnBkZgAADgAoABMAMgAwADkANgAxADQAOAAuADIAMAAzADQANgA4ADgALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAC1Vc2Vycy9qc2llay9Eb2N1bWVudHMvYmliLzIwOTYxNDguMjAzNDY4OC5wZGYAABMAAS8AABUAAgAM//8AAAAIAA0AGgAkADoAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAABnA==},
+	Bdsk-Url-1 = {https://doi.org/10.1145/2096148.2034688}}
+
+@inproceedings{Stefan:2011aa,
+	Abstract = {We describe a new, dynamic, floating-label approach to language-based information flow control, and present an implementation in Haskell. A labeled IO monad, LIO, keeps track of a current label and permits restricted access to IO functionality, while ensuring that the current label exceeds the labels of all data observed and restricts what can be modified. Unlike other language-based work, LIO also bounds the current label with a current clearance that provides a form of discretionary access control. In addition, programs may encapsulate and pass around the results of computations with different labels. We give precise semantics and prove confidentiality and integrity properties of the system.},
+	Address = {New York, NY, USA},
+	Author = {Stefan, Deian and Russo, Alejandro and Mitchell, John C. and Mazi\`{e}res, David},
+	Booktitle = {Proceedings of the 4th ACM Symposium on Haskell},
+	Date-Added = {2020-12-10 14:17:48 -0500},
+	Date-Modified = {2020-12-10 14:17:50 -0500},
+	Doi = {10.1145/2034675.2034688},
+	Isbn = {9781450308601},
+	Keywords = {information flow control, library, monad},
+	Location = {Tokyo, Japan},
+	Numpages = {12},
+	Pages = {95--106},
+	Publisher = {Association for Computing Machinery},
+	Series = {Haskell '11},
+	Title = {Flexible Dynamic Information Flow Control in Haskell},
+	Url = {https://doi.org/10.1145/2034675.2034688},
+	Year = {2011},
+	Bdsk-Url-1 = {https://doi.org/10.1145/2034675.2034688}}
+
+@article{Buiras:2015ab,
+	Abstract = { Information-Flow Control (IFC) is a well-established approach for allowing untrusted code to manipulate sensitive data without disclosing it. IFC is typically enforced via type systems and static analyses or via dynamic execution monitors. The LIO Haskell library, originating in operating systems research, implements a purely dynamic monitor of the sensitivity level of a computation, particularly suitable when data sensitivity levels are only known at runtime. In this paper, we show how to give programmers the flexibility of deferring IFC checks to runtime (as in LIO), while also providing static guarantees---and the absence of runtime checks---for parts of their programs that can be statically verified (unlike LIO). We present the design and implementation of our approach, HLIO (Hybrid LIO), as an embedding in Haskell that uses a novel technique for deferring IFC checks based on singleton types and constraint polymorphism. We formalize HLIO, prove non-interference, and show how interesting IFC examples can be programmed. Although our motivation is IFC, our technique for deferring constraints goes well beyond and offers a methodology for programmer-controlled hybrid type checking in Haskell. },
+	Address = {New York, NY, USA},
+	Author = {Buiras, Pablo and Vytiniotis, Dimitrios and Russo, Alejandro},
+	Date-Added = {2020-12-10 14:06:22 -0500},
+	Date-Modified = {2020-12-10 14:06:24 -0500},
+	Doi = {10.1145/2858949.2784758},
+	Issn = {0362-1340},
+	Issue_Date = {September 2015},
+	Journal = {SIGPLAN Not.},
+	Keywords = {constraint kinds, singleton types, Information-flow control, dynamic typing, hybrid typing, data kinds, gradual typing},
+	Month = aug,
+	Number = {9},
+	Numpages = {13},
+	Pages = {289--301},
+	Publisher = {Association for Computing Machinery},
+	Title = {HLIO: Mixing Static and Dynamic Typing for Information-Flow Control in Haskell},
+	Url = {https://doi.org/10.1145/2858949.2784758},
+	Volume = {50},
+	Year = {2015},
+	Bdsk-Url-1 = {https://doi.org/10.1145/2858949.2784758}}
+
+@inproceedings{Buiras:2015aa,
+	Abstract = { Information-Flow Control (IFC) is a well-established approach for allowing untrusted code to manipulate sensitive data without disclosing it. IFC is typically enforced via type systems and static analyses or via dynamic execution monitors. The LIO Haskell library, originating in operating systems research, implements a purely dynamic monitor of the sensitivity level of a computation, particularly suitable when data sensitivity levels are only known at runtime. In this paper, we show how to give programmers the flexibility of deferring IFC checks to runtime (as in LIO), while also providing static guarantees---and the absence of runtime checks---for parts of their programs that can be statically verified (unlike LIO). We present the design and implementation of our approach, HLIO (Hybrid LIO), as an embedding in Haskell that uses a novel technique for deferring IFC checks based on singleton types and constraint polymorphism. We formalize HLIO, prove non-interference, and show how interesting IFC examples can be programmed. Although our motivation is IFC, our technique for deferring constraints goes well beyond and offers a methodology for programmer-controlled hybrid type checking in Haskell. },
+	Address = {New York, NY, USA},
+	Author = {Buiras, Pablo and Vytiniotis, Dimitrios and Russo, Alejandro},
+	Booktitle = {Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming},
+	Date-Added = {2020-12-10 14:06:22 -0500},
+	Date-Modified = {2020-12-10 14:06:24 -0500},
+	Doi = {10.1145/2784731.2784758},
+	Isbn = {9781450336697},
+	Keywords = {Information-flow control, constraint kinds, data kinds, dynamic typing, gradual typing, hybrid typing, singleton types},
+	Location = {Vancouver, BC, Canada},
+	Numpages = {13},
+	Pages = {289--301},
+	Publisher = {Association for Computing Machinery},
+	Series = {ICFP 2015},
+	Title = {HLIO: Mixing Static and Dynamic Typing for Information-Flow Control in Haskell},
+	Url = {https://doi.org/10.1145/2784731.2784758},
+	Year = {2015},
+	Bdsk-File-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxATMjg1ODk0OS4yNzg0NzU4LnBkZk8RAV4AAAAAAV4AAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAAAAAABCRAAB/////xMyODU4OTQ5LjI3ODQ3NTgucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAD/////AAAAAFBERiAAAAAAAAEAAgAACiBjdQAAAAAAAAAAAAAAAAADYmliAAACAC8vOlVzZXJzOmpzaWVrOkRvY3VtZW50czpiaWI6Mjg1ODk0OS4yNzg0NzU4LnBkZgAADgAoABMAMgA4ADUAOAA5ADQAOQAuADIANwA4ADQANwA1ADgALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAC1Vc2Vycy9qc2llay9Eb2N1bWVudHMvYmliLzI4NTg5NDkuMjc4NDc1OC5wZGYAABMAAS8AABUAAgAM//8AAAAIAA0AGgAkADoAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAABnA==},
+	Bdsk-Url-1 = {https://doi.org/10.1145/2784731.2784758}}
+
+@article{Xia:2019aa,
+	Abstract = {Interaction trees (ITrees) are a general-purpose data structure for representing the behaviors of recursive programs that interact with their environments. A coinductive variant of ``free monads,'' ITrees are built out of uninterpreted events and their continuations. They support compositional construction of interpreters from event handlers, which give meaning to events by defining their semantics as monadic actions. ITrees are expressive enough to represent impure and potentially nonterminating, mutually recursive computations, while admitting a rich equational theory of equivalence up to weak bisimulation. In contrast to other approaches such as relationally specified operational semantics, ITrees are executable via code extraction, making them suitable for debugging, testing, and implementing software artifacts that are amenable to formal verification. We have implemented ITrees and their associated theory as a Coq library, mechanizing classic domain- and category-theoretic results about program semantics, iteration, monadic structures, and equational reasoning. Although the internals of the library rely heavily on coinductive proofs, the interface hides these details so that clients can use and reason about ITrees without explicit use of Coq's coinduction tactics. To showcase the utility of our theory, we prove the termination-sensitive correctness of a compiler from a simple imperative source language to an assembly-like target whose meanings are given in an ITree-based denotational semantics. Unlike previous results using operational techniques, our bisimulation proof follows straightforwardly by structural induction and elementary rewriting via an equational theory of combinators for control-flow graphs.},
+	Address = {New York, NY, USA},
+	Articleno = {51},
+	Author = {Xia, Li-yao and Zakowski, Yannick and He, Paul and Hur, Chung-Kil and Malecha, Gregory and Pierce, Benjamin C. and Zdancewic, Steve},
+	Date-Added = {2020-12-04 14:33:24 -0500},
+	Date-Modified = {2020-12-04 14:33:28 -0500},
+	Doi = {10.1145/3371119},
+	Issue_Date = {January 2020},
+	Journal = {Proc. ACM Program. Lang.},
+	Keywords = {compiler correctness, Coq, coinduction, monads},
+	Month = dec,
+	Number = {POPL},
+	Numpages = {32},
+	Publisher = {Association for Computing Machinery},
+	Title = {Interaction Trees: Representing Recursive and Impure Programs in Coq},
+	Url = {https://doi.org/10.1145/3371119},
+	Volume = {4},
+	Year = {2019},
+	Bdsk-File-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhWzMzNzExMTkucGRmTxEBPgAAAAABPgACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////CzMzNzExMTkucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAUERGIAAAAAAAAQACAAAKIGN1AAAAAAAAAAAAAAAAAANiaWIAAAIAJy86VXNlcnM6anNpZWs6RG9jdW1lbnRzOmJpYjozMzcxMTE5LnBkZgAADgAYAAsAMwAzADcAMQAxADEAOQAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAJVVzZXJzL2pzaWVrL0RvY3VtZW50cy9iaWIvMzM3MTExOS5wZGYAABMAAS8AABUAAgAM//8AAAAIAA0AGgAkADAAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAABcg==},
+	Bdsk-Url-1 = {https://doi.org/10.1145/3371119}}
+
+@book{Barthe:2020aa,
+	Date-Added = {2020-12-04 10:20:39 -0500},
+	Date-Modified = {2020-12-04 10:20:59 -0500},
+	Doi = {10.1017/9781108770750},
+	Place = {Cambridge},
+	Publisher = {Cambridge University Press},
+	Title = {Foundations of Probabilistic Programming},
+	Year = {2020},
+	Bdsk-File-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxAsRm91bmRhdGlvbnNfb2ZfUHJvYmFiaWxpc3RpY19Qcm9ncmFtbWluZy5wZGZPEQHAAAAAAAHAAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAAAAAAAAQkQAAf////8fRm91bmRhdGlvbnNfb2ZfUHJvI0ZGRkZGRkZGLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA/////wAAAABQREYgAAAAAAABAAIAAAogY3UAAAAAAAAAAAAAAAAAA2JpYgAAAgBILzpVc2Vyczpqc2llazpEb2N1bWVudHM6YmliOkZvdW5kYXRpb25zX29mX1Byb2JhYmlsaXN0aWNfUHJvZ3JhbW1pbmcucGRmAA4AWgAsAEYAbwB1AG4AZABhAHQAaQBvAG4AcwBfAG8AZgBfAFAAcgBvAGIAYQBiAGkAbABpAHMAdABpAGMAXwBQAHIAbwBnAHIAYQBtAG0AaQBuAGcALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAEZVc2Vycy9qc2llay9Eb2N1bWVudHMvYmliL0ZvdW5kYXRpb25zX29mX1Byb2JhYmlsaXN0aWNfUHJvZ3JhbW1pbmcucGRmABMAAS8AABUAAgAM//8AAAAIAA0AGgAkAFMAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAACFw==},
+	Bdsk-Url-1 = {https://doi.org/10.1017/9781108770750}}
+
+@article{Devriese:2017aa,
+	Abstract = {There has long been speculation in the scientific literature on how to dynamically enforce parametricity such as that yielded by System F. Almost 20 years ago, Sumii and Pierce proposed a formal compiler from System F into the cryptographic lambda calculus: an untyped lambda calculus extended with an idealised model of encryption. They conjectured that this compiler was fully abstract, i.e. that compiled terms are contextually equivalent if and only if the original terms were, a property that can be seen as a form of secure compilation. The conjecture has received attention in several other publications since then, but remains open to this day.  More recently, several researchers have been looking at gradually-typed languages that extend System F. In this setting it is natural to wonder whether embedding System F into these gradually-typed languages preserves contextual equivalence and thus parametricity.  In this paper, we answer both questions negatively. We provide a concrete counterexample: two System F terms whose contextual equivalence is not preserved by the Sumii-Pierce compiler, nor the embedding into the polymorphic blame calculus. This counterexample relies on the absence in System F of what we call a universal type, i.e., a type that all other types can be injected into and extracted from. As the languages in which System F is compiled have a universal type, the compilation cannot be fully abstract; this paper explains why.  We believe this paper thus sheds light on recent results in the field of gradually typed languages and it provides a perspective for further research into secure compilation of polymorphic languages.},
+	Address = {New York, NY, USA},
+	Articleno = {38},
+	Author = {Devriese, Dominique and Patrignani, Marco and Piessens, Frank},
+	Date-Added = {2020-12-02 12:24:13 -0500},
+	Date-Modified = {2020-12-02 12:24:16 -0500},
+	Doi = {10.1145/3158126},
+	Issue_Date = {January 2018},
+	Journal = {Proc. ACM Program. Lang.},
+	Keywords = {fully abstract compilation, System F, sealing, parametricity, universal type},
+	Month = dec,
+	Number = {POPL},
+	Numpages = {23},
+	Publisher = {Association for Computing Machinery},
+	Title = {Parametricity versus the Universal Type},
+	Url = {https://doi.org/10.1145/3158126},
+	Volume = {2},
+	Year = {2017},
+	Bdsk-File-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhWzMxNTgxMjYucGRmTxEBPgAAAAABPgACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////CzMxNTgxMjYucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAUERGIAAAAAAAAQACAAAKIGN1AAAAAAAAAAAAAAAAAANiaWIAAAIAJy86VXNlcnM6anNpZWs6RG9jdW1lbnRzOmJpYjozMTU4MTI2LnBkZgAADgAYAAsAMwAxADUAOAAxADIANgAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAJVVzZXJzL2pzaWVrL0RvY3VtZW50cy9iaWIvMzE1ODEyNi5wZGYAABMAAS8AABUAAgAM//8AAAAIAA0AGgAkADAAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAABcg==},
+	Bdsk-Url-1 = {https://doi.org/10.1145/3158126}}
+
+@book{Moller:2020aa,
+	Author = {Anders M\o{}ller and Michael I. Schwartzbach},
+	Date-Added = {2020-11-20 09:34:19 -0500},
+	Date-Modified = {2020-11-20 09:35:12 -0500},
+	Publisher = {Aarhus University},
+	Title = {Static Program Analysis},
+	Year = {2020},
+	Bdsk-File-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhV3NwYS5wZGZPEQEuAAAAAAEuAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAAAAAAAAQkQAAf////8Hc3BhLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA/////wAAAABQREYgAAAAAAABAAIAAAogY3UAAAAAAAAAAAAAAAAAA2JpYgAAAgAjLzpVc2Vyczpqc2llazpEb2N1bWVudHM6YmliOnNwYS5wZGYAAA4AEAAHAHMAcABhAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAhVXNlcnMvanNpZWsvRG9jdW1lbnRzL2JpYi9zcGEucGRmAAATAAEvAAAVAAIADP//AAAACAANABoAJAAsAAAAAAAAAgEAAAAAAAAABQAAAAAAAAAAAAAAAAAAAV4=}}
+
 @inproceedings{Gilray:2016aa,
 	Abstract = { Traditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been published that provide perfect call-stack precision in a computable manner: CFA2, PDCFA, and AAC. Unfortunately, implementing CFA2 and PDCFA requires significant engineering effort. Furthermore, all three are computationally expensive. For a monovariant analysis, CFA2 is in O(2^n), PDCFA is in O(n^6), and AAC is in O(n^8). In this paper, we describe a new technique that builds on these but is both straightforward to implement and computationally inexpensive. The crucial insight is an unusual state-dependent allocation strategy for the addresses of continuations. Our technique imposes only a constant-factor overhead on the underlying analysis and costs only O(n^3) in the monovariant case. We present the intuitions behind this development, benchmarks demonstrating its efficacy, and a proof of the precision of this analysis. },
 	Address = {New York, NY, USA},
@@ -1203,7 +1427,7 @@
 	Url = {http://doi.acm.org/10.1145/3229061},
 	Volume = {40},
 	Year = {2018},
-	Bdsk-File-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXGExNi10b3JvLnBkZk8RASwAAAAAASwAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAAAAAABCRAAB/////wxhMTYtdG9yby5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAD/////AAAAAAAAAAAAAAAAAAEAAgAACiBjdQAAAAAAAAAAAAAAAAADYmliAAACAB4vOlVzZXJzOmpzaWVrOmJpYjphMTYtdG9yby5wZGYADgAaAAwAYQAxADYALQB0AG8AcgBvAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAcVXNlcnMvanNpZWsvYmliL2ExNi10b3JvLnBkZgATAAEvAAAVAAIADP//AAAACAANABoAJAAxAAAAAAAAAgEAAAAAAAAABQAAAAAAAAAAAAAAAAAAAWE=},
+	Bdsk-File-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhWzMyMjkwNjEucGRmTxEBPgAAAAABPgACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////CzMyMjkwNjEucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAUERGIAAAAAAAAQACAAAKIGN1AAAAAAAAAAAAAAAAAANiaWIAAAIAJy86VXNlcnM6anNpZWs6RG9jdW1lbnRzOmJpYjozMjI5MDYxLnBkZgAADgAYAAsAMwAyADIAOQAwADYAMQAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAJVVzZXJzL2pzaWVrL0RvY3VtZW50cy9iaWIvMzIyOTA2MS5wZGYAABMAAS8AABUAAgAM//8AAAAIAA0AGgAkADAAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAABcg==},
 	Bdsk-Url-1 = {http://doi.acm.org/10.1145/3229061},
 	Bdsk-Url-2 = {http://dx.doi.org/10.1145/3229061}}
 
@@ -10321,13 +10545,13 @@ Gradual typing has explored how to incrementally move between static typing and
 @techreport{Sussman:1975ab,
 	Author = {Gerald Jay Sussman and Guy L. Steele, Jr.},
 	Date-Added = {2016-01-04 20:07:25 +0000},
-	Date-Modified = {2016-01-04 20:08:29 +0000},
+	Date-Modified = {2020-12-20 15:59:40 -0500},
 	Institution = {MIT},
 	Month = {December},
 	Number = {AI Memo No. 349},
 	Title = {Scheme: an interpreter for extended lambda calculus},
 	Year = {1975},
-	Bdsk-File-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhW0FJTS0zNDkucGRmTxEBKgAAAAABKgACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////C0FJTS0zNDkucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAAAAAAAAAAAAAAQACAAAKIGN1AAAAAAAAAAAAAAAAAANiaWIAAAIAHS86VXNlcnM6anNpZWs6YmliOkFJTS0zNDkucGRmAAAOABgACwBBAEkATQAtADMANAA5AC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAbVXNlcnMvanNpZWsvYmliL0FJTS0zNDkucGRmAAATAAEvAAAVAAIADP//AAAACAANABoAJAAwAAAAAAAAAgEAAAAAAAAABQAAAAAAAAAAAAAAAAAAAV4=}}
+	Bdsk-File-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhW0FJTS0zNDkucGRmTxEBPgAAAAABPgACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////C0FJTS0zNDkucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAAAAAAAAAAAAAAQACAAAKIGN1AAAAAAAAAAAAAAAAAANiaWIAAAIAJy86VXNlcnM6anNpZWs6RG9jdW1lbnRzOmJpYjpBSU0tMzQ5LnBkZgAADgAYAAsAQQBJAE0ALQAzADQAOQAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAJVVzZXJzL2pzaWVrL0RvY3VtZW50cy9iaWIvQUlNLTM0OS5wZGYAABMAAS8AABUAAgAM//8AAAAIAA0AGgAkADAAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAABcg==}}
 
 @book{Lane:1997aa,
 	Author = {Saunders Mac Lane},
@@ -24272,7 +24496,7 @@ semantics was validated.},
 	Source = {http://www.ncstrl.org:8900/ncstrl/servlet/search?formname=detail\&id=oai%3Ancstrlh%3Amitai%3AMIT-LCS%2F%2FMIT%2FLCS%2FTR-370},
 	Title = {A COMPILER FOR THE MIT TAGGED-TOKEN DATAFLOW ARCHITECTURE},
 	Year = {1986},
-	Bdsk-File-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxASTUlULUxDUy1UUi0zNzAucGRmTxEBRAAAAAABRAACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////Ek1JVC1MQ1MtVFItMzcwLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAAAAAAAAAAAAAAQACAAAKIGN1AAAAAAAAAAAAAAAAAANiaWIAAAIAJC86VXNlcnM6anNpZWs6YmliOk1JVC1MQ1MtVFItMzcwLnBkZgAOACYAEgBNAEkAVAAtAEwAQwBTAC0AVABSAC0AMwA3ADAALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASACJVc2Vycy9qc2llay9iaWIvTUlULUxDUy1UUi0zNzAucGRmABMAAS8AABUAAgAM//8AAAAIAA0AGgAkADkAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAABgQ==}}
+	Bdsk-File-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxASTUlULUxDUy1UUi0zNzAucGRmTxEBWAAAAAABWAACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////Ek1JVC1MQ1MtVFItMzcwLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAAAAAAAAAAAAAAQACAAAKIGN1AAAAAAAAAAAAAAAAAANiaWIAAAIALi86VXNlcnM6anNpZWs6RG9jdW1lbnRzOmJpYjpNSVQtTENTLVRSLTM3MC5wZGYADgAmABIATQBJAFQALQBMAEMAUwAtAFQAUgAtADMANwAwAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAsVXNlcnMvanNpZWsvRG9jdW1lbnRzL2JpYi9NSVQtTENTLVRSLTM3MC5wZGYAEwABLwAAFQACAAz//wAAAAgADQAaACQAOQAAAAAAAAIBAAAAAAAAAAUAAAAAAAAAAAAAAAAAAAGV}}
 
 @inproceedings{Schauser:1995it,
 	Author = {Klaus E. Schauser and Seth C. Goldstein},
@@ -33933,8 +34157,7 @@ these issues in Haskell.
 	Publisher = {ACM Press},
 	Title = {Programming with abstract data types},
 	Year = {1974},
-	Bdsk-File-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxAeLi4vLi4vLi4vcGFwZXJzL3A1MC1saXNrb3YucGRmTxEBbgAAAAABbgACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAwQ+lh0grAAAAT5kRDnA1MC1saXNrb3YucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAATyAnBv0ceAAAAAAAAAAAAAwACAAAJIAAAAAAAAAAAAAAAAAAAAAZwYXBlcnMAEAAIAADBD/nnAAAAEQAIAADBv6mOAAAAAQAMAE+ZEQBOpFMARsk2AAIALU1hY2ludG9zaCBIRDpVc2VyczpzaWVrOnBhcGVyczpwNTAtbGlza292LnBkZgAADgAeAA4AcAA1ADAALQBsAGkAcwBrAG8AdgAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAIFVzZXJzL3NpZWsvcGFwZXJzL3A1MC1saXNrb3YucGRmABMAAS8AABUAAgAL//8AAAAIAA0AGgAkAEUAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAABtw==},
-	Bdsk-File-2 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXnA1MC1saXNrb3YucGRmTxEBSAAAAAABSAACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////DnA1MC1saXNrb3YucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAAAAAAAAAAAAAAQACAAAKIGN1AAAAAAAAAAAAAAAAAANiaWIAAAIAKi86VXNlcnM6anNpZWs6RG9jdW1lbnRzOmJpYjpwNTAtbGlza292LnBkZgAOAB4ADgBwADUAMAAtAGwAaQBzAGsAbwB2AC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAoVXNlcnMvanNpZWsvRG9jdW1lbnRzL2JpYi9wNTAtbGlza292LnBkZgATAAEvAAAVAAIADP//AAAACAANABoAJAAzAAAAAAAAAgEAAAAAAAAABQAAAAAAAAAAAAAAAAAAAX8=},
+	Bdsk-File-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXnA1MC1saXNrb3YucGRmTxEBSAAAAAABSAACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////DnA1MC1saXNrb3YucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAAAAAAAAAAAAAAQACAAAKIGN1AAAAAAAAAAAAAAAAAANiaWIAAAIAKi86VXNlcnM6anNpZWs6RG9jdW1lbnRzOmJpYjpwNTAtbGlza292LnBkZgAOAB4ADgBwADUAMAAtAGwAaQBzAGsAbwB2AC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAoVXNlcnMvanNpZWsvRG9jdW1lbnRzL2JpYi9wNTAtbGlza292LnBkZgATAAEvAAAVAAIADP//AAAACAANABoAJAAzAAAAAAAAAgEAAAAAAAAABQAAAAAAAAAAAAAAAAAAAX8=},
 	Bdsk-Url-1 = {http://doi.acm.org/10.1145/800233.807045}}
 
 @book{Yourdon:1979kl,
@@ -42186,7 +42409,8 @@ software productivity and reliability },
 	Source = {http://www.lcs.mit.edu/publications/specpub.php?id=793},
 	Title = {{CLU} Reference Manual},
 	Year = {1979},
-	Bdsk-File-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxAhLi4vRHJvcGJveC9iaWIvTUlULUxDUy1UUi0yMjUucGRmTxEBkAAAAAABkAACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAADmrhEk1JVC1MQ1MtVFItMjI1LnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAQAzLM5ZsUAAAAAAAAAAAAAQADAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAAzOXhZAAAAAEAEAAOauEADmndAAXAcgACEikAAgA7TWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoARHJvcGJveDoAYmliOgBNSVQtTENTLVRSLTIyNS5wZGYAAA4AJgASAE0ASQBUAC0ATABDAFMALQBUAFIALQAyADIANQAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAKlVzZXJzL2pzaWVrL0Ryb3Bib3gvYmliL01JVC1MQ1MtVFItMjI1LnBkZgATAAEvAAAVAAIADP//AAAACAANABoAJABIAAAAAAAAAgEAAAAAAAAABQAAAAAAAAAAAAAAAAAAAdw=}}
+	Bdsk-File-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxASTUlULUxDUy1UUi0yMjUucGRmTxEBWAAAAAABWAACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////Ek1JVC1MQ1MtVFItMjI1LnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAUERGIAAAAAAAAQACAAAKIGN1AAAAAAAAAAAAAAAAAANiaWIAAAIALi86VXNlcnM6anNpZWs6RG9jdW1lbnRzOmJpYjpNSVQtTENTLVRSLTIyNS5wZGYADgAmABIATQBJAFQALQBMAEMAUwAtAFQAUgAtADIAMgA1AC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgAsVXNlcnMvanNpZWsvRG9jdW1lbnRzL2JpYi9NSVQtTENTLVRSLTIyNS5wZGYAEwABLwAAFQACAAz//wAAAAgADQAaACQAOQAAAAAAAAIBAAAAAAAAAAUAAAAAAAAAAAAAAAAAAAGV},
+	Bdsk-File-2 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxAhLi4vRHJvcGJveC9iaWIvTUlULUxDUy1UUi0yMjUucGRmTxEBkAAAAAABkAACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzcjA6kgrAAAADmrhEk1JVC1MQ1MtVFItMjI1LnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAQAzLM5ZsUAAAAAAAAAAAAAQADAAAJIAAAAAAAAAAAAAAAAAAAAANiaWIAABAACAAAzcj5KgAAABEACAAAzOXhZAAAAAEAEAAOauEADmndAAXAcgACEikAAgA7TWFjaW50b3NoIEhEOlVzZXJzOgBqc2llazoARHJvcGJveDoAYmliOgBNSVQtTENTLVRSLTIyNS5wZGYAAA4AJgASAE0ASQBUAC0ATABDAFMALQBUAFIALQAyADIANQAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAKlVzZXJzL2pzaWVrL0Ryb3Bib3gvYmliL01JVC1MQ1MtVFItMjI1LnBkZgATAAEvAAAVAAIADP//AAAACAANABoAJABIAAAAAAAAAgEAAAAAAAAABQAAAAAAAAAAAAAAAAAAAdw=}}
 
 @inproceedings{augustsson98:_cayenne,
 	Address = {New York, {NY}, {USA}},

book.tex

@@ -11831,9 +11831,9 @@ function in Figure~\ref{fig:guarded-vector}.  In the
 \code{differentiate-proxies} pass we shift this responsibility to the
 generated code.
 
-We begin by designing the output language $R_{\mathrm{proxy}}$.  In
+We begin by designing the output language $R^p_8$.  In
 $R_9$ we used the type \code{Vector} for both real vectors and vector
-proxies. In $R_{\mathrm{proxy}}$ we return the \code{Vector} type to
+proxies. In $R^p_8$ we return the \code{Vector} type to
 its original meaning, as the type of real vectors, and we introduce a
 new type, \code{GVector}, whose values can be either real vectors or
 vector proxies. This new type comes with a suite of new primitive
@@ -12064,6 +12064,78 @@ be translated in a similar way.
   \code{((lambda (x) x) e)}.
 \end{exercise}
 
+\begin{figure}[p]
+\begin{tikzpicture}[baseline=(current  bounding  box.center)]
+\node (R9) at (6,4)  {\large $R_9$};
+\node (R9p) at (3,4)  {\large $R'_9$};
+\node (R8pp) at (0,4)  {\large $R''_8$};
+\node (R8proxy) at (0,2)  {\large $R^p_8$};
+\node (R8proxy-2) at (3,2)  {\large $R^p_8$};
+\node (R8proxy-3) at (6,2)  {\large $R^p_8$};
+\node (R8proxy-4) at (9,2)  {\large $R^p_8$};
+\node (R8proxy-5) at (12,2)  {\large $R^p_8$};
+\node (F1-1) at (12,0)  {\large $R^p_8$};
+\node (F1-2) at (9,0)  {\large $R^p_8$};
+\node (F1-3) at (6,0)  {\large $R^p_8$};
+\node (F1-4) at (3,0)  {\large $R^p_8$};
+\node (F1-5) at (0,0)  {\large $R^p_8$};
+\node (C3-2) at (3,-2)  {\large $C^p_7$};
+
+\node (x86-2) at (3,-4)  {\large $\text{x86}^{*}_3$};
+\node (x86-3) at (6,-4)  {\large $\text{x86}^{*}_3$};
+\node (x86-4) at (9,-4) {\large $\text{x86}^{*}_3$};
+\node (x86-5) at (9,-6) {\large $\text{x86}^{\dagger}_3$};
+
+\node (x86-2-1) at (3,-6)  {\large $\text{x86}^{*}_3$};
+\node (x86-2-2) at (6,-6)  {\large $\text{x86}^{*}_3$};
+
+\path[->,bend right=15] (R9) edge [above] node
+     {\ttfamily\footnotesize type-check} (R9p);
+\path[->,bend right=15] (R9p) edge [above] node
+     {\ttfamily\footnotesize lower-casts} (R8pp);
+\path[->,bend right=15] (R8pp) edge [right] node
+     {\ttfamily\footnotesize differentiate-proxies} (R8proxy);
+\path[->,bend left=15] (R8proxy) edge [above] node
+     {\ttfamily\footnotesize shrink} (R8proxy-2);
+\path[->,bend left=15] (R8proxy-2) edge [above] node
+     {\ttfamily\footnotesize uniquify} (R8proxy-3);
+\path[->,bend left=15] (R8proxy-3) edge [above] node
+     {\ttfamily\footnotesize reveal-functions} (R8proxy-4);
+\path[->,bend left=15] (R8proxy-4) edge [above] node
+     {\ttfamily\footnotesize reveal-casts} (R8proxy-5);
+\path[->,bend left=15] (R8proxy-5) edge [left] node
+     {\ttfamily\footnotesize convert-assignments} (F1-1);
+\path[->,bend left=15] (F1-1) edge [below] node
+     {\ttfamily\footnotesize convert-to-clos.} (F1-2);
+\path[->,bend right=15] (F1-2) edge [above] node
+     {\ttfamily\footnotesize limit-fun.} (F1-3);
+\path[->,bend right=15] (F1-3) edge [above] node
+     {\ttfamily\footnotesize expose-alloc.} (F1-4);
+\path[->,bend right=15] (F1-4) edge [above] node
+     {\ttfamily\footnotesize remove-complex.} (F1-5);
+\path[->,bend right=15] (F1-5) edge [right] node
+     {\ttfamily\footnotesize explicate-control} (C3-2);
+\path[->,bend left=15] (C3-2) edge [left] node
+     {\ttfamily\footnotesize select-instr.} (x86-2);
+\path[->,bend right=15] (x86-2) edge [left] 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 [left] node
+     {\ttfamily\footnotesize 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 [right] node {\ttfamily\footnotesize print-x86} (x86-5);
+\end{tikzpicture}
+  \caption{Diagram of the passes for $R_9$ (gradual typing).}
+\label{fig:R9-passes}
+\end{figure}
+
+Figure~\ref{fig:R9-passes} provides an overview of all the passes needed
+for the compilation of $R_9$.
+
+
+
 \section{Further Reading}
 
 This chapter just scratches the surface of gradual typing.  The basic
@@ -12134,6 +12206,7 @@ type for parameter \code{a}. In Figure~\ref{fig:map-vec-poly} we apply
 vector of Booleans (and a function on Booleans).
 
 \begin{figure}[tbp]
+  % poly_test_2.rkt
 \begin{lstlisting}
 (: map-vec (All (a) ((a -> a) (Vector a a) -> (Vector a a))))
 (define (map-vec f v)
@@ -12299,6 +12372,24 @@ process in next pass of the compiler.
 \label{fig:r10-prime-syntax}
 \end{figure}
 
+The output of the type checker on the polymorphic \code{map-vec}
+example is listed in Figure~\ref{fig:map-vec-type-check}.
+
+\begin{figure}[tbp]
+  % poly_test_2.rkt
+\begin{lstlisting}
+(poly (a) (define (map-vec [f : (a -> a)] [v : (Vector a a)]) : (Vector a a)
+  (vector (f (vector-ref v 0)) (f (vector-ref v 1)))))
+
+(define (add1 [x : Integer]) : Integer (+ x 1))
+
+(vector-ref ((inst map-vec (All (a) ((a -> a) (Vector a a) -> (Vector a a)))
+                           (Integer))
+              add1 (vector 0 41)) 1)
+\end{lstlisting}
+\caption{Output of the type checker on the \code{map-vec} example.}
+\label{fig:map-vec-type-check}
+\end{figure}
 
 \begin{figure}[tbp]
 \begin{lstlisting}[basicstyle=\ttfamily\scriptsize]
@@ -12439,7 +12530,7 @@ process in next pass of the compiler.
 
 
 \begin{figure}[tbp]
-\begin{lstlisting}[basicstyle=\ttfamily\scriptsize]
+\begin{lstlisting}%[basicstyle=\ttfamily\scriptsize]
 (define/public ((check-well-formed env) ty)
   (match ty
     ['Integer (void)]
@@ -12463,12 +12554,12 @@ process in next pass of the compiler.
 \label{fig:well-formed-types}
 \end{figure}
 
-% TODO: interpreter for R10
+% TODO: interpreter for R'_10
 
 \section{Compiling Polymorphism}
 \label{sec:compiling-poly}
 
-Broadly speaking, there are three approaches to compiling parametric
+Broadly speaking, there are four approaches to compiling parametric
 polymorphism, which we describe below.
 
 \begin{description}
@@ -12482,65 +12573,162 @@ polymorphism, which we describe below.
   generic functions are used with which type arguments during
   compilation. (It can be done at runtime, with just-in-time
   compilation.) This approach is used to compile C++
-  templates~\citep{stroustrup88:_param_types}.
+  templates~\citep{stroustrup88:_param_types} and polymorphic
+  functions in NESL~\citep{Blelloch:1993aa} and
+  ML~\citep{Weeks:2006aa}.
   
 \item[Uniform representation] generates one version of each
-  polymorphic function but requires all values have a common format,
-  such as values of the \code{Any} type in $R_6$. Non-polymorphic code
-  (i.e. monomorphic code) is compiled similarly to code in a
-  dynamically typed language (like $R_7$), in which primitive
-  operators require their arguments to be projected from \code{Any}
-  and their results are injected into \code{Any}. This approach is
+  polymorphic function but requires all values have a common ``boxed''
+  format, such as the tagged values of type \code{Any} in
+  $R_6$. Non-polymorphic code (i.e. monomorphic code) is compiled
+  similarly to code in a dynamically typed language (like $R_7$), in
+  which primitive operators require their arguments to be projected
+  from \code{Any} and their results are injected into \code{Any}.  (In
+  object-oriented languages, the projection is accomplished via
+  virtual method dispatch.) The uniform representation approach is
   compatible with separate compilation and with first-class
   polymorphism.  However, it produces the least-efficient code because
   it introduces overhead in the entire program, including
-  non-polymorphic code. Some compilers for the ML language use the
-  uniform representation~\citep{Cardelli:1984aa,Appel:1987aa}.
-
-\item[Mixed representation] also generates one version of each
-  polymorphic function, using \code{Any} to represent type variables.
-  However, non-polymorphic code is compiled as usual (as in $R_8$) and
-  conversions are applied at the points of instantiations. This
-  approach is also compatible with separate compilation and
-  first-class polymorphism, but maintains the efficiency of
-  non-polymorphic code. The cost is some overhead at the boundary
-  between monomorphic and polymorphic code.
-
-  UNDER CONSTRUCTION
-  \citet{Leroy:1992qb}
-  \citep{Morrison:1991aa}
-  Java
+  non-polymorphic code. This approach is used in the implementation of
+  CLU~\cite{liskov79:_clu_ref,Liskov:1993dk},
+  ML~\citep{Cardelli:1984aa,Appel:1987aa}, and
+  Java~\citep{Bracha:1998fk}.
+  
+\item[Mixed representation] generates one version of each polymorphic
+  function, using a boxed representation for type
+  variables. Monomorphic code is compiled as usual (as in $R_8$) and
+  conversions are performed at the boundaries between monomorphic and
+  polymorphic (e.g. when a polymorphic function is instantiated and
+  called). This approach is compatible with separate compilation and
+  first-class polymorphism and maintains the efficiency for
+  monomorphic code. The tradeoff is increased overhead at the boundary
+  between monomorphic and polymorphic code.  This approach is used in
+  compilers for variants of ML~\citep{Leroy:1992qb} and starting in
+  Java 5 with the addition of autoboxing.
+  
+\item[Type passing] uses the unboxed representation in both
+  monomorphic and polymorphic code. Each polymorphic function is
+  compiled to a single function with extra parameters that describe
+  the type arguments. The type information is used by the generated
+  code to direct access of the unboxed values at runtime. This
+  approach is used in compilers for the Napier88
+  language~\citep{Morrison:1991aa} and ML~\citep{Harper:1995um}.  This
+  approach is compatible with separate compilation and first-class
+  polymorphism and maintains the efficiency for monomorphic
+  code. There is runtime overhead in polymorphic code from dispatching
+  on type information.
 \end{description}
 
+In this chapter we use the mixed representation approach, partly
+because of its favorable attributes, and partly because it is
+straightforward to implement using the tools that we have already
+built to support gradual typing. To compile polymorphic functions, we
+add just one new pass, \code{erase-types}, to compile $R_{10}$ to
+$R'_9$.
 
-%% This chapter may be based on ideas from \citet{Cardelli:1984aa},
-%% \citet{Leroy:1992qb}, \citet{Shao:1997uj}, or \citet{Harper:1995um}.
-
-% compile-time specialization: Ada, C++
-%   pos: efficient wrt. time
-%   neg: code size, no separate compilation, no first-class polymorphism
+\section{Erase Types}
+\label{sec:erase-types}
 
-% run-time specialization: C#
+We use the \code{Any} type from Chapter~\ref{ch:type-dynamic} to
+represent type variables. For example, Figure~\ref{fig:map-vec-erase}
+shows the output of the \code{erase-types} pass on the polymorphic
+\code{map-vec} (Figure~\ref{fig:map-vec-poly}). The occurrences of
+type parameter \code{a} are replaced by \code{Any} and the polymorphic
+\code{All} types are removed from the type of \code{map-vec}. 
 
-% box everywhere: early ML \citep{Cardelli:1984aa,Appel:1987aa}
+\begin{figure}[tbp]
+\begin{lstlisting}
+(define (map-vec [f : (Any -> Any)] [v : (Vector Any Any)])
+                   : (Vector Any Any)
+  (vector (f (vector-ref v 0)) (f (vector-ref v 1))))
 
-% mixed representations:
-%    Vliet:1985aa
-%    (Gallium Caml compiler) \citet{Leroy:1992qb}, 
-%    Napier88 \citep{Morrison:1991aa}
-%    Java
+(define (add1 [x : Integer]) : Integer (+ x 1))
 
-% Morrison:1991aa An ad hoc approach to the implementation of polymorphism.
-% by Morrison, Dearle, Connor, and Brown, 1991.
-%    uses type tags
+(vector-ref ((cast map-vec
+                     ((Any -> Any) (Vector Any Any) -> (Vector Any Any))  
+                     ((Integer -> Integer) (Vector Integer Integer)
+                               -> (Vector Integer Integer)))
+             add1 (vector 0 41)) 1)
+\end{lstlisting}
+\caption{The polymorphic \code{map-vec} example after type erasure.}
+\label{fig:map-vec-erase}
+\end{figure}
 
-% Cardelli:1984aa: 
+This process of type erasure creates a challenge at points of
+instantiation. For example, consider the instantiation of
+\code{map-vec} in Figure~\ref{fig:map-vec-type-check}.
+The type of \code{map-vec} is
+\begin{lstlisting}
+(All (a) ((a -> a) (Vector a a) -> (Vector a a)))
+\end{lstlisting}
+and it is instantiated to 
+\begin{lstlisting}
+((Integer -> Integer) (Vector Integer Integer)
+   -> (Vector Integer Integer))
+\end{lstlisting}
+After erasure, the type of \code{map-vec} is
+\begin{lstlisting}
+((Any -> Any) (Vector Any Any) -> (Vector Any Any))
+\end{lstlisting}
+but we need to convert it to the instantiated type.  This is easy to
+do in the target language $R'_9$ with a single \code{cast}.  In
+Figure~\ref{fig:map-vec-erase}, the instantiation of \code{map-vec}
+has been compiled to a \code{cast} from the type of \code{map-vec} to
+the instantiated type. The source and target type of a cast must be
+consistent (Figure~\ref{fig:consistent}), which indeed is the case
+because both the source and target are obtained from the same
+polymorphic type of \code{map-vec}, replacing the type parameters with
+\code{Any} in the former and with the deduced type arguments in the
+later. (Recall that the \code{Any} type is consistent with any type.)
 
-\section{Erase Types}
-\label{sec:erase-types}
+To implement the \code{erase-types} pass, we recommend defining a
+recursive auxiliary function named \code{erase-type} that applies the
+following two transformations. It replaces type variables with
+\code{Any}
+\begin{lstlisting}
+|$x$|
+|$\Rightarrow$|
+Any
+\end{lstlisting}
+and it removes the polymorphic \code{All} types.
+\begin{lstlisting}
+(All |$xs$| |$T_1$|)
+|$\Rightarrow$|
+|$T'_1$|
+\end{lstlisting}
+Apply the \code{erase-type} function to all of the type annotations in
+the program.
 
+Regarding the translation of expressions, the case for \code{Inst} is
+the interesting one. We translate it into a \code{Cast}, as shown
+below. The type of the subexpression $e$ is the polymorphic type
+$\LP\key{All} xs T\RP$. The source type of the cast is the erasure of
+$T$, the type $T'$. The target type $T''$ is the result of
+substituting the arguments types $ts$ for the type parameters $xs$ in
+$T$ followed by doing type erasure.
+\begin{lstlisting}
+(Inst |$e$| (All |$xs$| |$T$|) |$ts$|)
+|$\Rightarrow$|
+(Cast |$e'$| |$T'$| |$T''$|)
+\end{lstlisting}
+where $T'' = \LP\code{erase-type}~\LP\code{subst-type}~s~T\RP\RP$
+and $s = \LP\code{map}~\code{cons}~xs~ts\RP$.
 
+Finally, each polymorphic function is translated to a regular
+functions in which type erasure has been applied to all the type
+annotations and the body.
+\begin{lstlisting}
+(Poly |$ts$| (Def |$f$| ([|$x_1$| : |$T_1$|] |$\ldots$|) |$T_r$| |$\itm{info}$| |$e$|))
+|$\Rightarrow$|          
+(Def |$f$| ([|$x_1$| : |$T'_1$|] |$\ldots$|) |$T'_r$| |$\itm{info}$| |$e'$|)
+\end{lstlisting}
 
+\begin{exercise}\normalfont
+  Implement a compiler for the polymorphic language $R_{10}$ by
+  extending and adapting your compiler for $R_9$. Create 6 new test
+  programs that use polymorphic functions. Some of them should make
+  use of first-class polymorphism. 
+\end{exercise}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %% \chapter{High-level Optimization}