# Changeset 2352 for Papers

Ignore:
Timestamp:
Sep 26, 2012, 5:57:59 PM (9 years ago)
Message:

Removed repeated references as suggested by the referee

File:
1 edited

### Legend:

Unmodified
 r2351 Aside from their application in verified compiler projects such as CerCo, CompCert~\cite{leroy:formally:2009} and CompCertTSO~\cite{sevcik:relaxed-memory:2011}, verified assemblers such as ours could also be applied to the verification of operating system kernels. Of particular note is the verified seL4 kernel~\cite{klein:sel4:2009,klein:sel4:2010}. Of particular note is the verified seL4 kernel~\cite{klein:sel4:2009}. This verification explicitly assumes the existence of, amongst other things, a trustworthy assembler and compiler. % piton We are not the first to consider the total correctness of an assembler for a non-trivial assembly language. Perhaps the most impressive piece of work in this domain is the Piton stack~\cite{moore:piton:1996,moore:grand:2005}. Perhaps the most impressive piece of work in this domain is the Piton stack~\cite{moore:piton:1996}. This was a stack of verified components, written and verified in ACL2, ranging from a proprietary FM9001 microprocessor verified at the gate level, to assemblers and compilers for two high-level languages---a dialect of Lisp and $\mu$Gypsy~\cite{moore:grand:2005}. % jinja Klein and Nipkow consider a Java-like programming language, Jinja~\cite{klein:machine:2006,klein:machine:2010}. Klein and Nipkow consider a Java-like programming language, Jinja~\cite{klein:machine:2006}. They provide a compiler, virtual machine and operational semantics for the programming language and virtual machine, and prove that their compiler is semantics and type preserving.