A type theory for Krivine-style evaluation and compilation

Kwanghoon Choi, Atsushi Ohori

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)


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.

Original languageEnglish
Pages (from-to)213-228
Number of pages16
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Publication statusPublished - 2004 Dec 1

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A type theory for Krivine-style evaluation and compilation'. Together they form a unique fingerprint.

Cite this