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