# Changeset 1365 for Deliverables/D4.2-4.3/reports

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

changed description of task in 4.2 report.

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

### Legend:

Unmodified
 r1364 The Grant Agreement states that Task T4.2, entitled Functional encoding in the Calculus of Constructions' has associated Deliverable D4.2, consisting of the following: \begin{quotation} 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. CIC 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. \end{quotation} This report details our implementation of this deliverable.