Changeset 1366


Ignore:
Timestamp:
Oct 13, 2011, 11:33:55 AM (8 years ago)
Author:
mulligan
Message:

added connections with other languages to d4.3 report, also fixed mistaken attribution of d2.2 to d2.1

Location:
Deliverables/D4.2-4.3/reports
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.2-4.3/reports/D4-2.tex

    r1365 r1366  
    124124\label{subsect.connections.with.other.deliverables}
    125125
    126 Deliverable D4.2 enjoys a close relationship with three other deliverables, namely deliverables D2.1, D4.3 and D4.4.
    127 
    128 Deliverable D2.1, the O'Caml implementation of a cost preserving compiler for a large subset of the C programming language, is the basis upon which we have implemented the current deliverable.
     126Deliverable D4.2 enjoys a close relationship with three other deliverables, namely deliverables D2.2, D4.3 and D4.4.
     127
     128Deliverable D2.2, the O'Caml implementation of a cost preserving compiler for a large subset of the C programming language, is the basis upon which we have implemented the current deliverable.
    129129In particular, the architecture of the compiler, its intermediate languages, and the overall implementation of the Matita encodings has been taken from the O'Caml compiler.
    130130Any variations from the O'Caml design are due to bugs identified in the prototype compiler during the Matita implementation, our identification of code that can be abstracted and made generic, or our use of Matita's much stronger type system to enforce invariants through the use of dependent types.
  • Deliverables/D4.2-4.3/reports/D4-3.tex

    r1365 r1366  
    121121\subsection{Connections with other deliverables}
    122122\label{subsect.connections.with.other.deliverables}
     123
     124Deliverable D4.3 enjoys a close relationship with three other deliverables, namely deliverables D2.2, D4.3 and D4.4.
     125
     126Deliverable D2.2, the O'Caml implementation of a cost preserving compiler for a large subset of the C programming language, is the basis upon which we have implemented the current deliverable.
     127In particular, the architecture of the compiler, its intermediate languages and their semantics, and the overall implementation of the Matita encodings has been taken from the O'Caml compiler.
     128Any variations from the O'Caml design are due to bugs identified in the prototype compiler during the Matita implementation, our identification of code that can be abstracted and made generic, or our use of Matita's much stronger type system to enforce invariants through the use of dependent types.
     129
     130Deliverable D4.2 can be seen as a `sister' deliverable to the deliverable reported on herein.
     131In particular, where this deliverable reports on the encoding in the Calculus of Constructions of the backend semantics, D4.2 is the encoding in the Calculus of Constructions of the mutual translations of those languages.
     132As a result, a substantial amount of Matita code is shared between the two deliverables.
     133
     134Deliverable D4.4, the backend correctness proofs, is the immediate successor of this deliverable.
    123135
    124136%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
Note: See TracChangeset for help on using the changeset viewer.