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