Rémi Bonnet

This is supposed to be a joint project with the semester project (directed by Philipp Haller). The idea is to find an extension of the work presented in http://lamp.epfl.ch/~phaller/uniqueness_types.pdf

This project consist in :

• writing an alternate typing system that doesn't require expose and localize constructs

(status : done)

• prove that all safeties guaranties provided by the system of the paper stay valid

(status : proof sketch finished, formalization in progress)

• exhibit an algorithm that is able to typecheck in polynomial time (and prove its validity)

(status : algorithm written, proof in progress)

• show that if we remove the expose & localize statements from a valid program, the new typing system still validates it

(status : done)

For the SAV part, i will try to more specifically show this (interesting) side result :

Currently, the current system is only able typechecks methods without loops that have parameter annotations. Although, if the algorithm knows the types of the method called inside the currently typechecked method, then it can find the “best possible” typing result. Thus, by iterating, it should be able to find the best typing result which is a fixed point of the submethod types → method type application. Of course, we need to find an order on functions types and prove monocity of the typing algorithm with respect to submethod types, and also that we are in a lattice (well, actually, we aren't, but there is workarounds) (status : lots of ideas with reasonable backup but nothing formalized or proven)

(current work : In progress)