Changeset 563 for Deliverables
- Timestamp:
- Feb 17, 2011, 4:45:17 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/ITP-Paper/itp-2011.tex
r562 r563 754 754 In contrast, the ARM instruction set and memory model is relatively uniform, simplifying any formalisation considerably. 755 755 756 Perhaps the closest project to CerCo is CompCert~\cite{leroy:formal :2009,leroy:formally:2009}.757 CompCert concerns the certification of a n ARM compiler and includes a formalisation in Coq of a subset of ARM.756 Perhaps the closest project to CerCo is CompCert~\cite{leroy:formally:2009}. 757 CompCert concerns the certification of a C compiler and includes a formalisation in Coq of a subset of PowerPC. 758 758 Coq and Matita essentially share the same logic. 759 759
Note: See TracChangeset
for help on using the changeset viewer.