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

Master Internship at Université d’Orléans, France

Reactive Synchronous Programming

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.

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.

During this internship, we will focus on the study of a purely functional approach of the synchronous reactive model. At first, the selected candidate will have to carry out a bibliographcal work on the subject. In a second step, we will focus on the design of a micro-language for which a formal semantics will be done in Coq [1]. This formalization will lead to the realization of a certified interpreter of the language. From an applied point of view the objective of the internship is to take a first step towards the proposition of a language of high-level programming for the Internet of Things.

The natural continuation of this internship will be the preparation of a PhD in computer science at the University of Orleans.

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: March 13th 2019

References

[1] The coq proof assistant. https://coq.inria.fr/.

[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.

Candidature : Par email adressé aux deux encadrants avant le 11 Janvier 2019.