Merge branch 'master' of https://github.com/IUCompilerCourse/Essentials-of-Compilation

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

@@ -2460,15 +2460,14 @@ start:
 \end{minipage}
 \end{tabular} \\
 
-In the output of \code{select-instructions}, there is an entry for
-\code{locals-types} in the $\itm{info}$ of the \code{Program} node,
-which is needed here so that we have the list of variables that should
-be assigned to homes. The support code computes the
-\code{locals-types} entry. In particular, \code{type-check-C0}
-installs it in the $\itm{info}$ field of the \code{Program} node.
-When using \code{interp-tests} or \code{compiler-tests} (see Appendix,
-Section~\ref{appendix:utilities}), specify \code{type-check-C0} as the
-type checker to use after \code{explicate-control}.
+The \code{locals-types} entry in the $\itm{info}$ of the
+\code{X86Program} node is an alist mapping all the variables in the
+program to their types (for now just \code{Integer}).  The
+\code{assign-homes} pass should replace all uses of those variables
+with stack locations.  As an aside, the \code{locals-types} entry is
+computed by \code{type-check-Cvar} in the support code, which installs
+it in the $\itm{info}$ field of the \code{CProgram} node, which should
+be propagated to the \code{X86Program} node.
 
 In the process of assigning variables to stack locations, it is
 convenient for you to compute and store the size of the frame (in
@@ -2801,7 +2800,7 @@ If there are more than six arguments, then the convention is to use
 space on the frame of the caller for the rest of the
 arguments. However, in Chapter~\ref{ch:functions} we arrange to never
 need more than six arguments. For now, the only function we care about
-is \code{read\_int} and it takes zero arguments.
+is \code{read\_int} and it takes zero argument.
 %
 The register \code{rax} is for the return value of a function.
 
@@ -2812,7 +2811,7 @@ example from the caller point of view and then from the callee point
 of view.
 
 The program makes two calls to the \code{read} function.  Also, the
-variable \code{x} is in use during the second call to \code{read}, so
+variable \code{x} is in-use during the second call to \code{read}, so
 we need to make sure that the value in \code{x} does not get
 accidentally wiped out by the call to \code{read}.  One obvious
 approach is to save all the values in caller-saved registers to the
@@ -2826,16 +2825,16 @@ location in the first place. Or better yet, if we can arrange for
 \code{x} to be placed in a callee-saved register, then it won't need
 to be saved and restored during function calls.
 
-The approach that we recommend for variables that are in use during a
+The approach that we recommend for variables that are in-use during a
 function call is to either assign them to callee-saved registers or to
 spill them to the stack. On the other hand, for variables that are not
-in use during a function call, we try the following alternatives in
+in-use during a function call, we try the following alternatives in
 order 1) look for an available caller-saved register (to leave room
 for other variables in the callee-saved register), 2) look for a
 callee-saved register, and 3) spill the variable to the stack.
 
 It is straightforward to implement this approach in a graph coloring
-register allocator. First, we know which variables are in use during
+register allocator. First, we know which variables are in-use during
 every function call because we compute that information for every
 instruction (Section~\ref{sec:liveness-analysis-r1}). Second, when we
 build the interference graph (Section~\ref{sec:build-interference}),
@@ -3145,15 +3144,14 @@ interference graph is an undirected graph that has an edge between two
 locations if they are live at the same time, that is, if they
 interfere with each other.
 
-The most obvious way to compute the interference graph is to look at
-the set of live locations between each statement in the program and add
-an edge to the graph for every pair of variables in the same set.
-This approach is less than ideal for two reasons. First, it can be
-expensive because it takes $O(n^2)$ time to look at every pair in a
-set of $n$ live locations. Second, there is a special case in which
-two locations that are live at the same time do not actually interfere
-with each other: when they both contain the same value because we have
-assigned one to the other.
+An obvious way to compute the interference graph is to look at the set
+of live locations between each instruction and add an edge to the graph
+for every pair of variables in the same set.  This approach is less
+than ideal for two reasons. First, it can be expensive because it
+takes $O(n^2)$ time to consider at every pair in a set of $n$ live
+locations. Second, in the special case where two locations hold the
+same value (because one was assigned to the other), they can be live
+at the same time without interfering with each other.
 
 A better way to compute the interference graph is to focus on the
 writes~\cite{Appel:2003fk}. We do not want the writes performed by an
@@ -3299,14 +3297,12 @@ program, under the key \code{conflicts}.
 \index{Sudoku}
 \index{color}
 
-We come to the main event, mapping variables to registers (or to stack
-locations in the event that we run out of registers).  We need to make
-sure that two variables do not get mapped to the same register if the
-two variables interfere with each other.  Thinking about the
-interference graph, this means that adjacent vertices must be mapped
-to different registers.  If we think of registers as colors, the
-register allocation problem becomes the widely studied graph coloring
-problem~\citep{Balakrishnan:1996ve,Rosen:2002bh}.
+We come to the main event, mapping variables to registers and stack
+locations. Variables that interfere with each other must be mapped to
+different locations.  In terms of the interference graph, this means
+that adjacent vertices must be mapped to different locations.  If we
+think of locations as colors, the register allocation problem becomes
+the graph coloring problem~\citep{Balakrishnan:1996ve,Rosen:2002bh}.
 
 The reader may be more familiar with the graph coloring problem than he
 or she realizes; the popular game of Sudoku is an instance of the
@@ -3394,18 +3390,18 @@ locations. The registers that are not used for register allocation,
 such as \code{rax}, are assigned to negative integers. In particular,
 we assign $-1$ to \code{rax} and $-2$ to \code{rsp}.
 
-One might wonder why we include registers at all in the liveness
-analysis and interference graph.  For example, we never allocate a
-variable to \code{rax} and \code{rsp}, so it would be harmless to
-leave them out.  As we see in Chapter~\ref{ch:tuples}, when we begin
-to use register for passing arguments to functions, it will be
-necessary for those registers to appear in the interference graph
-because those registers will also be assigned to variables, and we
-don't want those two uses to encroach on each other. Regarding
-registers such as \code{rax} and \code{rsp} that are not used for
-variables, we could omit them from the interference graph, but that
-would require adding special cases to our algorithm, which would
-complicate the logic for little gain.
+%% One might wonder why we include registers at all in the liveness
+%% analysis and interference graph, for example, we never allocate a
+%% variable to \code{rax} and \code{rsp}, so it would be harmless to
+%% leave them out.  As we see in Chapter~\ref{ch:tuples}, when we begin
+%% to use register for passing arguments to functions, it will be
+%% necessary for those registers to appear in the interference graph
+%% because those registers will also be assigned to variables, and we
+%% don't want those two uses to encroach on each other. Regarding
+%% registers such as \code{rax} and \code{rsp} that are not used for
+%% variables, we could omit them from the interference graph but that
+%% would require adding special cases to our algorithm, which would
+%% complicate the logic for little gain.
 
 
 \begin{figure}[btp]
@@ -3717,51 +3713,24 @@ the patch instructions pass. In this example, the trivial move of
 movq -8(%rbp), %rax
 addq %rax, -16(%rbp)
 \end{lstlisting}
-
-We recommend creating a helper function named \code{color-graph} that
-takes an interference graph and a list of all the variables in the
-program. This function should return a mapping of variables to their
-colors (represented as natural numbers). By creating this helper
-function, you will be able to reuse it in Chapter~\ref{ch:functions}
-when you add support for functions.  To prioritize the processing of
-highly saturated nodes inside your \code{color-graph} function, we
-recommend using the priority queue data structure (see the side bar on
-the right). Note that you will also need to maintain a mapping from
-variables to their ``handles'' in the priority queue so that you can
-notify the priority queue when their saturation changes.
-
-\begin{wrapfigure}[23]{r}[1.0in]{0.6\textwidth}
-  \small
-  \begin{tcolorbox}[title=Priority Queue]
-    A \emph{priority queue} is a collection of items in which the
-    removal of items is governed by priority. In a ``min'' queue,
-    lower priority items are removed first. An implementation is in
-    \code{priority\_queue.rkt} of the support code.  \index{priority
-      queue} \index{minimum priority queue}
-  \begin{description}
-  \item[$\LP\code{make-pqueue}\,\itm{cmp}\RP$] constructs an empty
-    priority queue that uses the $\itm{cmp}$ predicate to determine
-    whether its first argument has priority lower than or equal to its
-    second argument.
-  \item[$\LP\code{pqueue-count}\,\itm{queue}\RP$] returns the number of
-    items in the queue.
-  \item[$\LP\code{pqueue-push!}\,\itm{queue}\,\itm{item}\RP$] inserts
-    the item into the queue and returns a handle for the item in the
-    queue.
-  \item[$\LP\code{pqueue-pop!}\,\itm{queue}\RP$] returns the item with
-    the lowest priority.
-  \item[$\LP\code{pqueue-decrease-key!}\,\itm{queue}\,\itm{handle}\RP$]
-    notifies the queue that the priority has decreased for the item
-    associated with the given handle.
-  \end{description}
-\end{tcolorbox}
-\end{wrapfigure}
-
-Once you have obtained the coloring from \code{color-graph}, you can
-assign the variables to registers or stack locations and then reuse
-code from the \code{assign-homes} pass from
-Section~\ref{sec:assign-r1} to replace the variables with their
-assigned location. 
+\end{minipage}
+$\Rightarrow\qquad$
+\begin{minipage}{0.45\textwidth}
+\begin{lstlisting}
+movq $1, -8(%rbp)
+movq $42, %rcx
+addq $7, -8(%rbp)
+movq -8(%rbp), %rax
+movq %rax, -16(%rbp)
+addq %rcx, -8(%rbp)
+movq -16(%rbp), %rcx
+negq %rcx
+movq -8(%rbp), %rax
+addq %rcx, %rax
+jmp conclusion
+\end{lstlisting}
+\end{minipage}
+\end{center}
   
 \begin{exercise}\normalfont
   Implement the compiler pass \code{allocate-registers}, which should
@@ -7465,7 +7434,7 @@ If there are
 more than six arguments, then the convention is to use space on the
 frame of the caller for the rest of the arguments. However, to ease
 the implementation of efficient tail calls
-(Section~\ref{sec:tail-call}), we arrange never to need more than six
+(Section~\ref{sec:tail-call}), we arrange to never need more than six
 arguments.
 %
 Also recall that the register \code{rax} is for the return value of

defs.tex

@@ -1,5 +1,56 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+\newcommand{\LangInt}{\ensuremath{R_{\ttm{Int}}}} % R0
+\newcommand{\LangVar}{\ensuremath{R_{\ttm{Var}}}} % R1
+\newcommand{\LangCVar}{\ensuremath{C_{\ttm{Var}}}} % C0
+\newcommand{\LangVarANF}{\ensuremath{R^{\mathsf{ANF}}_{\ttm{Var}}}}
+\newcommand{\LangIf}{\ensuremath{R_{\ttm{If}}}} %R2
+\newcommand{\LangCIf}{\ensuremath{C_{\ttm{If}}}} %C1
+\newcommand{\LangIfANF}{\ensuremath{R^{\mathsf{ANF}}_{\ttm{if}}}} %R2
+\newcommand{\LangVec}{\ensuremath{R_{\ttm{Vec}}}} %R3
+\newcommand{\LangCVec}{\ensuremath{C_{\ttm{Vec}}}} %C2
+\newcommand{\LangVecANF}{\ensuremath{R^{\mathsf{ANF}}_{\ttm{Vec}}}} %R3
+\newcommand{\LangAlloc}{\ensuremath{R_{\ttm{Alloc}}}} %R3'
+\newcommand{\LangFun}{\ensuremath{R_{\ttm{Fun}}}} %R4
+\newcommand{\LangCFun}{\ensuremath{C_{\ttm{Fun}}}} %C3
+\newcommand{\LangFunANF}{\ensuremath{R^{\mathsf{ANF}}_{\ttm{Fun}}}} %R4
+\newcommand{\LangFunRef}{\ensuremath{R_{\ttm{FunRef}}}} %F1
+\newcommand{\LangFunRefAlloc}{\ensuremath{R^{\ttm{Alloc}}_{\ttm{FunRef}}}} %R'4
+\newcommand{\LangLam}{\ensuremath{R_\lambda}} %R5
+\newcommand{\LangCLam}{\ensuremath{C_{\ttm{Clos}}}} %C4
+\newcommand{\LangAny}{\ensuremath{R_{\ttm{Any}}}} %R6
+\newcommand{\LangAnyFunRef}{\ensuremath{R^{\ttm{FunRef}}_{\ttm{Any}}}} %R'6
+\newcommand{\LangAnyAlloc}{\ensuremath{R^{\ttm{Alloc}}_{\ttm{Any}}}} %R'6
+\newcommand{\LangCAny}{\ensuremath{C_{\ttm{Any}}}} %C5
+\newcommand{\LangDyn}{\ensuremath{R_{\ttm{Dyn}}}} %R7
+\newcommand{\LangDynFunRef}{\ensuremath{R^{\ttm{FunRef}}_{\ttm{Dyn}}}} %R'7
+\newcommand{\LangLoop}{\ensuremath{R_{\ttm{While}}}} %R8
+\newcommand{\LangLoopFunRef}{\ensuremath{R^{\ttm{FunRef}}_{\ttm{While}}}} %R'8
+\newcommand{\LangLoopAlloc}{\ensuremath{R^{\ttm{Alloc}}_{\ttm{While}}}} %R'8
+\newcommand{\LangCLoop}{\ensuremath{C_{\circlearrowleft}}} %C7
+\newcommand{\LangLoopANF}{\ensuremath{R^{\mathsf{ANF}}_{\ttm{While}}}} %R8
+\newcommand{\LangGrad}{\ensuremath{R_{\ttm{?}}}} %R9
+\newcommand{\LangCast}{\ensuremath{R_{\ttm{cast}}}} %R9'
+\newcommand{\LangProxy}{\ensuremath{R_{\ttm{proxy}}}} %R8''
+\newcommand{\LangPVec}{\ensuremath{R_{\ttm{PVec}}}} %R8''
+\newcommand{\LangPVecFunRef}{\ensuremath{R^{\ttm{FunRef}}_{\ttm{PVec}}}} %R8''
+\newcommand{\LangPVecAlloc}{\ensuremath{R^{\ttm{Alloc}}_{\ttm{PVec}}}} %R8''
+\newcommand{\LangPoly}{\ensuremath{R_{\ttm{Poly}}}} %R10
+\newcommand{\LangInst}{\ensuremath{R_{\ttm{Inst}}}} %R'10
+\newcommand{\LangCLoopPVec}{\ensuremath{C^{\ttm{PVec}}_{\circlearrowleft}}} %Cp7
+
+\newcommand{\LangXVar}{\ensuremath{\mathrm{x86}_{\ttm{Var}}}} % pseudo x86_0
+\newcommand{\LangXASTInt}{\ensuremath{\mathrm{x86}_{\ttm{Int}}}} % x86_0
+\newcommand{\LangXInt}{\ensuremath{\mathrm{x86}_{\ttm{Int}}}} %x86^{\dagger}_0
+\newcommand{\LangXASTIf}{\ensuremath{\mathrm{x86}_{\ttm{If}}}} %x86_1
+\newcommand{\LangXIf}{\ensuremath{\mathrm{x86}_{\ttm{If}}}} %x86^{\dagger}_1
+\newcommand{\LangXIfVar}{\ensuremath{\mathrm{x86}^{\ttm{Var}}_{\ttm{If}}}} %x86^{*}_1
+\newcommand{\LangXASTGlobal}{\ensuremath{\mathrm{x86}_{\ttm{Global}}}} %x86_2
+\newcommand{\LangXGlobal}{\ensuremath{\mathrm{x86}_{\ttm{Global}}}} %x86^{\dagger}_2
+\newcommand{\LangXGlobalVar}{\ensuremath{\mathrm{x86}^{\ttm{Var}}_{\ttm{Global}}}} %x86^{*}_2
+\newcommand{\LangXIndCall}{\ensuremath{\mathrm{x86}_{\ttm{callq*}}}} %x86_3
+\newcommand{\LangXIndCallVar}{\ensuremath{\mathrm{x86}^{\ttm{Var}}_{\ttm{callq*}}}} %x86^*_3
+
 \newcommand{\itm}[1]{\ensuremath{\mathit{#1}}}
 \newcommand{\ttm}[1]{\ensuremath{\mathtt{#1}}}
 \newcommand{\Stmt}{\itm{stmt}}
@@ -26,17 +77,19 @@
 \newcommand{\RS}[0]{\key{]}}
 \newcommand{\INT}[1]{\key{(Int}\;#1\key{)}}
 \newcommand{\BOOL}[1]{\key{(Bool}\;#1\key{)}}
-\newcommand{\PRIM}[2]{\LP\key{Prim}~#1~\LP\key{list}~#2\RP\RP}
-\newcommand{\READ}{\key{(Prim}\;\code{'read}\;\key{'())}}
+\newcommand{\PRIM}[2]{\LP\key{Prim}~#1~\LP #2\RP\RP}
+\newcommand{\READ}{\key{(Prim}\;\code{read}\;\key{())}}
 \newcommand{\CREAD}{\key{(read)}}
-\newcommand{\NEG}[1]{\key{(Prim}\;\code{'-}\;\code{(list}\;#1\;\code{))}}
+\newcommand{\NEG}[1]{\key{(Prim}\;\code{-}\;\code{(}#1\code{))}}
 \newcommand{\CNEG}[1]{\LP\key{-}~#1\RP}
 \newcommand{\PROGRAM}[2]{\LP\code{Program}\;#1\;#2\RP}
+\newcommand{\CPROGRAM}[2]{\LP\code{CProgram}\;#1\;#2\RP}
+\newcommand{\XPROGRAM}[2]{\LP\code{X86Program}\;#1\;#2\RP}
 \newcommand{\PROGRAMDEFSEXP}[3]{\code{(ProgramDefsExp}~#1~#2~#3\code{)}}
 \newcommand{\PROGRAMDEFS}[2]{\code{(ProgramDefs}~#1~#2\code{)}}
-\newcommand{\ADD}[2]{\key{(Prim}\;\code{'+}\;\code{(list}\;#1\;#2\code{))}}
+\newcommand{\ADD}[2]{\key{(Prim}\;\code{+}\;\code{(}#1\;#2\code{))}}
 \newcommand{\CADD}[2]{\LP\key{+}~#1~#2\RP}
-\newcommand{\SUB}[2]{\key{(Prim}\;\code{'-}\;\code{(list}\;#1\;#2\code{))}}
+\newcommand{\SUB}[2]{\key{(Prim}\;\code{-}\;\code{(}#1\;#2\code{))}}
 \newcommand{\CSUB}[2]{\LP\key{-}~#1~#2\RP}
 \newcommand{\CWHILE}[2]{\LP\key{while}~#1~#2\RP}
 \newcommand{\WHILE}[2]{\LP\key{WhileLoop}~#1~#2\RP}
@@ -44,25 +97,26 @@
 \newcommand{\BEGIN}[2]{\LP\key{Begin}~#1~#2\RP}
 \newcommand{\CSETBANG}[2]{\LP\key{set!}~#1~#2\RP}
 \newcommand{\SETBANG}[2]{\LP\key{SetBang}~#1~#2\RP}
-\newcommand{\AND}[2]{\key{(Prim}\;\code{'and}\;\code{(list}\;#1\;#2\code{))}}
-\newcommand{\OR}[2]{\key{(Prim}\;\code{'or}\;\code{(list}\;#1\;#2\code{))}}
-\newcommand{\NOT}[1]{\key{(Prim}\;\code{'not}\;\code{(list}\;#1\;\code{))}}
-\newcommand{\UNIOP}[2]{\key{(Prim}\;#1\;\code{(list}\;#2\code{))}}
+\newcommand{\AND}[2]{\key{(Prim}\;\code{and}\;\code{(}#1\;#2\code{))}}
+\newcommand{\OR}[2]{\key{(Prim}\;\code{or}\;\code{(}#1\;#2\code{))}}
+\newcommand{\NOT}[1]{\key{(Prim}\;\code{not}\;\code{(}#1\;\code{))}}
+\newcommand{\UNIOP}[2]{\key{(Prim}\;#1\;\code{(}#2\code{))}}
 \newcommand{\CUNIOP}[2]{\LP #1\;#2 \RP}
-\newcommand{\BINOP}[3]{\key{(Prim}\;#1\;\code{(list}\;#2\;#3\code{))}}
+\newcommand{\BINOP}[3]{\key{(Prim}\;#1\;\code{(}#2\;#3\code{))}}
 \newcommand{\CBINOP}[3]{\LP #1\;#2\;#3\RP}
-\newcommand{\CLET}[3]{\LP\key{let}~\LP\LS\Var~\Exp\RS\RP~\Exp\RP}
+\newcommand{\CLET}[3]{\LP\key{let}~\LP\LS#1~#2\RS\RP~#3\RP}
 \newcommand{\CIF}[3]{\LP\key{if}~#1~#2~#3\RP}
 \newcommand{\VAR}[1]{\key{(Var}\;#1\key{)}}
 \newcommand{\LET}[3]{\key{(Let}~#1~#2~#3\key{)}}
 \newcommand{\IF}[3]{\key{(If}\,#1\;#2\;#3\key{)}}
-\newcommand{\VECTOR}[1]{\LP\key{Prim}\;\code{'vector}\;\LP\key{list}\;#1\RP\RP}
-\newcommand{\VECREF}[2]{\LP\key{Prim}\;\code{'vector-ref}\;\LP\key{list}\;#1\;#2\RP\RP}
-\newcommand{\VECSET}[3]{\LP\key{Prim}\;\code{'vector-set!}\;\LP\key{list}\;#1\;#2\;#3\RP\RP}
-\newcommand{\VECLEN}[1]{\LP\key{Prim}\;\code{'vector-length}\;\LP\key{list}\;#1\RP\RP}
-\newcommand{\ANYVECREF}[2]{\LP\key{Prim}\;\code{'any-vector-ref}\;\LP\key{list}\;#1\;#2\RP\RP}
-\newcommand{\ANYVECSET}[3]{\LP\key{Prim}\;\code{'any-vector-set!}\;\LP\key{list}\;#1\;#2\;#3\RP\RP}
-\newcommand{\ANYVECLEN}[1]{\LP\key{Prim}\;\code{'any-vector-length}\;\LP\key{list}\;#1\RP\RP}
+\newcommand{\CAST}[3]{\LP\key{Cast}~#1~#2~#3\RP}
+\newcommand{\VECTOR}[1]{\LP\key{Prim}\;\code{vector}\;\LP\;#1\RP\RP}
+\newcommand{\VECREF}[2]{\LP\key{Prim}\;\code{vector-ref}\;\LP\;#1\;#2\RP\RP}
+\newcommand{\VECSET}[3]{\LP\key{Prim}\;\code{vector-set!}\;\LP\;#1\;#2\;#3\RP\RP}
+\newcommand{\VECLEN}[1]{\LP\key{Prim}\;\code{vector-length}\;\LP\;#1\RP\RP}
+\newcommand{\ANYVECREF}[2]{\LP\key{Prim}\;\code{any-vector-ref}\;\LP\;#1\;#2\RP\RP}
+\newcommand{\ANYVECSET}[3]{\LP\key{Prim}\;\code{any-vector-set!}\;\LP\;#1\;#2\;#3\RP\RP}
+\newcommand{\ANYVECLEN}[1]{\LP\key{Prim}\;\code{any-vector-length}\;\LP\;#1\RP\RP}
 \newcommand{\CLOSURE}[2]{\LP\key{Closure}~#1~#2\RP}
 \newcommand{\ALLOC}[2]{\LP\key{Allocate}~#1~#2\RP}
 \newcommand{\ALLOCCLOS}[3]{\LP\key{AllocateClosure}~#1~#2~#3\RP}
@@ -78,6 +132,7 @@
 \newcommand{\CFUNREFARITY}[2]{\key{(fun-ref-arity}~#1~#2\code{)}}
 \newcommand{\LAMBDA}[3]{\key{(Lambda}~#1~#2~#3\code{)}}
 \newcommand{\CLAMBDA}[3]{\LP\key{lambda:}\,#1\,\key{:}\,#2\;\Exp\RP}
+\newcommand{\CGLAMBDA}[3]{\LP\key{lambda:}\,#1\,#2\;\Exp\RP}
 \newcommand{\INJECT}[2]{\LP\key{Inject}~#1~#2\RP}
 \newcommand{\PROJECT}[2]{\LP\key{Project}~#1~#2\RP}
 \newcommand{\CINJECT}[2]{\LP\key{inject}~#1~#2\RP}
@@ -94,13 +149,16 @@
 \newcommand{\REG}[1]{\key{(Reg}\;#1\key{)}}
 \newcommand{\BYTEREG}[1]{\key{(ByteReg}\;#1\key{)}}
 \newcommand{\DEREF}[2]{\key{(Deref}~#1~#2\key{)}}
-\newcommand{\DEF}[5]{\key{(Def}~#1~#2~#3~#4~#5\key{)}}
+\newcommand{\DEF}[5]{\LP\key{Def}~#1~#2~#3~#4~#5\RP}
 \newcommand{\CDEF}[4]{\LP\key{define}~\LP#1~#2\RP\,\key{:}\,#3~#4\RP}
+\newcommand{\CGDEF}[4]{\LP\key{define}~\LP#1~#2\RP\,#3~#4\RP}
+\newcommand{\DECL}[2]{\LP\key{Decl}~#1~#2\RP}
+\newcommand{\INST}[3]{\LP\key{Inst}~#1~#2~#3\RP}
 \newcommand{\CFG}[1]{\key{(CFG}\;#1\key{)}}
 \newcommand{\BLOCK}[2]{\key{(Block}\;#1\;#2\key{)}}
 \newcommand{\STACKLOC}[1]{(\key{stack}\;#1)}
-\newcommand{\BININSTR}[3]{\key{(Instr}\;#1\;\key{(list}\;#2\;#3\key{))}}
-\newcommand{\UNIINSTR}[2]{\key{(Instr}\;#1\;\key{(list}\;#2\key{))}}
+\newcommand{\BININSTR}[3]{\key{(Instr}\;#1\;\key{(}\;#2\;#3\key{))}}
+\newcommand{\UNIINSTR}[2]{\key{(Instr}\;#1\;\key{(}\;#2\key{))}}
 \newcommand{\CALLQ}[2]{\key{(Callq}~#1~#2\key{)}}
 \newcommand{\INDCALLQ}[2]{\key{(IndirectCallq}~#1~#2\key{)}}
 \newcommand{\RETQ}{\key{(Retq)}}