article · 2009

Biorthogonality, step-indexing and compiler correctness

Cited by 119Abstract and details only

Abstract

We define logical relations between the denotational semantics of a simply typed functional language with recursion and the operational behaviour of low-level programs in a variant SECD machine. The relations, which are defined using biorthogonality and stepindexing, capture what it means for a piece of low-level code to implement a mathematical, domain-theoretic function and are used to prove correctness of a simple compiler. The results have been formalized in the Coq proof assistant.

Cite this paper

APA 7

Benton, N., & Hur, C.-K. (2009). Biorthogonality, step-indexing and compiler correctness. https://doi.org/10.1145/1596550.1596567

MLA 9

Benton, Nick, and Chung-Kil Hur. “Biorthogonality, step-indexing and compiler correctness.” 2009, pp. 97–108, https://doi.org/10.1145/1596550.1596567.

Chicago

Benton, Nick, and Chung-Kil Hur. 2009. “Biorthogonality, step-indexing and compiler correctness.” https://doi.org/10.1145/1596550.1596567.

Harvard

Benton, N. and Hur, C.-K. (2009) ‘Biorthogonality, step-indexing and compiler correctness’. Available at: https://doi.org/10.1145/1596550.1596567.

BibTeX

@article{benton2009biorthogonality,
  title = {{Biorthogonality, step-indexing and compiler correctness}},
  author = {Benton, Nick and Hur, Chung-Kil},
  pages = {97--108},
  year = {2009},
  doi = {10.1145/1596550.1596567}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.