The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.

Verified compilation on a verified processor

The work

AuthorsAndreas Lööw; Ramana Kumar; Yong Kiam Tan; Magnus O. Myreen; Michael Norrish; Oskar Abrahamsson; Anthony C. J. Fox
Editors
Typemisc
Year2019
Citekeyloow2019verified

Where it appeared

Published inProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation
Pages1041--1053

Identifiers

DOI10.1145/3314221.3314622
OpenAlexW2953840721

From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.

Abstract

Developing technology for building verified stacks, i.e., computer systems with comprehensive proofs of correctness, is one way the science of programming languages furthers the computing discipline. While there have been successful projects verifying complex, realistic system components, including compilers (software) and processors (hardware), to date these verification efforts have not been compatible to the point of enabling a single end-to-end correctness theorem about running a verified compiler on a verified processor.

How it got here

How it got hereagent via openalex
Added2026-10-26 04:42 UTC
Not denied bya person 2026-10-29 17:12 UTC

Cite it as

@misc{loow2019verified,
  title        = {Verified compilation on a verified processor},
  author       = {Andreas Lööw and Ramana Kumar and Yong Kiam Tan and Magnus O. Myreen and Michael Norrish and Oskar Abrahamsson and Anthony C. J. Fox},
  year         = {2019},
  journal      = {Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation},
  pages        = {1041--1053},
  doi          = {10.1145/3314221.3314622},
}

This record lives at https://refs.drheap.org/loow2019verified/ and will keep doing so.