@article{morrisett_system_1999,
	title = {From system {F} to typed assembly language},
	volume = {21},
	issn = {01640925},
	doi = {10/dcgqj3},
	abstract = {We motivate the design of typed assembly language (TAL) and present a type-preserving ttranslation from Systemn F to TAL. The typed assembly language we pressent is based on a conventional RISC assembly language, but its static type sytem provides support for enforcing high-level language abstratctions, such as closures, tuples, and user-defined abstract data types. The type system ensures that well-typed programs cannot violatet these abstractionsl In addition, the typing constructs admit many low-level compiler optimiztaions. Our translation to TAL is specified as a sequence of type-preserving transformations, including CPS and closure conversion phases; type-correct source programs are mapped to type-correct assembly language. A key contribution is an approach to polymorphic closure conversion that is considerably simpler than previous work. The compiler and typed assembly lanugage provide a fully automatic way to produce certified code, suitable for use in systems where unstrusted and potentially malicious code must be checked for safety before execution.},
	number = {3},
	journal = {ACM Transactions on Programming Languages and Systems},
	author = {Morrisett, Greg and Walker, David and Crary, Karl and Glew, Neal},
	year = {1999},
	note = {ISBN: 0897919793},
	pages = {527--568}
}

{"_id":"oBqubpuGemxS3iSMw","bibbaseid":"morrisett-walker-crary-glew-fromsystemftotypedassemblylanguage-1999","authorIDs":[],"author_short":["Morrisett, G.","Walker, D.","Crary, K.","Glew, N."],"bibdata":{"bibtype":"article","type":"article","title":"From system F to typed assembly language","volume":"21","issn":"01640925","doi":"10/dcgqj3","abstract":"We motivate the design of typed assembly language (TAL) and present a type-preserving ttranslation from Systemn F to TAL. The typed assembly language we pressent is based on a conventional RISC assembly language, but its static type sytem provides support for enforcing high-level language abstratctions, such as closures, tuples, and user-defined abstract data types. The type system ensures that well-typed programs cannot violatet these abstractionsl In addition, the typing constructs admit many low-level compiler optimiztaions. Our translation to TAL is specified as a sequence of type-preserving transformations, including CPS and closure conversion phases; type-correct source programs are mapped to type-correct assembly language. A key contribution is an approach to polymorphic closure conversion that is considerably simpler than previous work. The compiler and typed assembly lanugage provide a fully automatic way to produce certified code, suitable for use in systems where unstrusted and potentially malicious code must be checked for safety before execution.","number":"3","journal":"ACM Transactions on Programming Languages and Systems","author":[{"propositions":[],"lastnames":["Morrisett"],"firstnames":["Greg"],"suffixes":[]},{"propositions":[],"lastnames":["Walker"],"firstnames":["David"],"suffixes":[]},{"propositions":[],"lastnames":["Crary"],"firstnames":["Karl"],"suffixes":[]},{"propositions":[],"lastnames":["Glew"],"firstnames":["Neal"],"suffixes":[]}],"year":"1999","note":"ISBN: 0897919793","pages":"527–568","bibtex":"@article{morrisett_system_1999,\n\ttitle = {From system {F} to typed assembly language},\n\tvolume = {21},\n\tissn = {01640925},\n\tdoi = {10/dcgqj3},\n\tabstract = {We motivate the design of typed assembly language (TAL) and present a type-preserving ttranslation from Systemn F to TAL. The typed assembly language we pressent is based on a conventional RISC assembly language, but its static type sytem provides support for enforcing high-level language abstratctions, such as closures, tuples, and user-defined abstract data types. The type system ensures that well-typed programs cannot violatet these abstractionsl In addition, the typing constructs admit many low-level compiler optimiztaions. Our translation to TAL is specified as a sequence of type-preserving transformations, including CPS and closure conversion phases; type-correct source programs are mapped to type-correct assembly language. A key contribution is an approach to polymorphic closure conversion that is considerably simpler than previous work. The compiler and typed assembly lanugage provide a fully automatic way to produce certified code, suitable for use in systems where unstrusted and potentially malicious code must be checked for safety before execution.},\n\tnumber = {3},\n\tjournal = {ACM Transactions on Programming Languages and Systems},\n\tauthor = {Morrisett, Greg and Walker, David and Crary, Karl and Glew, Neal},\n\tyear = {1999},\n\tnote = {ISBN: 0897919793},\n\tpages = {527--568}\n}\n\n","author_short":["Morrisett, G.","Walker, D.","Crary, K.","Glew, N."],"key":"morrisett_system_1999","id":"morrisett_system_1999","bibbaseid":"morrisett-walker-crary-glew-fromsystemftotypedassemblylanguage-1999","role":"author","urls":{},"downloads":0},"bibtype":"article","biburl":"https://bibbase.org/zotero/k4rtik","creationDate":"2020-05-31T17:07:22.756Z","downloads":0,"keywords":[],"search_terms":["system","typed","assembly","language","morrisett","walker","crary","glew"],"title":"From system F to typed assembly language","year":1999,"dataSources":["Z5Dp3qAJiMzxtvKMq"]}