Guillaume Claret

M2 internship

March to July 2011

With Yann Régis-Gianas and Roberto Amadio.

Place

23 avenue d'Italie - 75013 Paris

Done

TODO

  • define and implement a MiniML language with region based memory management and instrumentation tags

Timeline

Week 14

  • …
TODO
  • export assertions to Pangolin with the monadic transformation
  • try to export to the Who program checker
  • make a real example

Week 13

  • begining of the Hoare project (tool to manipulate Hoare assertions on a functional program with cost annotations)

Week 12

  • monadic transformation to express traces as values, semantics correction
  • usage of pre/post labels mentioned
TODO
  • proove full semantics equivalence for monadic transformation
  • define a light version of Hoare logic for functional languages
  • implement a light version of Pangolin

Week 11

Week 10

  • standardization of languages uzed in the proof of correctness of the compiler
TODO
  • prove the correctness of execution time computation with label on RTLabs
  • prove other compilation passes, like explicit closure (just after hoisting), RTLabs generation, …
  • understand this kind of paper : Linear Dependent Types and Relative Completeness

Week 9

  • CPS proof with exceptions finished
  • proof of the closure conversion (actually only hoisting) with labels
Readings

Week 8

  • LaTeX version of the proof of last week for CPS conversion
  • look at the Coq proof of Chlipala
  • tests of Coq formalization of lambda-calculus
Readings

Week 7

  • draft of a proof of the CPS conversion with labels from big steps to small steps semantics (with environments)

Week 6

  • semantics of MicroML used to define the ones of MiniML, Cps and Closure
  • proof of the CPS conversion with exceptions and small steps semantics (without labels)

Week 5

  • let construct in MicroML
  • How to detect raise-free expressions to remove some application labels ?
  • What Hoare logic on functionnal programs with exceptions looks like ?
Readings

Week 4

  • sum types and exceptions
  • labels on applications are back because exceptions can stop the execution at any point

Week 3

  • labels added to the compiler for time evaluation, parser for nice examples, fixpoint operator

Week 2

  • writing of a compiler from MiniML to abstract Register Transfer Language, with an interpreter for each intermediate language
Readings

Week 1

  • introduction to the subject
Readings