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

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

[Frédéric Dabrowski]

[-- Attachment #1: Type: text/plain, Size: 6403 bytes --]

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.


[-- Attachment #2: Type: text/html, Size: 24021 bytes --]

[Caml-list] Master Internship in computer science at Université d’Orléans, France

[Frédéric Dabrowski]

[-- Attachment #1: Type: text/plain, Size: 6031 bytes --]

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

[-- Attachment #2: Type: text/html, Size: 22375 bytes --]