Changeset 3248 for Deliverables/D4.4/report.tex
- Timestamp:
- May 1, 2013, 1:40:42 AM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.4/report.tex
r3222 r3248 128 128 The aim of WP4 is is to build the trusted version of the compiler back-end, 129 129 from the intermediate \textsf{RTLabs} language down to assembly. The development 130 is made in \textsf{matita}, and it allows the tr suted compiler to be extracted130 is made in \textsf{matita}, and it allows the trusted compiler to be extracted 131 131 to \textsf{OCaml}. 132 132 … … 143 143 starts to be able to meddle with return addresses that live in memory, the call structure 144 144 is no more guaranteed to be preserved after the high-level, structured 145 languages. This ishas little meaning as far as pure extensional semantic145 languages. This has little meaning as far as pure extensional semantic 146 146 preservation is required---after all, if the source language meddles with the 147 147 call structure there is no problem as long as the target language will follow.
Note: See TracChangeset
for help on using the changeset viewer.