Changeset 2577 for Deliverables

Timestamp:

Jan 11, 2013, 5:00:57 PM (8 years ago)

Author:

tranquil

Message:

abstract of indexed labels talk

File:

• Deliverables/Dissemination/README (modified) (1 diff)

Deliverables/Dissemination/README

@@ -48 +48 @@
 
 Module:
-Targeting more advanced optimisations: indexed labelling (tentative title).
-Abstract (* To come (Bologna?)*)
+Targeting more advanced optimisations: indexed labelling.
+Abstract
+We present an extension to the labelling approach. The original approach looses
+preciseness when differences arise as to the cost of the same portion of code,
+whether due to code transformation such as loop optimisations or advanced
+architecture features (e.g. cache). We propose to address this weakness by
+formally indexing cost labels with the iterations of the containing loops they
+occur in. These indexes can be transformed during the compilation, and when
+lifted back to source code they produce dependent costs.
+The proposed changes have been implemented in CerCo's untrusted prototype
+compiler.
 
-Module: 
+Module:
 Certifying and reasoning on cost annotations of functional programs.
 Abstract