Languages, Compilation, and Semantics LIP Seminar
13th Edition, 2020, new date to be decided (was April 15th)
Information
The seminar will be hold at Room Condorcet, 1 place de l'Italie (Monod site). The meeting is open to all members of FIL, ie the labs LIP, LIRIS, and CITI.
Program
9h159h30  Welcome  
9h3010h30  Zsolt Istvan  Even though there has been a large number of proposals to accelerate databases using specialized hardware, often the opinion of the community is pessimistic: the performance and energy efficiency benefits of specialization are seen to be outweighed by the limitations of the proposed solutions and the additional complexity of including specialized hardware, such as field programmable gate arrays (FPGAs),
in servers. Recently, however, as an effect of stagnating CPU performance, server architectures
started to incorporate various programmable hardware components, ranging from smart network
interface cards, through SSDs with offloading capabilities, to nearCPU accelerators. This availability of
heterogeneous hardware brings new opportunities to databases and this talk makes the case that there
is cause for optimism. In the light of a shifting hardware landscape and emerging analytics workloads, it is
time to revisit our stance on hardware acceleration and to start exploring emerging research questions
around programmability and integration.
Bio: Zsolt Istvan is an Assistant Research Professor at the IMDEA Software Institute in Madrid, Spain. In his research he explores how specialized hardware can be used to make dataintensive systems more efficient.  
10h3011h00  Coffee break  
11h0012h00  Reiner Hähnle  We propose a new static software analysis principle called Abstract Execution, generalizing Symbolic Execution: While the latter analyzes all possible execution paths of a specific program, Abstract Execution analyzes a partially unspecified program by permitting abstract symbols representing unknown contexts. There is a wide range of applications of Abstract Execution, especially for verifying relational properties of schematic programs. We implemented Abstract Execution in a deductive verification framework and proved correctness of eight wellknown statementlevel refactoring rules, including two with loops. For each refactoring we characterize the preconditions that make it semanticspreserving. Most preconditions were not mentioned in the literature. 
12th Edition, 2020, new date to be decided (was April 9th)
Information
The seminar will be hold at Room D8 003 (Buisson Site), ENS Lyon. The meeting is open to all members of FIL, ie the labs LIP, LIRIS, and CITI.
Program
9h009h15  Welcome  
9h3010h30  Damien Pous (LIP)  I will first give a brief description of proof assistants: computer
programs that make it possible to write and check proofs, and to
exploit certified algorithms for some laborious subproofs.
Then I will spend most of the talk showing that graphs and tools from graph theory can be used to characterise certain equational theories, and to obtain decision procedures for some of them. There, a crucial point is to be able to characterise subclasses of graphs of treewidth at most two. We formalised some of these ideas in the Coq proof assistant with C. Doczkal, which first required developing a general purpose library for graph theory (see the talk in the afternoon). We plan to pursue this effort in the future: not only this helps us in our daily research using graphs for equational theories, but this also opens the way to the formalisation of challenging results in graph theory. 
10h3010h45  coffee break  
10h4511h45  Nicolas Trotignon (LIP)  The goal of this talk is to survey a classical method to prove theorems that describe the structure of graph classes. We will see several examples, such as the seminal theorem of Wagner on planar graphs from 1937 and the Strong perfect graph theorem from 2002. I will try to convince the audience that formal proofs are potentially interesting in this field, even if it not much used so far. 
11h4513h30  lunch  
13h3014h30  Jan Goedgebeur (Ghent University, Belgium)  Computers are often used in combinatorics to determine if combinatorial objects with given structural or extremal properties exist as these existence problems are often too complex to solve by hand. This is done by designing and implementing generation algorithms which construct combinatorial objects from a given class (typically avoiding the generation of isomorphic copies) and analysing the resulting graphs.
In this talk we will give an introduction to the exhaustive isomorphismfree generation of graphs. We will also give concrete examples of how this has helped to gain new insights and solve problems in mathematics and chemistry. Applications in mathematics include the generation of cubic graphs and snarks. We will present a new algorithm for the efficient generation of all nonisomorphic cubic graphs and show how this algorithm can be extended to generate snarks efficiently. A snark is a cyclically 4edgeconnected cubic graph with chromatic index 4. Snarks are of interest since for a lot of conjectures it can be proven that if the conjecture is false, the smallest possible counterexamples will be snarks. Our algorithm enabled us to generate all snarks up to 36 vertices, which was impossible with previous methods. This new list of snarks allowed us to find counterexamples to several published open conjectures. An application of graph enumeration in chemistry is the generation of the Nobel Prize winning fullerenes (cubic plane graphs where all faces are pentagons or hexagons). We will sketch a new algorithm for the generation of all nonisomorphic fullerenes. Our implementation of this algorithm allowed us to generate all fullerenes up to 400 vertices, which enabled us to prove that the smallest counterexample to the spiral conjecture has 380 vertices. This talk is based on joint work with Gunnar Brinkmann (Ghent University) and Brendan McKay (Australian National University). 
14h3014h45  coffee break  
14h4515h45  Christian Doczkal (Inria/Marelle)  Over the last couple of years we have developed a library of graph theory results in the interactive theorem prover Coq. This was motivated by the wish to formalize recent results on axiomatizations of graph isomorphism for treewidthtwo graphs. Given the lack of a generalpurpose graph theory library for Coq when we started our project, our second goal, right from the start, was to improve upon the state of the art in formalized graph theory by building a reusable library.
In my talk, I will report on our experience building the library, highlighting key design choices, selected results, and some directions for future extensions. This talk is based on joint work with Damien Pous. 
11th Edition, 2019, September 19th
Information
The seminar will be hold at Room B2 (4th floor, GN1 North), Monod Site, ENS Lyon. The meeting is open to all members of FIL, ie the labs LIP, LIRIS, and CITI.
Program
9h009h30  Welcome  
9h3010h30  Radu Mateescu (CONVECS team, Inria)  For analyzing the behaviour of concurrent valuepassing systems,
classical temporal logics must be extended with datahandling primitives.
Since the early days of formal verification, many such extensions were
proposed, both in the linear/branching time and the state/action based
settings. We present MCL (Model Checking Language), an extension of
the alternationfree modal mucalculus with datahandling features,
generalized regular expressions over transition sequences, and fairness
operators expressed using omegaregular expressions. MCL was designed
for a versatile and succinct formulation of temporal properties interpreted
on labeled transition systems (LTSs) containing data values, i.e.,
statetransition graphs modeling the behaviour of concurrent systems.
We illustrate the usage of MCL by means of classical examples of properties
(safety, liveness, and fairness) and discuss its expressiveness and
model checking complexity. We also briefly describe the implementation
of MCL provided by the EVALUATOR model checker of the CADP verification
toolbox, which evaluates an MCL formula on an LTS on the fly and produces
diagnostics (counterexamples and witnesses). Finally, we illustrate the
recent extension of MCL with a probabilistic operator, which computes
on the fly the probability measure of a transition sequence in a
probabilistic transition system (PTS). Combined with datahandling features,
this probabilistic operator enables the quantitative analysis of
sequences having peak cost values (e.g., number of operations, energy
consumption, etc.). 
10h3011h00  Coffee break  
11h0012h00  David Monniaux (Verimag)  This is a joint work with Cyril Six and Sylvain Boulmé.
CompCert (compcert.inria.fr) is a compiler for the C language with a machinechecked proof of correctness: if it succeeds in compiling a program, then the semantics of the assembly code should match that of the source code. This is ensured by giving semantics to all intermediate languages, and proofs that all transformations preserve the semantics. It is mainly developed in Coq. Extending CompCert to a new architecture is not so hard, albeit tedious, assuming that architecture is sufficiently similar to those already supported. We did so for the upcoming Kalray MPPA3 processor. CompCert however had no optimization pass for instruction scheduling — that is, reordering instruction to exploit instructionlevel parallelism (e.g. posting memory reads sufficiently in advance before using their results, so as to avoid stalling waiting for the read value). This is not much important on highly outoforder processors such as x86, but is of great importance on inorder processors. MPPA3 is a VLIW (very large instruction word) inorder processor, meaning that the compiler can specify multiple instructions to be executed at the same cycle, according to certain wellformedness rules. We designed a highly modular and parametric system for scheduling instructions in the backend, after register allocation. This system is composed of a transformation pass, itself calling a scheduler among a choice of several, and a checker, verifying that the semantics of the results of the transformation matches that of the input. We can also add extra transformation passes to implement other transformations (in our case, coalescing of multipleword reads and writes). Only the checker needs to be implemented in Coq proved correct; the transformation phases and schedulers do not (in fact, one of the schedulers calls an external solver). 
10th Edition, 2019, March 21st
Information
The seminar will be hold at amphi G, Monod Site, ENS Lyon. The meeting is open to all members of FIL, ie the labs LIP, LIRIS, and CITI.
Program
9h009h30  Welcome  
9h3010h30  Bruno Guillon (Cristal) 
When dealing with large graphs, classical algorithms for finding paths
such as Dijkstra's Algorithm are unsuitable, because they require to
perform too many disk accesses. To avoid the cost of this expensive
accesses, while keeping a data structure of size quasilinear in the
size of the graph, we propose to guide the path search with a distance
oracle, obtained from a topological embedding of the graph.
I will present fresh experimental research on this topic, in which we
obtain graph embeddings using learning algorithms from natural
language processing. On some graphs, such as the graph of publications
of DBLP, our topologicallyguided path search allows us to visit a
small portion of the graph only, in average.
This is joint work with Charles Paperman.

10h3011h00  Coffee break  
11h0011h45  Éric Ruten (LIG)  Field Programmable Gate Array (FPGA) architectures are suitable hardware platforms for systems that need high performance and flexibility, because they support dynamic partial reconfiguration (DPR) to implement adaptive hardware algorithms e.g., for performance or energy efficiency. They are used for example in embedded systems such as UAV, e.g. for video processing. It is a challenge to design Autonomic Managers for such highly dynamic systems, taking into account the combinatorial design space of configurations and criteria and policies to decide on whether to reconfigure, and what next configuration to choose. In this paper, we propose a Domain Specific Language (DSL) called CtrlDPR, allowing designers to easily generate Autonomic Managers. They can describe their system and their management strategies, in terms of the entities composing the system : tasks, versions, applications, ressources, policies. The DSL relies on a behavioural modelling of these entities, targeted at the design of autonomic managers to control the reconfigurations in such a way as to enforce given policies and strategies. The models we use involve automata to describe the state space of configurations, and the transitions representing reconfigurations; they also involve discrete control techniques exploiting such models in order to obtain a correct runtime manager. These modelbased control techniques are embedded in a compiler, connected to a reactive language and discrete controller synthesis tool, which enables to generate a C implementation of the controller enforcing the management strategies. We apply our DSL for the management of a video application on a UAV. 
11h4512h30  Thierry Gautier (LIP)  OpenMP (http://www.openmp.org) est un standard de facto qui est piloté par l’ARB (Architecture Review Board) composé de la plupart des grands constructeurs en HPC ainsi que par certains représentants universitaires. L’objectif d’OpenMP est d’offrir un ensemble de directives pour annoter du code séquentiel afin d'exploiter tous les niveaux de parallélisme qui sont offerts par les matériels, i.e. multicœurs, unités vectorielles et accélérateurs. Dans cette présentation nous nous attacherons à repositionner les évolutions actuelles de la norme 4.x entre son passé (pré 3.0) et son futur (5.0) en s’intéressant plus particulièrement au modèle de tâches.
Nous présenterons la manière dont sont définies les tâches et leurs dépendances dans le modèle OpenMP. Nous verrons qu'un tel programme OpenMP est fonctionnellement portable mais que l'obtention des performances doit aussi prendre en compte l'implementation à disposition. Nous illustrerons sur quelques exemples typiques en HPC l'impact de quelques runtimes (GCC, ICC/LLVM, …) sur les performances dont certains choix d'implémentation restentcritiquables. 
9th Edition, 2018, December 18th
Information
The seminar will be hold at Amphi E (ground floor), Monod Site, ENS Lyon. The meeting is open to all members of FIL, ie the labs LIP, LIRIS, and CITI.
Program
9h009h30  Welcome  
9h3010h30  Claire Maiza (Verimag)  In this talk, we present a survey on multicore timing analyses including delays due to interferences (shared memory, shared bus). We show that interference analysis is possible (scalability and precision). We illustrate this point with our interference analysis where the delay is integrated into schedulability analysis. We show that applying this analysis to a real platform (Kalray MPPA2) comes with a necessary smart software implementation and hardware configuration. 
10h3011h00  Coffee break  
11h0011h45  Hélène Coullon (LS2N)  With the emergence of largescale virtualized distributed infrastructures, such as Cloud, Fog and Edge computing, for instance, the automation of the deployment of distributed software is of great importance for IT administrators and developers. While many production tools already help developers automate their deployment tasks, academic research is interested in safe and verified modeling to ensure the correct behavior of a software configuration or reconfiguration. In this talk I will present Madeus, a formal component model for the deployment of distributed software that enhances the efficiency of deployment. Madeus puts forward more concurrency than other deployment models. This implies a greater complexity and a greater propensity for error. Hence, I will also introduce ongoing work regarding the verification of properties on Madeus deployments by model checking. Finally, I will rapidly present ongoing work regarding the extension of Madeus to dynamic software reconfiguration. 
11h4512h30  Colin Riba (LIP)  This talk surveys a CurryHoward perspective on Rabin's Tree Theorem, the decidability of Monadic SecondOrder Logic (MSO) on infinite trees.
Rabin's Tree Theorem proceeds by effective translations of MSOformulae to tree automata. We show that the operations on automata used in these translations can be organized in a deduction system based on intuitionistic linear logic (ILL). We propose a computational interpretation of this deduction system along the lines of the CurryHoward proofsasprograms correspondence. This interpretation, relying on the usual technology of game semantics, maps proofs to strategies in twoplayer games generalizing usual acceptance games of tree automata. 
8th Edition, 2018, October 4th
Information
The seminar will be hold at Room 003, Site Buisson, ENS Lyon. The meeting is open to all members of the labs LIP, LIRIS, and CITI.
Program
9h009h30  Welcome  
9h3010h30  Simone Martini (U. Bologne/Collegium de Lyon 20182019)  A Conceptual History of Programming Languages aims to be an organic tale of how some of the notions present in programming languages entered the field, how their semantics has been modified during the years, which linguistic mechanisms were proposed to “name” those concepts in specific languages. This evolution happened in dialogue and under the influence of important areas of mathematics, which, at some point across the sixties and the seventies, were identified with mathematical logic (and prooftheory in particular). Contrary to most folklore, however, the explicit recognition of the influence of mathematical logic on programming language design is not something that happens since the beginning. Moreover, concepts of the same name (e.g. types) have slightly different meanings in the two fields. I will describe this phenomenon for the notion of (data) type, starting with the fifties (Fortran and Algol), and arriving to the early eighties (abstract data types and objects oriented languages). 
10h3011h00  
11h0011h45  Emmanuel Coquery (U. LyonI/LIRIS)  Views are named queries in databases. They can be used either for storing the result of costly queries in tables, this is called materialized views. They can also be used to restrict access to data, by allowing users to query only views and forbidding direct access to tables. We call such views « access control views ». We consider the problem of, given a set of access control views on tables and a set of materialized views on the same tables, to devise a set of access control view to protect the materialized views. This problem boils down to identify the information accessible from both sets of views. We give an overview of a sound but incomplete algorithm for the case where views are restricted to conjunctive queries. 
11h4512h30  Damiano Mazza (CNRS/LIPN)  The CookLevin theorem (the statement that SAT is NPcomplete) is a
fundamental result of complexity theory. We will give a proof of this
theorem entirely based on the properties of a certain type system for a
simple Turingcomplete programming language. Such a type system arises
from very general considerations, formalized in the language of category
theory, relating types and program approximations. 
7th Edition, 2018, July, 5th
Information
The seminar will be hold at “Salle des Thèses”, ENS Lyon, Site Monod, Batiment MGN1, ENS Lyon, Monod site. The meeting is open to all members of the labs LIP, LIRIS, and CITI.
Program
Click on title for abstract.
9h009h30  Welcome  
9h3010h30  Nicolas Halbwachs (Verimag)  This is a joint work with Rémy Boutonnet.
Program analysis by abstract interpretation using relational abstract domains — like polyhedra or octagons — easily extends from state analysis (construction of reachable states) to relational analysis (construction of inputoutput relations). In this talk, we exploit this extension to enable interprocedural program analysis, by constructing relational summaries of procedures. In order to improve the accuracy of procedure summaries, we propose a method to refine them into disjunctions of relations, these disjunctions being directed by preconditions on input parameters.  
10h3011h00  Coffee break  
11h0011h45  Matthieu Moy (LIP) 
Simple, singlecore processors have been the main execution platform
for critical realtime software for years. Such software can be
handwritten in imperative languages, but code generation from
higherlevel languages such as the synchronous dataflow SCADE
(industrial version of the Lustre language) are also used in
production today.
Singlecore processors are reaching their limits. Performance, or energy efficiency constraints are leading the industry towards multicore or manycore including for critical systems. These architectures raise new major challenges for timing analysis. In this talk, we present a code generation flow from SCADE that produces parallel and yet predictable code for Kalray MPPA architecture. The code generation scheme is designed together with a timing analysis that take into account interference between cores when they access the local memory. This work was performed as part of the CAPACITES project: http://capacites.minalogic.net/  
11h4512h30  Pierre Clairambault (LIP) 
HigherOrder ModelChecking (HOMC) has recently emerged as an approach
to automated verification of higherorder programs, prompted by Ong's
2006 result that Monadic Second Order Logic (MSO) is decidable on
infinite trees generated by HigherOrder Recursion Schemes (HORS). It is
under active development, with implementations reporting encouraging
results despite an awful theoretical worst case complexity.
In principle, HOMC algorithms work by reduction to Ong's theorem. In practice, this often involves CPS translations which are costly in terms of complexity, and so as to get tight complexity people have instead reproved variations of Ong's theorem for extensions of HORS (with data, or callbyvalue) and drastically restricted fragments of MSO. In this talk, I will introduce Linear HORS (LHORS), an extension of HORS with additional type constructors imported from Linear Logic. Data and callbyvalue evaluation admit a finer translation to LHORS exploiting the idea of linearlyused continuations. Moreover LHORS enjoy a decidable modelchecking problem, whose complexity essentially ignores linear types. In this way we recover and extend several developments that were originally proved independently of Ong's theorem. This is joint work with Andrzej Murawski and Charles Grellois, presented at POPL'18. 
6th Edition, 2018, April, 26th
Information
The seminar will be hold at the room at 1 place de l'école, ENS Lyon, Monod site. The meeting is open to all members of the labs LIP, LIRIS, and CITI.
Program
Click on title for abstract.
9h009h30  Welcome  
9h3010h30  Warwick Tucker (Uppsala University & LIP)  In this talk we will discuss some powerful techniques from the field of computeraided proofs. The methods we will present are all based on setvalued mathematics (interval analysis) which is wellsuited for computational proofs where the underlying problem is continuous rather than discrete. We will also talk about some concrete mathematical problems that we are currently trying to solve using the abovementioned methods.  
10h3011h00  Coffee break  
11h0011h45  Ludovic Henrio (I3S) 
Active objects is a programming paradigm strongly inspired from actors. In this talk, I will first present the active object programming model, and the different languages that implement it.
In the Scale team we develop one particular active object language: the ASP model, and its reference implementation: ProActive.
This will allow me to show how active objects can be used to implement software components, and how we extended the model to support local multithreading. I will also illustrate how this model is efficient and expressive.
Finally, I will present different efforts in applying formal methods to this programming model and to software components in order to ensure the correctness of programming languages and of distributed applications.
 PDF PPTX 
11h4512h30  Laure Daviaud (Warwick University) 
We define two classes of functions, called regular (respectively,
firstorder) list functions, which manipulate objects such as lists,
lists of lists, pairs of lists, lists of pairs of lists, etc. The
definition is in the style of regular expressions: the functions are
constructed by starting with some basic functions (e.g. projections from
pairs, or head and tail operations on lists) and putting them together
using four combinators (most importantly, composition of functions).
Our main results are that firstorder list functions are exactly the
same as firstorder transductions, under a suitable encoding of the
inputs; and the regular list functions are exactly the same as
MSOtransductions.
This is a joint work with Mikolaj Bojanczyk and Krishna Shankara Naravanan. 
5th Edition, 2018, March, 8th
Information
The seminar will be hold at Amphi J, ENS Lyon, Monod site. The meeting is open to all members of the labs LIP, LIRIS, and CITI.
Program
Click on title for abstract.
9h009h30  Welcome  
9h3010h30  Albert Cohen (Inria) 
Deep learning models with convolutional and recurrent networks are
ubiquitous and analyze massive amounts of audio, image, video, text
and graph data, with applications in automatic translation,
speechtotext, scene understanding, ranking user preferences, ad
placement, etc. Competing frameworks for building these networks such
as TensorFlow, Chainer, CNTK, Torch/PyTorch, Caffe1/2, MXNet and
Theano, explore different tradeoffs between usability and
expressiveness, research or production orientation and supported
hardware. They operate on a DAG of computational operators, wrapping
highperformance libraries such as CUDNN (for NVIDIA GPUs) or NNPACK
(for various CPUs), and automate memory allocation, synchronization,
distribution. Custom operators are needed where the computation does
not fit existing highperformance library calls, usually at a high
engineering cost. This is frequently required when new operators are
invented by researchers. Such operators suffer a severe performance
penalty, which limits the pace of innovation. Furthermore, even if
there is an existing runtime call these frameworks can use, it often
does not offer optimal performance for a user's particular network
architecture and dataset, missing optimizations between operators as
well as specialization to the size and shape of data.
We will survey the workinprogress design of (1) a language close to the mathematics of deep learning called Tensor Comprehensions, featuring interesting developments in the areas of automatic range inference, declarative array programming, and dataflow modeling of recurrent networks; (2) a polyhedral JustInTime compiler to convert a mathematical description of a deep learning DAG into a CUDA kernel with delegated memory management and synchronization, also providing optimizations such as operator fusion and specialization for specific sizes; (3) a high level metaprogramming environment and compilation cache populated by an autotuner, acting as a builttoorder library. In a first paper, we demonstrate the suitability of the polyhedral framework to construct a domainspecific optimizer effective on stateoftheart deep learning models on GPUs. Our flow reaches up to 4x speedup over NVIDIA libraries on kernels relevant to the Machine Learning Community, and on an actual model used in production at Facebook. TC also facilitates algorithmic exploration, exposing up to 2 orders of magnitude speedup on research layers. It is open source, integrated with mainstream frameworks Caffe2 (productionoriented) and PyTorch (researchoriented). TC is still at an early stage, and looking for contributions and collaboration. https://research.fb.com/announcingtensorcomprehensions  
10h3011h00  Coffee break  
11h0011h45  Abdallah Arioua (LIRIS)  Repairing techniques for relational databases have leveraged integrity constraints to detect and then resolve errors in the data. User guidance has started to be employed in this setting to avoid a prohibitory exploration of the search space of solutions. In this paper, we present a userguided repairing technique for Knowledge Bases (KBs) enabling updates suggested by the users to resolve errors. KBs exhibit more expressive constraints with respect to relational tables, such as tuplegenerating dependencies (TGDs) and negative rules (a form of denial constraints). We consider TGDs and a notable subset of denial constraints, named contradiction detecting dependencies (CDDs). We propose userguided polynomialdelay algorithms that ensure the repairing of the KB in the extreme cases of interaction among these two classes of constraints. To the best of our knowledge, such interaction is so far unexplored even in repairing methods for relational data. We prove the correctness of our algorithms and study their feasibility in practical settings. We conduct an extensive experimental study on synthetically generated KBs and a realworld inconsistent KB equipped with TGDs and CDDs. We show the practicality of our proposed interactive strategies by measuring the actual delay time and the number of questions required in our interactive framework.  
11h4512h30  Guilhem Jaber (LIP)  This talk will present SyTeCi, the first general automated tool to check contextual equivalence for programs written in an higherorder language with references (i.e. local mutable states), corresponding to a fragment of OCaml.
After introducing the notion of contextual equivalence, we will see on some examples why it is hard to prove such equivalences (reentrant calls, private states). As we will see, such examples can be found in many different programming languages. Then, we will introduce SyTeCi, a tool to automatically check such equivalences. This tool is based on a reduction of the problem of contextual equivalence of two programs to the problem of reachability of “error states” in transition systems of memory configurations. Contextual equivalence being undecidable (even in a finitary setting), so does the nonreachability problem for such transition systems. However, one can apply modelchecking techniques (predicate abstraction, summarization of pushdown systems) to check nonreachability via some approximations. This allows us to prove automatically many nontrivial examples of the literature, that could only be proved by hand before. We will end this talk by the presentation of a prototype implementing this work. 
4th Edition, 2017, June, 1st
Information
The seminar will be hold at the Seminar room of the Centre Blaise Pascal (Access plan) The meeting is open to all members of the labs LIP, LIRIS, and CITI.
Program
Click on title for abstract.
9h009h30  Welcome  
9h3010h15  Alain Darte (LIP)  Compiler code optimizations, and even manual code optimizations, rely on performance models, in general fairly simple analytic models, to drive the different optimization phases. They are certainly useful to provide methodologies, give ``grand principles'', but, when facing reality and approaching optimality, it is not clear how “good” they actually are. They can even drive us to wrong beliefs. In general, we (the community) are fairly bad at measuring the impact of these
models, especially in today's context, with such a range of computer architectures (from FPGA, GPU, vector multicores, to future exascale), with many levels of parallelism and data storage, and where bandwidth, pipelining, and locality are more important than pure computing power. I will give several examples of code optimizations where, if analytic models can provide reassuring metrics for theoretical work, they give very little information on actual performance improvements. I will also quickly present a more heuristic performance model, introduced by physicists, the ECM model, that is fairly useful to optimize codes for vector machines. With Thierry Dumont (from ICJ), we are currently developing an alternative to standard stencillike sparse computations with a better focus on exploiting vector operations as well as spatial and temporal data locality.“ 
10h1510h45  Coffee break  
10h4511h30  Eric Rutten et Gwenael Delaval (LIG)  Heptagon is a synchronous programming language, whose compilation involves discrete controller synthesis. It allows the programmer to express non determinism, by the use of controllable variables, associated with temporal properties the final program will satisfy. These temporal properties are enforced by a controller, automatically generated by a controller synthesis tool. We will present he Heptagon language, its semantics and compilation, and illustrates its use as a backend for CtrlF, a DSL for autonomic managers of reconfigurable software components. 
11h3013h30  Lunch  
13h3014h00  Xavier Urbain (LIRIS)  Mobile robot networks emerged in the past few years as a promising distributed computing model, and received increasing attention from the Distributed Computing community. On the one hand, the use of cooperative swarms of inexpensive robots to achieve various complex tasks in potentially hazardous environments is a promising option to reduce human and material costs and assess the relevance of Distributed Computing in a practical setting. On the other hand, execution model differences warrant extreme care when revisiting “classical results” from Distributed Computing, as very small changes in assumed hypotheses may completely change the feasibility of a particular problem.
I will present a formal proof framework for localised distributed protocols in mobile robotic networks, based on the Coq Proof Assistant. The framework allows for a relatively easy specification of context, protocols, and properties. It was successfully used to certify impossibility results, and to establish formally the correctness of distributed protocols. 
14h0014h30  Jérôme Richard (LIP)  Taskbased models are known to greatly enhance performance and performance portability while component models ease the separation of concerns and thus improves modularity and adaptability. In this talk, we present the COMET programming model, a component model for HPC extended with task concepts, and its implementation built on top OpenMP and L2C.
We evaluate the approach on five synthetic usecases representative of common patterns from HPC applications. Experimental results show that the approach is very efficient on the usecases. On one hand, independent software codes can be easily composed. On the other hand, finegrained composition supports very good performance. It sometimes even outperforms classical handwritten OpenMP implementations thank to better task interleaving. The presentation will also presents previous results conducted on a realworld usecase analysis of a subpart of the production application GYSELA. 
14h3015h00  Coffee break  
15h0015h30  Anupam Das (LIP)  Relational algebras provide important languages for reasoning about programs. In this talk I will present some axiomatisations and proof systems for Kleene algebra, in particular focussing on the importance of “analytic”systems, towards automated reasoning with relational expressions. I will present a methodology for handling least fixed points, such as transitive closure, that has recently become significant in proof theory: nonwellfounded reasoning. While this can be fallacious in general, correct reasoning can be ensured by 'fairness' criteria, and we can thus design classes of systems suitable for reasoning in these frameworks. 
3rd Edition, 2016, November, 3rd
Information
The seminar will be hold at the Seminar room of the Centre Blaise Pascal (Access plan) The meeting is open to all members of the labs LIP, LIRIS, and CITI.
Preliminary Program
9h9h30  Welcome  
9h3010h15  Guillaume Salagnac (CITI)  Peripheral State Persistence For Transiently Powered Systems  
10h1510h45  Coffee break  
10h4511h30  Olivier Muller (TIMA)  An OpenMP flow targeting HPC systems with FPGA  
11h3013h00  Lunch  
13h0013h45  Paul Feautrier (LIP)  Toward a polynomial model, with application to the OpenStream Language (cont'd)  
13h4514h30  Christophe Alias et Laure Gonnord (LIP)  Estimation of Parallel Complexity with Rewriting Techniques  
14h3015h00  Coffee break  
15h0015h45  Romuald Thion (LIRIS)  Inference leakage detection for authorization policies over RDF data  
15h4516h30  Patrick Baillot (LIP)  On a typebased time complexity analysis of subrecursive programs 
2nd Edition, 2016, June 24th
Information
The seminar will be hold at the Buisson site of ENS Lyon, allée de Fontenay. The meeting is open to all members of the labs LIP, LIRIS, and CITI.
Program
9h9h30  Welcome  
9h3010h15  Damien Pous (LIP)  Tutorial Coq  
10h1511h00  Angela Bonifati (LIRIS)  Schema matching and mapping systems  
11h11h30  Coffee break  
11h3012h15  Matteo Mio (LIP)  Tutorial Markov Decision Processes / Stochastic Games  
–  
12h1513h45  Lunch break at Descartes CROUS  
–  
13h4514h30  Paul Feautrier (LIP)  Toward a polynomial model, with application to the OpenStream Language  
14h3015h15  Tomofumi Yuki (LIP)  Static Analysis of Parallel Programs with Loops, Tasks, and Synchronizations  
15h1515h45  Coffee break  
15h4516h30  Tanguy Risset (CITI)  Compilation de dataflow parametrique pour machines multicore heterogènes  
16h3017h15  Adrien BassoBlandin (LIP)  Model instantiation in KAMI 
1st Edition, 2016, March 17th
Information
The seminar had gathered 31 people, Thursday 17 March 2016, at résidence Villemanzy, 21 montée St Sébastien at Lyon, 1er arr. (http://www.belambravillemanzy.fr/fr/seminaires). The meeting was open to all members of the labs CITILIPLIRIS.
Program
9h9h15  Welcome  
9h1510h  Laure Gonnord et Lionel Morel (LIP/CITI)  Les langages flot de données dans tous leurs états  
10h10h30  Coffee break  
10h3011h15  Emmanuel Coquery (LIRIS)  Langages de requêtes en bases de données: tour d’horizon des différents paradigmes  
11h1511h45  Hélène Coullon (LIP)  The MultiStencil Language  
11h4512h15  Christian Perez (LIP)  Des langages d'assemblages dans les modèles à composants logiciels  
–  
12h1513h45  Lunch break  
–  
13h4514h30  Russ Harmer (LIP)  Executable knowledge  
14h3015h  Thierry Gautier (LIP)  Programmation et exécution d’algorithmes parallèles  
15h15h30  Coffee break  
15h3016h  Simon Castellan (LIP)  Weak memory models using event structures  
16h16h30  Arnaud Lefray (LIP)  Formalisation of security requirements 