Equations is a plugin for the Coq proof assistant which
provides a notation for defining programs by dependent
pattern-matching and structural or well-founded
recursion. It additionally derives useful high-level proof
principles for demonstrating properties about them,
abstracting away from the implementation details of the
function and its compiled form. I will present the general
design and implementation that provides a robust and
expressive function definition package as a definitional
extension to the Coq kernel. At the core of the system is
a new simplifier for dependent equalities based on an
original handling of the no-confusion property of
constructors. I will also present examples of how the tool
helps not only writing complex programs but also proofs
about them.
14/02/2019: Jean-Ferdinand Susini
: Programmation réactive avec les SugarCubes
24/01/2019: Ulysse Gérard
: Programming with lambda-tree syntax
We present the design of a new functional programming
language, MLTS, that uses the λ-tree syntax approach to
encoding bindings that appear within data structures. In
this setting, bindings never become free nor escape their
scope: instead, binders in data structures are permitted
to move into binders within programs. The design of MLTS
includes additional sites within programs that directly
support this movement of bindings.We illustrate the
features of MLTS by presenting several collections of
examples. We also present a typing discipline that
naturally extends thetyping of OCaml programs. In order to
formally define the language’s operational semantics, we
present an abstract syntax for MLTS and a natural
semantics for its evaluation. We shall view such natural
semantics as a logical theory with a rich logic that
includes both nominal abstraction and the ∇-quantifier: as
a result, the natural semantic specification of MLTScan be
given a succinct and elegant presentation.
13/12/2018: Serge Rosmorduc
: Coder un corpus d’égyptien ancien, problèmes et perspectives
Le codage d’un corpus combinant une langue morte et une
écriture fortement iconique, pose le problème de
l’identité même du signe d’écriture et du « grain » de
l’encodage. La création du corpus Ramsès, en collaboration
avec l’Université de Liège, nous a permis de mettre en
evidence les problèmes de cohérence des formalismes
existants. Nous présenterons quelques cas intéressants et
nous exposerons l’état de nos réflexions sur la création
d’un nouveau répertoire de codes.
18/10/2018: Boubacar Sall
: Raffinement de Programmes Impératifs en Coq
D'une spécification abstraite intelligible à un programme
éfficace, il peut exister un écart important. Cet écart
est en général difficile à combler d'une traite. La
technique des raffinements successifs est un moyen de
répondre à ce problème. Il s'agit d'appliquer à la
spécification initiale une séries de transformations
simples, qui permettent après chaque transformation de se
rapprocher d’une solution exécutable. La correction du
programme finalement obtenu découle alors de la correction
des transformations, correction dont il faut bien entendu
s'assurer, par la preuve de préférence. Dans ce
séminaire, nous présentons une application du raffinement
qui s'appuie sur l'assistant de preuves Coq afin de
formaliser les spécifications, les programmes, la
méthodologie de raffinement ainsi que les obligations de
preuves qui en découlent.
11/10/2018: François Lamarche
: Pourquoi et comment apprendre le Rust
Durant les cinq dernière années on a introduit une
poignée de langages pour occuper le même créneau que le
C++. Rust, dont la version 1.0 date de février 2015, a
pris pas mal d'avance sur la compétition. Pour s’en
convaincre il suffit d’observer la croissance de son site
de paquetages www.crates.io.
Rust se distingue d’abord et avant tout par un système de
types à la fois très fort et très moderne, qui permet
d’avoir recours au polymorphisme paramétrique autant
qu'au polymorphisme ad hoc pour produire du code
générique. On peut décrire Rust en une phrase en disant
que qu'il s’approche autant qu’on peut le faire d’un
langage fonctionnel—en particulier, on a les
fermetures—sans nécessiter un garbage collector. Il
donne aussi l'accès explicite au sous-ensemble de sa
bibliothèque standard qui peut se passer de malloc, pour
des programes embarqués qui tournent sur le “bare metal”.
Donc c’est un langage à la fois bas-niveau et
haut-niveau, qui compile directement en IR LLVM, pour
générer du code aussi rapide que le C.
La caractéristique la plus célèbre de ce système de types
est le fameux “borrow checker” et ses “lifetimes", qui
tient compte explicitement de la durée de vie des
références (qui sont des objets plus sophistiqués que de
simples pointeurs) et tue dans l'oeuf énormément
d’erreurs communes dans les langages bas niveau comme le
“use after release”. Ce même système de types simplifie
aussi énormément la gestion de threads multiples.
Mais ce n’est pas un langage pour débutants! Est-ce
surprenant après ce que je viens de dire? Il faut
développer une certaine expérience pour comprendre les
messages d’erreur du compilateur et passer du “mais
qu’est-ce que ça veut dire?” au “ah oui, bien sûr, quel
étourdi je suis!”. En passant c’est un compilateur
aimable et plein d’attentions.
Je vais donc donner les bases de ce système de types,
partager un peu mon expérience d'apprentissage, et
pointer sur la documentation qui permettra aux intéressés
(il y en aura sûrement) de progresser dans
l’apprentissage du premier vrai langage de programmation
du 21ème siècle.
04/10/2018: Danko Ilik
: Industrial use of proof assistants in cyber-security and safety
In this talk, I will give an overview of certain industrial schemas
that are used in cyber-security and in safety when high-levels of
assurance, provided by formal proofs, are required. After that, I will
concentrate on the scientific aspects relating to proofs and
programming languages, and the special role that proof assistants play
during these evaluations.
At the end of the talk, I will briefly overview the
/stages/ for master students that are currently being
offered in embedded systems at Siemens Mobility and
available at: https://jobs.siemens-info.com/jobs?page=1
05/07/2018: Nicolas Toper
: Parallélisation de bytecode Java
28/06/2018: Gabriel Scherer
: Tout réussir en répétant beaucoup
Dans cet exposé je vais vous montrer comment implémenter
un effet de non-déterminisme angélique (par exemple
l'opérateur `amb`) directement en OCaml, en utilisant
seulement de l'état modifiable et des exceptions. Cette
implémentation peut s'étendre pour obtenir les
continuations délimitées ! Il n'est pas nécessaire de
connaître déjà le non-déterminisme ou les continuations
pour suivre l'exposé, qui commencera (pour la culture) par
un petit tour d'horizon des notions d'effet en langages de
programmation: style direct et indirect, monades, la
réflexion monadique de Filinski, et les "effect handlers".
07/06/2018: Ruben Milocco
: Efficient relay selections in WSN and prediction using
ARMA models
The presence of both location and transmission range
uncertainties require efficient relays selection in
wireless sensor networks (WSN) to guarantee speed and
amount of information transferred with respect to the
energy used. Based on the effect that these uncertainties
have on the link channel capacity, strategies to decide
the next hop relay, which optimizes, in mean, the maximum
rate of information transmitted with the minimum number of
hops are analyzed. Topics such as, Estimation of distance
between nodes in a WSN; Derivation and comparison of error
bounds; The problem of distance uncertainties in
geographic routing, and The robust geographic routing
strategy by selecting nodes using metrics like loss of
information and progress of information are analyzed.
On the other hand, the prediction of data in time series
is important in many TIC’s applications. The optimal
predictor, in the sense of minimum variance, is the
stable-inverse of the model that whiteness the time series
data. This turns the prediction as an identification
problem of a model in real-time. In particular, if the
data series is stochastically time-varying, a real-time
identification algorithm is what should be used. In this
talk we will analyze the problem of real-time prediction
of time series using an ARMA model. Applications are
presented to predicting the popularity of video contents
using real traces extracted from YouTube, we show that
Auto- Regressive and Moving Average (ARMA) models can
provide accurate predictions. Also predicting data centers
requests such as CPU, priority and memory are addressed.
31/5/2018: Steven Varoumas
: Programmation synchrone multi-horloges pour microcontrôleurs à faibles
ressources
Dans cet exposé, on présentera OCaLustre, une extension
synchrone à flots de données du langage OCaml, inspirée du
langage Lustre et destinée à la programmation de
microcontrôleurs. Après présentation de l'écosystème qui
permet l'exécution de bytecode OCaml sur microcontrôleurs
(très) limités en ressources, et après avoir décrit la
sémantique d'OCaLustre et ses différentes étapes de
compilation, on détaillera le système des horloges
synchrones d'OCaLustre. Ce système, permettant d'attribuer
des conditions de présence aux flots d'un programme, peut
être vu comme un système de types. On présentera alors en
détails nos travaux visant à formaliser ce système dans
Coq.
9/4/2018: Hajer Baazaoui
: Construction d'ontologies et d'ontologies floues :
application à la recherche d'information
15/02/2018: Anne-Gwen Bosser
: Sur la narration interactive, la logique linéaire, Coq, et
la danse contemporaine
Continuation-passing style translations, or CPS, are used
notably in compilers. They make a functional program more
explicit by sequentializing its computations and reifying
its control. They have been used as an intermediate
language in many compilers. Yet, we cannot directly use
Plotkin's original CPS translation to design compilers,
for several reasons: i) the resulting terms it produces
are verbose (they contain ``administrative redexes'', a
well-studied problem) and inefficient (they perform nested
beta-reductions sequentially); and ii) their loose syntax
can hide possible further optimizations, in particular
tail call elimination.
These issues have been solved in isolation and on paper,
but never combined together and formalized, which i) is
necessary to scale to safe, full-featured optimizing
compilers and ii) is not a mere juxtaposition of the
techniques but requires insight on the design of CPS
translations themselves. We propose to design and
implement in OCaml a compacting, optimizing CPS
translation, while using OCaml's type system to verify
that it maps well-typed terms to well-typed terms in a
tightly restricted syntactical form (the ``typeful''
approach to formalization). The resulting artifact can be
used directly to design optimizing compilers, and the path
towards it offers a tutorial on optimizing CPS
translations, and yet another use case for OCaml's
advanced type system.
14/12/2017: Rachid Rebiha
: Crypto-monnaie et blockchain
Pour diverses raisons, les crypto-monnaies et leurs
protocoles reçoivent beaucoup d'attention. D'une part, les
optimistes expliquent que le Bitcoin est enfin une monnaie
cryptographique avec le bon protocole contournant tous les
obstacles qui ont mis fin aux tentatives précédentes. D'un
autre côté, nous trouvons ceux qui veulent exprimer leurs
réserves et leurs préoccupations sur le plan technique et
économique. Cette présentation vise à identifier
l'approche clé choisie dans le protocole. Nous proposons
de reconstruire le protocole avec sa structure (Block
Chain) et le concept sous-jacent de son algorithme de
consensus. Nous allons procéder étape par étape pour
aborder les obstacles informatiques perçus. Nous
proposerons des déductions substantielles basées sur ce
qui est programmé à court et à long terme. Enfin, nous
pourrions brièvement évoquer un éventuel programme de
recherche impliquant des méthodes formelles et des
crypto-monnaies (par exemple, l'analyse, la preuve, la
vérification de «smart contract», ...).
5/10/2017: Benoit Rognier
(cofondateur EDUKERA): Edukera, un assistant de
démonstration mathématique destiné à la remise à niveau des
étudiants en début de cursus scientifique.
edukera permet aux étudiants d'élaborer des démonstrations
mathématiques à l'aide des définitions et théorèmes du
cours mis à disposition dans la "boîte à outils".
L'application edukera valide automatiquement les solutions
élaborées par les étudiants. Elle fournit aux enseignants
des statistiques d'activité détaillées, pour le soutien et
l'évaluation des étudiants.
edukera est également adapté à l'enseignement de la
Logique formelle grâce à un chapitre dédié (connecteurs,
quantificateurs, ...).
Programme : présentation de l'interface de démonstration,
exemples de démonstration, bénéfices pédagogiques
10/03/2016: Sergueï Lenglet
Equivalences comportementales pour les opérateurs de
contrôle
Les équivalences comportementales permettent de prouver
que deux programmes se comportent de la même manière
quelque soit le contexte d'exécution. Dans cette
présentation, nous présenterons plusieurs styles
d'équivalences comportementales pour un lambda calcul
étendu avec des opérateurs de contrôle délimité. Ces
opérateurs permettent à un programme de capturer une
partie de son environnement d'exécution, par exemple pour
le sauvegarder et le restaurer plus tard.
14/04/2016: Ivan Gazeau
: Système de typage pour garantir la confidentialité dans le
Cloud
This talk presents a type system that ensures that data is
kept confidential in a distributed environment. We assume
an open environment in which a range of processes at
different locations communicate over channels. Principal
identities can be created at runtime and our type system
labels variables with the identities of those allowed to
know them. Encryption preserves these types when data is
sent between devices. Similar to other work in this area,
we prove a form of non-interference result: that the value
of high level data is not observable by its affect on low
level data. However, we also prove a location-based
result: if all locations that are not explicitly trusted
with a variable are replaced with untyped active
attackers, then none of these attackers can know the value
of that variable. We argue that this model is well suited
for open cloud services and give an example of a secure
cloud storage service.
08/04/2016: Guillaume Scerri
: Tackling new challenges in security using logical methods
Security protocols are more widely used everyday. This
growing ecosystem makes the need for automated
verification and certification of protocols ever more
prominent. In this talk we will present a new logic based
tool (SCARY) for proving security, acting in a new model
proposed by G. Bana and H. Comon in 2012. SCARY
significantly differs from previous automated tools in
that it is a consistency checker rather than a model
checker. It provides a much more fine grained analysis
than previous tools. We will show how such a tool is
particularly well suited for tackling the new challenges
arising from Cloud Computing and the Smart Objects. We
will also see why SCARY is a particularly good candidate
for providing proof scripts for security oriented proof
assistants.
31/03/2016: Lionel Rieg
: Formalisation de la compilation des langages synchrones : de
Lustre à Esterel
Les langages synchrones sont un paradigme de calcul dans
lequel l'exécution d'un programme est découpée en
instants. Au sein de chaque instant, les calculs sont
supposés se faire instantanément —c'est l'hypothèse de
synchronie—, ce qui réconcilie parallélisme et
déterminisme. On peut distinguer deux familles de
langages synchrones : les langages orientés données tels
Lustre ou Signal et les langages orientés contrôle tel
Esterel. En me concentrant sur Lustre et Esterel, je vais
montrer quelles sont les difficultés de prouver
formellement leur compilation. Comme nous le verrons, ces
difficultés sont très différentes selon la cible vers
laquelle on compile, un langage de programmation ou des
circuits digitaux.
29/03/2016: Guilhem Jaber
: Raisonner sur l'équivalence de programmes pour des langages
fonctionnels avec effets.
L'équivalence contextuelle de programmes pour un langage
fonctionnel avec références (i.e. des cellules mémoires
mutables) est un problème notoirement difficile,
particulièrement en présence de références d’ordre
supérieur (c’est à dire des références pouvant stocker des
fonctions). Ces deux dernières décennies, différentes
techniques ont été introduites pour traiter ce problème:
relations logiques a la Kripke, bisimulations, et
sémantique des jeux algorithmique.
Après avoir présenté les principes essentiels derrière ces
techniques, nous tisserons des liens entres elles grâce à
l'introduction de la sémantique des jeux opérationnelle,
en se basant sur un modèle de traces. Cela nous permettra
d'aboutir à une nouvelle méthode de preuve d'équivalences:
les bisimulations ouvertes a la Kripke. L'avantage majeur
de cette méthode est d'être suffisamment simple pour
pouvoir à terme être en grande partie automatisée.
24/03/2016: Thomas Carle
:
Compilation efficace et correcte-par-construction pour systèmes
cyber-physiques complexes.
Les domaines de la compilation et de l’ordonnancement
temps-réel se sont développés séparément. Si ces deux
domaines partagent le même objectif – la construction
d’implémentations correctes – leur séparation est
justifiée historiquement par des différences
significatives entre les modèles et les méthodes
utilisées. Cependant, étant donnée la complexification
actuelle des applications et du matériel composant les
plateformes d’exécution, les objets et les problèmes
étudiés dans ces deux domaines se recouvrent de plus en
plus. Dans ce séminaire, je vais passer en revue mes
travaux en insistant particulièrement sur ceux touchant à
la compilation pour systèmes embarqués critiques, et
esquisser en quoi ces travaux plaident pour une
réconciliation entre les domaines de la compilation et de
l’ordonnancement temps-réel. Ce rapprochement est opéré
autour de l’utilisation du formalisme et des langages
synchrones, qui peuvent être vus comme une extension
commune des modèles utilisés classiquement en compilation
(Single Static Assignment et Data Dependency Graphs) et en
ordonnancement temps-réel (Dependent Task Graphs), mais
qui fournissent également des techniques puissantes pour
manipuler efficacement des structures de contrôle
complexes et qui ouvrent la porte à la preuve formelle des
algorithmes de compilation ou à la preuve automatisée des
implémentations compilées.
22/03/2016: Abderrahim Ait Wakrime
:
Une approche par composants pour la visualisation
scientifique interactive.
Les architectures par composants sont de plus en plus
étudiées et utilisées pour le développement efficace des
applications en génie logiciel. Elles offrent, d’un coté,
une architecture claire aux développeurs, et de l’autre,
une séparation des différentes parties fonctionnelles et
en particulier dans les applications de visualisation
scientifique interactives. La modélisation de ces
applications doit permettre la description des
comportements de chaque composant et les actions globales
du système. De plus, les interactions entre composants
s’expriment par des schémas de communication qui peuvent
être très complexes avec, par exemple, la possibilité de
perdre des messages pour gagner en performance.
Cet exposé propose le modèle ComSA (Component-based
approach for Scientific Applications) qui est basé sur une
approche par composants dédiée aux applications de
visualisation scientifique interactive et dynamique
formalisée par les réseaux FIFO colorés stricts
(sCFN). Les principales contributions sont dans un premier
temps, un ensemble d’outils pour modéliser les différents
comportements des composants ainsi que les différentes
politiques de communication au sein de l’application. Dans
un second temps, la définition de propriétés garantissant
un démarrage propre de l’application en analysant et
détectant les blocages. Cela permet de garantir la
vivacité tout au long de l’exécution de
l’application. Finalement l’étude de la reconfiguration
dynamique des applications d’analyse visuelle par ajout ou
suppression à la volée d’un composant sans arrêter toute
l’application. Cette reconfiguration permet de minimiser
le nombre de services non disponibles.
17/03/2016: Matthias Puech
:
Types contextuels pour la méta-programmation : où
raisonnements et langages se construisent ensemble.
La méta-programmation est l'écriture de programme qui
interprètent, manipulent ou génèrent des programmes. Les
langages qui la facilite, comme Lisp par exemple,
présentent de nombreux écueils pour le programmeur et un
typage statique y est un allié important. Nous nous
intéresserons ici à la conception de systèmes de types
pour une sorte particulière de méta-programmation: le
calcul par niveau (staged computations).
Nous proposons la théorie des types contextuelle avec
environnements de première classe comme discipline de
typage des langages par niveaux. Celle-ci est en
correspondence de Curry-Howard avec une extension
conservatrice de la logique modale de nécessité S4, la
logique contextuelle. En particulier, ce système subsume
nombre de propositions précédentes, notamment les systèmes
basés sur LTL de Davies et Pfenning. Ce résultat offre
notamment un nouveau jour sur le processus de
normalisation de programmes, utile dans l'analyse statique
et l'optimisation.
Ces travaux, conduits à McGill en collaboration avec
Brigitte Pientka, s'inscrivent dans le cadre d'une étude
plus générale des mécanismes de typage, d'interprétation
et de compilation de programmes à la lumière de la théorie
de la preuve; son but ultime étant de raffiner la
conception de nos outils d'analyse et de preuve formelle
des programmes.
15/03/2016: Pablo Rauzy
:
Approche formelle de la sécurité des données personnelles
Je présenterai rapidement mes travaux de thèse sur la
sécurité des implémentations cryptographiques face aux
attaques physiques, puis je parlerai de ce que le fais en
post-doc autour de la notion de "privacy as
control". Enfin je donnerai un aperçu de ce que j'aimerais
faire par la suite dans le cadre de la protection des
données personnelles.
