Laboratoire d'informatique de l'École polytechnique


Talk by Raphaëlle Crubillé: «On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem»

Speaker: Raphaëlle Crubillé
Location: Room Philippe Flajolet, Alan Turing building
Date: Tue, 21 Jan 2020, 14:00-15:00

The next Comète seminar will take place on Tuesday, January 21st at 2pm in Saclay Salle Philippe Flajolet (LIX - Alan Turing building, École Polytechnique). Raphaëlle Crubillé, post-doc on formal methods for probabilistic programs at IMDEA, will talk about “On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem”.

Abstract: Logical relations are one of the most powerful techniques in the theory of programming languages, and have been used extensively for proving properties of a variety of higher-order calculi. However, there are properties that cannot be immediately proved by means of log- ical relations, for instance program continuity and differentiability in higher-order languages extended with real-valued functions. Informally, the problem stems from the fact that these properties are naturally expressed on terms of non-ground type (or, equivalently, on open terms of base type), and there is no apparent good definition for a base case (i.e. for closed terms of ground types). To overcome this issue, we introduce a generalization of the concept of a logical relation, which we dub open logical relation, and prove that it can be fruitfully applied in several contexts in which the property of interest is about expressions of first-order type. Our setting is a simply-typed λ-calculus enriched with real numbers and real-valued first-order functions from a given set, such as the one of continuous or differentiable functions. We first prove a containment theorem stating that for any such a collection of functions including projection functions and closed under function composition, any well-typed term of first-order type denotes a function belonging to that collection. Then, we show by way of open logical relations the correctness of the core of a recently published algorithm for forward automatic differentiation. Finally, we define a refinement-based type system for local continuity in an extension of our calculus with conditionals, and prove the soundness of the type system using open logical relations.

Talk by Qi Fan: «Multi-Objective Task Scheduling in Mobile Cloud Environments»

Speaker: Qi Fan
Location: Room Thomas Flowers, Alan Turing building
Date: Fri, 17 Jan 2020, 11:00-12:00

Qi Fan, a new PhD student in the Cedar team, will present her published work at IEEE Access, January 17th at 11am in Thomas Flowers room of Turing Building.

Abstract: The technology of the mobile cloud computing aims to extend the resource capacity and computing capability of mobile devices. It is convenient for mobile users to obtain computing resources according to their demands. In this environment, a set of tasks generated by mobile devices could be scheduled to the proper resource providers in terms of the requirements of various mobile users. However, when the number of tasks and service providers increases, computing cost rises as well. In addition, the total completion time could be influenced by the selection of cloud resources with various processing capability. Thus, it is quite significant to consider how to optimize the task scheduling while satisfying different demands of users.

Talk by Valeria Vignudelli: «A powerset construction for nondeterministic and probabilistic systems»

Speaker: Valeria Vignudelli
Location: Salle Philippe Flajolet, Alan Turing building
Date: Thu, 16 Jan 2020, 14:00-15:00

The next Comète seminar will take place on Thursday, January 20th at 2pm in Salle Philippe Flajolet (LIX - Alan Turing building, École Polytechnique). Valeria Vignudelli, postdoctoral researcher at ENS Lyon, will talk about “A powerset construction for nondeterministic and probabilistic systems”.

Abstract: The powerset construction provides a method for establishing trace equivalence of nondeterministic transition systems. The definition of trace equivalence requires to directly compare the traces that can be performed by two systems. The main idea of the powerset construction is that trace equivalence can be recovered alternatively by first determinizing the systems, i.e., transforming them into deterministic systems, and then by recovering trace equivalence on the original systems as bisimulation equivalence on the determinized systems. On transition systems combining nondeterministic and probabilistic choices, the definition of trace equivalence has itself some underlying intricacies. In this talk, I will show how a powerset-like construction can be defined for nondeterministic and probabilistic labelled transition systems. The construction we propose fits a generalization of the powerset construction based on coalgebra, an abstract framework to study transition system semantics. This allows us to recover many interesting properties of trace equivalence for nondeterministic and probabilistic transition systems. This talk is based on joint work with Filippo Bonchi and Ana Sokolova, available at