A Type Theory for Krivine-Style Evaluation and Compilation

  • Kwanghoon Choi
  • Atsushi Ohori
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3302)


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.


Type System Type Theory Operational Semantic Current Spine Typing Rule 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Choi, K., Han, T.: A type system for the push-enter model. Information Processing Letters 87, 205–211 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Choi, K., Ohori, A.: A type theory for Krivine-style evaluation and compilation. Technical report IS-RR-2004-014, JAIST (2004)Google Scholar
  3. 3.
    Cregut, P.: An abstract machine for the normalization of λ-terms. In: Proc. ACM Conference on LISP and Functional Programming, pp. 333–340 (1990)Google Scholar
  4. 4.
    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)Google Scholar
  5. 5.
    Hannan, J., Hicks, P.: Higher-order uncurrying. In: Proc. ACM Symposium on Principles of Programming Languages (1998)Google Scholar
  6. 6.
    Leroy, X.: The ZINC experiment: an economical implementation of the ML language. Technical Report 117, INRIA (1992)Google Scholar
  7. 7.
    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)Google Scholar
  8. 8.
    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)CrossRefGoogle Scholar
  9. 9.
    Ohori, A.: The logical abstract machine: a Curry-Howard isomorphism for machine code. In: Proc. International Symp. on Functional and Logic Programming (1999)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Kwanghoon Choi
    • 1
  • Atsushi Ohori
    • 1
  1. 1.School of Information ScienceJapan Advanced Institute of Science and TechnologyTatsunokuchi, IshikawaJapan

Personalised recommendations