Hi I join also our current position :)
Title: Optional Static Types for Dynamic Languages
Context: Dynamically-typed languages cannot take advantage of static type information. In this context we would like to study the benefits of introducing static type annotations on library design, general robustness and tooling. The benefits will be at the level of robustness (bug identification), tools (IDE), and support for assembly/c generation in case of static compilation.
The Ph.D. grant is financed in the context of the Safe Python project. In this context the Ph.D. student will have to work in contact with the project partners and help in the context of some deliverables.
The student will:
- compare existing static subsets of dynamic languages; - formally define the semantics of RPython (this is one deliverables of the project); - analyze the benefits of static typing for existing Python and Pharo code; - explore type checking in presence of incomplete or inconsistent type annotations.
Some possible paths for the student:
- studying the existing python libraries and analyzing the "distance" to the RPython subset; - using PLT redex which is a domain-specific language to specify and debug the operational semantics; - using the abstract syntax tree of PyLint and use the Frama-C infrastructure; - building a Python parser based on PetitParser.
Since we are developing Pharo and that static type annotations is important to support C or assembly generation, we would like to apply the same techniques to Pharo through:
- building on top of existing work done in the context of the Gradual Types project of PLEIAD; - the development of some tools; - the analysis of existing libraries.
References
[1] D. Ancona, M. Ancona, A Cuni, and N. Matsakis. RPython: a Step Towards Reconciling Dynamically and Statically Typed OO Languages. In OOPSLA 2007 Proceedings and Companion, DLS'07: Proceedings of the 2007 Symposium on Dynamic Languages, pages 53-64. ACM, 2007. [2] A Visual Environment for Developing Context-Sensitive Term Rewriting Systems Jacob Matthews, Robert Bruce Findler, Matthew Flatt, and Matthias Felleisen [3] Felleisen,M.,Hieb,R.:The revised report on the syntactic theories of sequential control and state. (1992) 235â271
Skills and Profile:
The student must hold a Master's in Computer Science, control engineering, mathematics, scientific computation, or an equivalent diploma. Nationality is not taken into consideration. Knowledge in programming language design is required. Object-oriented programming with knowledge of Smalltalk and Python are a plus.
About Lille and INRIA
Lille is located in the North of France at the border to Belgium, one hour from Paris, 1h20 from London, 35 min from Brussels, by train.
French food, combined with belgian beer. RMoD: http://rmod.lille.inria.fr INRIA Lille: http://www.inria.fr/lille/ INRIA in General: http://www.inria.fr Lille: http://en.wikipedia.org/wiki/Lille http://wikitravel.org/en/Lille
Duration : 36 months â starting date of the contract : October 2012, 15th Salary: 1957.54 EUR the first two years and 2058.84 EUR the third year Monthly salary after taxes: around 1597.11 EUR the 1st two years and 1679.76 EUR the 3rd year (social security included). Possibility of French courses Help for housing Scientific Resident card and help for husband/wife visa
Additional Information Contact information: stephane.ducasse@inria.fr and marcus.denker@inria.fr