Abstract
This paper develops a type theory for Krivine-style evaluation and compilation. We first define a static type system for lambda terms where lambda abstraction is interpreted as a code to pop the “spine stack” and to continue execution. Higher-order feature is obtained by introducing a typing rule to convert a code to a closure. This is in contrast with the conventional type theory for the lambda calculus, where lambda abstraction always creates higher-order function. We then define a type system for Krivine-style low-level machine, and develops type-directed compilation from the term calculus to the Krivine-style machine. We establish that the compilation preserves both static and dynamic semantics. This type theoretical framework provides a proper basis to analyze various properties of compilation. To demonstrate the strength of our framework, we perform the above development for two versions of low-level machines, one of which statically determines the spine stack, and the other of which dynamically determines the spine stack using a runtime mark, and analyze their relative merit.
This work has been partially supported by Grant-in-aid for scientific research on basic research (B), no :15300006.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Choi, K., Han, T.: A type system for the push-enter model. Information Processing Letters 87, 205–211 (2003)
Choi, K., Ohori, A.: A type theory for Krivine-style evaluation and compilation. Technical report IS-RR-2004-014, JAIST (2004)
Cregut, P.: An abstract machine for the normalization of λ-terms. In: Proc. ACM Conference on LISP and Functional Programming, pp. 333–340 (1990)
Duba, B., Harper, R., MacQueen, D.: Typing first-class continuations in ML. In: Proc. ACM Symp. on Principles of Prog. Languages, pp. 163–173 (1991)
Hannan, J., Hicks, P.: Higher-order uncurrying. In: Proc. ACM Symposium on Principles of Programming Languages (1998)
Leroy, X.: The ZINC experiment: an economical implementation of the ML language. Technical Report 117, INRIA (1992)
Morrisett, G., Crary, K., Glew, N., Walker, D.: Stack-based typed assembly language. In: Sipper, M., Mange, D., Pérez-Uribe, A. (eds.) ICES 1998. LNCS, vol. 1478. Springer, Heidelberg (1998)
Ohori, A.: A Curry-Howard isomorphism for compilation and program execution. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol. 1581, pp. 179–258. Springer, Heidelberg (1999)
Ohori, A.: The logical abstract machine: a Curry-Howard isomorphism for machine code. In: Proc. International Symp. on Functional and Logic Programming (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Choi, K., Ohori, A. (2004). A Type Theory for Krivine-Style Evaluation and Compilation. In: Chin, WN. (eds) Programming Languages and Systems. APLAS 2004. Lecture Notes in Computer Science, vol 3302. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30477-7_15
Download citation
DOI: https://doi.org/10.1007/978-3-540-30477-7_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23724-2
Online ISBN: 978-3-540-30477-7
eBook Packages: Springer Book Archive