Changeset 1204


Ignore:
Timestamp:
Sep 10, 2011, 12:13:55 PM (8 years ago)
Author:
mulligan
Message:

small change

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r1203 r1204  
    778778Like CerCo, the CLI Stack compilers gave the cost of high-level instructions in processor cycles.
    779779The CLI Stack high-level languages ($\mu$Gypsy and Nqthm Lisp) and FM9001 microprocessor were not commercial products, but bespoke designs for the purpose of verification (see~\cite{moore:grand:2005}).
    780 This work has been continued by Hunt and Swords, verifying the Centaur Technologies Via Nano and Isaiah micoprocessors in ACL2~\cite{hunt:verifying:2010}.
     780This work has, however, been continued by Hunt and Swords, verifying the Centaur Technologies Via Nano and Isaiah micoprocessors in ACL2~\cite{hunt:verifying:2010}.
    781781
    782782The CompCert C compiler is extracted to O'Caml using Coq's code extraction facility.
Note: See TracChangeset for help on using the changeset viewer.