From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTP id 19E265D5 for ; Fri, 22 Feb 2019 14:40:34 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.58,400,1544482800"; d="scan'208,217";a="370515025" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 22 Feb 2019 15:40:29 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id 93EDA825FD; Fri, 22 Feb 2019 15:40:29 +0100 (CET) Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 71C39825BD; Fri, 22 Feb 2019 15:40:03 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=frederic.dabrowski@univ-orleans.fr; spf=Pass smtp.mailfrom=frederic.dabrowski@univ-orleans.fr; spf=None smtp.helo=postmaster@sucre.univ-orleans.fr IronPort-PHdr: =?us-ascii?q?9a23=3AlUQWdhDC8y/XeoTFE8TwUyQJP3N1i/DPJgcQr6Af?= =?us-ascii?q?oPdwSP35p8WwAkXT6L1XgUPTWs2DsrQY07qQ6/iocFdDyK7JiGoFfp1IWk1Nou?= =?us-ascii?q?QttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZr?= =?us-ascii?q?KeTpAI7SiNm82/yv95HJbAhEmDmwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+?= =?us-ascii?q?NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjD?= =?us-ascii?q?QhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj?= =?us-ascii?q?8KOSMn/mHZisJ+j6xVrxyuqBN934HZe5uaOOZkc67HYd8XS2hMU8BMXCJBGIO8?= =?us-ascii?q?aI4PAvIBM+ZCtY7yukEJrQG/BQawHOzhxCVHiWTs3a093eUhCgLG3A09FN8Jvn?= =?us-ascii?q?TUtsv6O7oMXuCvzanH0S/PYO5M1jjm8ojIdR4goeqPXbJxasfR1E8vFwLbjlmJ?= =?us-ascii?q?rozlJTeV2foXvGid9OpsT+yvi3Q+pgx3vzOhyMAsiozTiYIUzFDJ7SR5wIAvJd?= =?us-ascii?q?25UkF3e9CkEIFWuiqHNIV2WtsvT3xstSs10LEKpJ+2cSoQxJkp2xLTcfiKfoeQ?= =?us-ascii?q?7h/hV+udOyl0iG9ldb6lmhq/8FasxvfzW8S21ltBszBLncPWtn8X0hze8siHRe?= =?us-ascii?q?V5/kemwTuPzB3T5f1eIU8qj6bbNpghwr8ulpYKtkTDBCv2l1vsg6+QbUUo4Oao?= =?us-ascii?q?6/7/brXnoJ+TKZN0hxnjPqkqlcGzG/k0PwkMUmSB9+mwyKfv8En2TblSi/05iK?= =?us-ascii?q?jZsJTUJcQBoa65BhdY0og56xmhEjipzs4YnXgbI15fZR2IlZPmO0vJIPH2Fve/?= =?us-ascii?q?gFWsnSx2x/DAP73hHIzBLn/ZkLflY7ly8UhcyBEpwdBR/ZJYEqsBL+7rWk/tqN?= =?us-ascii?q?zYCQc0PBCuzObiDNVxz4ceWWOUAq+FK67Sql+J5uc3I+aWfoMVuTD9K+Ik5/H0?= =?us-ascii?q?l3M5l0Udd7Gz3ZQLcHC4AuhmI0KBbHXwhdcBCH4GsRY6TOz3k1KPSiVTZna3X6?= =?us-ascii?q?Ik/D43EoOmDYHZRoCsmrONxim7HocFLlxBX1uLCDLjc5iOc/YKciObZMF71nQL?= =?us-ascii?q?WaLkSooJ2h208Q7/jbR9aqLI6zUVrtfq0t5y+uvYmDk29CdoFIKG3miWCXxsk2?= =?us-ascii?q?UOATI6weQ3qkt7wUqZy6V+iO1wEd1I++hESBk3L9jA0uE8DdS2EhnMdcqTSUq3?= =?us-ascii?q?atuhGjg9CNUrzJtGbEpnXdq6ijje2Su0RrAPmrqMDpg5t6vYx3XqYchnjz7N06?= =?us-ascii?q?w5jl0vXspIMyigi7Fk3wzSHJLS1UqXkLyleOId2jTM/SGN1y7GtUdeVwh7XL7t?= =?us-ascii?q?WXEEekbN68/+7ULPU7LrCLIpNRFEwNKDM7ZHL9HkyFtcTfHoNZLQeSb5kG61AV?= =?us-ascii?q?OMx6iQRIvsYWQUmivHTAAAmgUT9DCCNAY5LiOguH7TF3pzE1PxJkT29eR3rmj9?= =?us-ascii?q?QFVwhw6WKlNszbu70hEZn7mdTrUdxOEqoiAk/htunVo8xdPdPPaJrRBmY75fYJ?= =?us-ascii?q?tp7k1K2W/Dtgc7MpWqNad9nV0fWxlxvl2r0A9zB4xGio4ktiV5n0JJNauE3QYZ?= =?us-ascii?q?JHuj1pfqN+iPczigzFWUc6fTn2rm/pOT86YL5u4/rgy87hyvF1Rn9G9j3tBTyD?= =?us-ascii?q?2S/MeTVVZAYdfKSk8ysiNCifTCeCBkuNHJ03xydK6utjLL3clvCvF3kk/9Leca?= =?us-ascii?q?C7uNEUrJK+NfB8WqL7ZxyUO0ZQgJev1U9bBxONmievKAw+ilJrQ4kQ=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AFCwCrCHBch14ep8IaAUcDDg8BAQUBB?= =?us-ascii?q?wUBgWUCgQwBRoEWA4EAJ4NHQIh5jRCYI4FnKBABhEACg34aBwEENBIBAwEBAgE?= =?us-ascii?q?BAQEBEwEBAQoLCQgpIwyCOiKCbwMDDBdFBRwJOgEJAgJMCwcMBgIBAYMcAYF2j?= =?us-ascii?q?QyCepthgS8fhSWDXYEIBYxIVYFBgREngj2EcwkBEQIBPyaCQoJXAollEz5WhUO?= =?us-ascii?q?TCgcCgRuGI4Nvhy0fimeIKIJXh3eFUI4MN4EGcXRMgmwJgi2FEohaPD8BMYEFA?= =?us-ascii?q?QGPBAEB?= X-IPAS-Result: =?us-ascii?q?A0AFCwCrCHBch14ep8IaAUcDDg8BAQUBBwUBgWUCgQwBRoE?= =?us-ascii?q?WA4EAJ4NHQIh5jRCYI4FnKBABhEACg34aBwEENBIBAwEBAgEBAQEBEwEBAQoLC?= =?us-ascii?q?QgpIwyCOiKCbwMDDBdFBRwJOgEJAgJMCwcMBgIBAYMcAYF2jQyCepthgS8fhSW?= =?us-ascii?q?DXYEIBYxIVYFBgREngj2EcwkBEQIBPyaCQoJXAollEz5WhUOTCgcCgRuGI4Nvh?= =?us-ascii?q?y0fimeIKIJXh3eFUI4MN4EGcXRMgmwJgi2FEohaPD8BMYEFAQGPBAEB?= X-IronPort-AV: E=Sophos;i="5.58,400,1544482800"; d="scan'208,217";a="297023688" Received: from sucre.univ-orleans.fr ([194.167.30.94]) by mail3-smtp-sop.national.inria.fr with ESMTP; 22 Feb 2019 15:40:01 +0100 Received: from localhost (localhost [127.0.0.1]) by sucre.univ-orleans.fr (Postfix) with ESMTP id D811B7C181; Fri, 22 Feb 2019 15:39:58 +0100 (CET) Received: from sucre.univ-orleans.fr ([127.0.0.1]) by localhost (sucre.univ-orleans.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id Xt8+qpOjfgvE; Fri, 22 Feb 2019 15:39:58 +0100 (CET) Received: from smtps.univ-orleans.fr (smtpkerb1.univ-orleans.fr [194.167.30.60]) by sucre.univ-orleans.fr (Postfix) with ESMTP id C33157C17F; Fri, 22 Feb 2019 15:39:58 +0100 (CET) Received: from [192.168.1.39] (5dy45-1-78-215-162-47.fbx.proxad.net [78.215.162.47]) by smtps.univ-orleans.fr (Postfix) with ESMTPSA id C81451002E; Fri, 22 Feb 2019 15:40:00 +0100 (CET) To: coq-club@inria.fr, gdr-im@gdr-im.fr, types-announce@lists.seas.upenn.edu, concurrency@listserver.tue.nl, security@fosad.org, gdr.gpl@univ-grenoble-alpes.fr, compilation-news@lists.gforge.inria.fr, annonces@listes.societe-informatique-de-france.fr, caml-list@inria.fr, lamha.lifo@listes.univ-orleans.fr, gt-verif@gdr-im.fr References: From: =?UTF-8?Q?Fr=c3=a9d=c3=a9ric_Dabrowski?= Message-ID: Date: Fri, 22 Feb 2019 15:40:00 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.4.0 MIME-Version: 1.0 In-Reply-To: Content-Type: multipart/alternative; boundary="------------49198FF474D9DA4FA4F665A5" Content-Language: en-US X-Validation-by: frederic.dabrowski@univ-orleans.fr Subject: [Caml-list] =?UTF-8?Q?Master_Internship_in_computer_science_at_Un?= =?UTF-8?Q?iversit=C3=A9_d=E2=80=99Orl=C3=A9ans=2C_France?= Reply-To: =?UTF-8?Q?Fr=c3=a9d=c3=a9ric_Dabrowski?= X-Loop: caml-list@inria.fr X-Sequence: 17365 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: This is a multi-part message in MIME format. --------------49198FF474D9DA4FA4F665A5 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit 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. > --------------49198FF474D9DA4FA4F665A5 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: 8bit

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.

--------------49198FF474D9DA4FA4F665A5--