sorry for the repost, it seems the attached pdf in the previous mail was corrupted

Fully-funded 3-years Phd scolarship at Université d’Orléans, France

Reactive Synchronous Programming : Semantics and applications to IOT

Advisors : W. Bousdira, F. Dabrowski

Research Team : LIFO/LMV

Theme : Concurrency semantics

Laboratory

The Laboratory of Fundamental Computer Science of Orleans (LIFO, EA 4022) is a laboratory of the University of Orleans and INSA Center-Val de Loire. Research conducted at LIFO ranges from algorithmics to natural language processing, from automatic learning to massive parallel computing, from verification and certification to system security.

Team

The aim of the LMV team is to improve the understanding of safety and security of computer systems. From "partial order" logic to usual programming languages, the team members work on these questions at different levels of abstraction.

Funding : Fully-funded 3-years scholarship from the French Ministry for Education and Research

Subject : The reactive synchronous programming model [9] is a relaxation of the ESTEREL model [6]. In the latter, a collection of processes progress by successive phases of global synchronization (“ clock ticks ”) and communicate by events. At each instant (a phase between two ticks) each component reacts to the presence / absence of events. While the ESTEREL model solves the problem of causality posed by the instantaneous reaction to absence by restricting the expressivity of the language, the synchronous reactive model delays reaction to absence (the absence of a signal can not be decided before the end of an instant). Several works have focused on the semantic study of languages derived from this model [2, 5, 3] and on the analysis of the properties of such programs [4, 12]. Other works have successfully studied the possibility of using this programming model in the context of mobility [7]. Implementations of this programming model have been proposed for several languages like C, Scheme, Ocaml and Java [8, 13, 10, 11]. In [9], the authors propose a version of this model supporting strong security properties.

In this thesis, we will focus on a purely functional approach of the synchronous reactive model (existing languages have imperative features). As a first step, the selected candidate will have to carry out the semantic study of a programming language based on this model. An obvious starting point will be the article [1]. In a second step, the definition of desirable properties for the programs of this language will lead to the implementation of verification tools dedicated to these properties. The different developments will have to be formalized using the Coq proof assistant. Depending on the results obtained, the automatic extraction of code from the latter may be considered.

From an applied point of view the objective of this thesis is to propose a high-level programming language for the Internet Of Objects. In particular, such a language should make it possible to deploy a program, conceived in a global manner, on the different actors of a communicating scenario.

Application

We are happy to provide more details to potential applicants. Requests for additional information regarding the project’s content/motivation, other informal enquiries, and formal applications can be sent to Frédéric Dabrowski (frederic.dabrowski@univ-orleans.fr). Formal applications must include:

• A motivation letter

• A cv, including a list of courses with grades

• A copy of the master’s thesis (if already available)

• The name of at least one scientist able and willing to provide a reference

Deadline for applications: May 15th 2019

References

[1] M. Abadi and G. Plotkin. A model of cooperative threads. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’09, pages 29–40, New York, NY, USA, 2009. ACM.

[2] R. M. Amadio. The sl synchronous language, revisited. The Journal of Logic and Algebraic Programming, 70(2):121 – 150, 2007. Algebraic Process Calculi: The First Twenty Five Years and Beyond.

[3] R. M. Amadio. A synchronous pi-calculus. Inf. Comput., 205(9):1470–1490, 2007.

[4] R. M. Amadio and F. Dabrowski. Feasible reactivity in a synchronous pi-calculus. In Proceedings of the 9th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, PPDP ’07, pages 221–230, New York, NY, USA, 2007. ACM.

[5] R. M. Amadio and M. Dogguy. On affine usages in signal-based communication. CoRR, abs/0804.1729, 2008.

[6] G. Berry and G. Gonthier. The esterel synchronous programming language: design, semantics, implementation. Science of Computer Programming, 19(2):87 – 152, 1992.

[7] G. Boudol. Ulm: A core programming model for global computing. In D. Schmidt, editor, Programming Languages and Systems, pages 234–248, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg.

[8] F. Boussinot. Fairthreads: mixing cooperative and preemptive threads in c. Concurrency and Computation: Practice and Experience, 18:445–469, 2006.

[9] F. Boussinot and F. Dabrowski. Safe Reactive Programming: the FunLoft Proposal. In MULTIPROG’08, pages –, Sweden, 2008.

[10] F. Boussinot and J.-F. Susini. The sugarcubes tool box: A reactive java framework. Softw. Pract. Exper., 28(14):1531–1550, Dec. 1998.

[11] L. Mandel and C. Pasteur. Réactivité des systèmes coopératifs : le cas de ReactiveML. In D. Pous and C. Tasson, editors, JFLA - Journées francophones des langages applicatifs, Aussois, France, Feb. 2013. Damien Pous and Christine Tasson.

[12] A. A. Matos, G. Boudol, and I. Castellani. Typing noninterference for reactive programs. The Journal of Logic and Algebraic Programming, 72(2):124 – 156, 2007. Programming Language Interference and Dependence.

[13] M. Serrano, F. Boussinot, and B. Serpette. Scheme fair threads. In Proceedings of the 6th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, PPDP ’04, pages 203–214, New York, NY, USA, 2004. ACM.