Ignore:
Timestamp:
Oct 13, 2011, 11:30:36 AM (9 years ago)
Author:
mulligan
Message:

changed description of task in 4.2 report.

added outline and description of task to 4.3 report

File:
1 edited

Legend:

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

    r1364 r1365  
    114114The Grant Agreement states that Task T4.2, entitled `Functional encoding in the Calculus of Constructions' has associated Deliverable D4.2, consisting of the following:
    115115\begin{quotation}
    116 Executable Formal Semantics of back-end intermediate languages: This prototype is the formal counterpart of deliverable D2.1 for the back end side of the compiler and validates it.
     116CIC encoding: Back-end: Functional Specification in the internal language of the Proof Assistant (the Calculus of Inductive Construction) of the back end of the compiler. This unit is meant to be composable with the front-end of deliverable D3.2, to obtain a full working compiler for Milestone M2. A first validation of the design principles and implementation choices for the Untrusted Cost-annotating OCaml Compiler D2.2 is achieved and reported in the deliverable, possibly triggering updates of the Untrusted Cost-annotating OCaml Compiler sources.
    117117\end{quotation}
    118118This report details our implementation of this deliverable.
Note: See TracChangeset for help on using the changeset viewer.