Phase Distinctions In The Compilation Of Epigram Export

@article{citeulike:315612, abstract = {We describe the execution of Epigram on a stock architecture such as the G-machine, compiling via a core type theory and a supercombinator language. We show, via optimising transformations on the core type theory, that unused or duplicated values can be erased at run-time. Thus there exists a phase distinction, not between types and values, but between values which are used at compile-time only and values which are used at run-time. Through a simple example, lookup of a value in a sized vector, we show how our optimisations remove compile-time only values from terms and, furthermore, how we can use straightforward static analysis with our rich type information to avoid the need for any run-time bounds check when executing the lookup function.}, author = {Mckinna, James and Brady, Edwin}, citeulike-article-id = {315612}, citeulike-linkout-0 = {http://www-fp.dcs.st-andrews.ac.uk/~eb/writings/epiphase.pdf}, keywords = {dependent-types, epigram, staged-programming}, posted-at = {2005-09-11 06:28:16}, priority = {2}, title = {Phase Distinctions In The Compilation Of Epigram}, url = {http://www-fp.dcs.st-andrews.ac.uk/~eb/writings/epiphase.pdf} }

TY - JOUR ID - citeulike:315612 L3 - citeulike-article-id:315612 N2 - We describe the execution of Epigram on a stock architecture such as the G-machine, compiling via a core type theory and a supercombinator language. We show, via optimising transformations on the core type theory, that unused or duplicated values can be erased at run-time. Thus there exists a phase distinction, not between types and values, but between values which are used at compile-time only and values which are used at run-time. Through a simple example, lookup of a value in a sized vector, we show how our optimisations remove compile-time only values from terms and, furthermore, how we can use straightforward static analysis with our rich type information to avoid the need for any run-time bounds check when executing the lookup function. TI - Phase Distinctions In The Compilation Of Epigram KW - dependent-types KW - epigram KW - staged-programming AU - Mckinna, James AU - Brady, Edwin UR - http://www-fp.dcs.st-andrews.ac.uk/~eb/writings/epiphase.pdf ER -