Explicit Substitutitions for Constructive Necessity Export

@misc{citeulike:401388, abstract = {Machine.  be applied to design an abstract machine from our modal calculus with explicit substitutions. The main application of our modal calculus is as a framework for specifying and analysing computation stages in the context of functional languages. We use our constructive type theory to translate a variant of Nielson and Nielson's two-level functional language whose two levels correspond to compile-time and run-time (types and) programs. This gives rise to a compile-time and a run-time...}, author = {Ghani, Neil and de Paiva, Valeria and Ritter, Eike}, citeulike-article-id = {401388}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.1759}, keywords = {explicit-subs, logic, modal}, posted-at = {2005-11-19 17:12:44}, priority = {0}, title = {Explicit Substitutitions for Constructive Necessity}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.1759} }

TY - GEN ID - citeulike:401388 L3 - citeulike-article-id:401388 N2 - Machine.  be applied to design an abstract machine from our modal calculus with explicit substitutions. The main application of our modal calculus is as a framework for specifying and analysing computation stages in the context of functional languages. We use our constructive type theory to translate a variant of Nielson and Nielson's two-level functional language whose two levels correspond to compile-time and run-time (types and) programs. This gives rise to a compile-time and a run-time... TI - Explicit Substitutitions for Constructive Necessity KW - explicit-subs KW - logic KW - modal AU - Ghani, Neil AU - de Paiva, Valeria AU - Ritter, Eike UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.1759 ER -