Property

Job field

From LRDE

This is a property of type Text.

Showing 40 pages using this property.
J
The Spot library (http://spot.lip6.fr/) contains many algorithms for translating LTL formulas into Büchi automata, and to simplify these formulas and automata. A recently added technique (in Spot version 1.2) allows us to minimize deterministic Büchi automata using a SAT-solver. To minimize a n-state deterministic Büchi automaton (an NP-complete problem) we encode its equivalence with a (n-1)-state deterministic Büchi automaton as a SAT problem, and let a SAT solver do the work of finding a solution. If such a solution is found, we try again, looking for a (n-2) state automaton, etc.  +
Les méthodes d'imagerie par tomographie optique cohérente trouvent une application majeure en imagerie ophtalmique de la rétine. Mais les techniques d'imagerie confocale de l'état de l'art, basées sur l'utilisation d'une source de lumière balayée spatialement et une détection sur photodiode, sont limitées en débit (de l'ordre de 100 Mega voxel/s pour les instruments médicaux les plus aboutis actuellement). Une nouvelle gamme d'appareils de tomographie optique cohérente actuellement en cours de développement s'appuie sur des lasers accordables en longueur d'onde et une détection holographique sur caméra, permettant d'atteindre des débits de l'ordre de 10 Giga voxel/s. Leur très haute sensibilité assure un tel débit de données tout en respectant les normes médicales d'illumination de la rétine. Les séquences recueillies sont de types "hyperspectrales": elles permettent, à un instant donné, de réaliser une cartographie des contrastes de diffusion et d'absorption optique à différents niveaux de profondeur de pénétration dans la rétine. Ces séquences, acquises à très haute fréquence temporelle, facilitent ainsi l'étude des phénomènes dynamiques tels que le flux sanguin dans les vaisseaux rétiniens. Le volume et la cadence d'acquisition de données d'une part, et la reconstruction par calcul d'hologrammes d'autre part, jouent un rôle crucial dans la définition et l'acquisition de signaux pertinents exploitables pour l'imagerie hyperspectrale en temps réel. La visualisation en temps réel des images acquises par interférométrie holographique est en effet très gourmande en puissance de calcul, car contrairement aux méthodes de visualisation directe, des algorithmes de calcul de propagation d'ondes sont nécessaires pour reconstruire l'image à partir d'interférogrammes échantillonnés par la caméra.  +
The classical theory of automata, of transducers and of rational expressions, admits a very elegant and extremely useful extension (eg, in natural language processing) taking into account the concept of weighting. The weights are then taken in a semi-ring, which can be classical (⟨𝔹, ∨, ∧⟩, ⟨ℤ, +, ×⟩, ⟨ℚ, +, ×⟩, etc..), tropical (⟨ℤ, min, +⟩, etc..), or yet of another type (e.g. rational expressions). Vcsn is a project led by Alexandre Duret-Lutz and Akim Demaille (LRDE). It is a platform for the manipulation of automata, transducers and weighted rational expressions. It is written in C++11 avoiding the classical object-oriented programming in favor of generic programming (template) for more performance. Vcsn is an heir of the Vaucanson 2 project which was developed in partnership with Jacques Sakarovitch (Telecom ParisTech) and Sylvain Lombardy (LaBRI). Vcsn aims at speed and user friendliness. To achieve this goal, it is built in three layers: * ''static'': this is a templated C++ library with efficient data structures and algorithms * ''dyn'': this C++ API support type-erasure and shields the user from the complex API of ''static'' while preserving performances. It also support code-generation and linking on the fly * ''Python'': on top of ''dyn'', a Python binding allows a pleasant use of Vcsn, without any C++ knowledge required.  +
The Spot library (https://spot.lrde.epita.fr/), written in C++11, offers several algorithms and data structures to build model checkers. It contains many algorithms for handling linear-time temporal logic (LTL) formulas, or for different variants of Büchi automata. Spot also distributes several command-line tools, built on top of the library. Finally, Spot includes some Python bindings, as well as a web interface (https://spot.lrde.epita.fr/trans.html) for easy access to one of the features of the library.  +
The Spot library (http://spot.lip6.fr/) contains many algorithms for translating LTL formulas into Büchi automata, and to simplify these formulas and automata. A recently added technique allows us to minimize deterministic Büchi automata using a SAT-solver; the implementation is actually not restricted to Büchi and can work with deterministic omega-automata with any acceptance conditions. To minimize a n-state deterministic omega-automaton (an NP-complete problem) we encode its equivalence with a (n-1)-state deterministic omega-automaton as a SAT problem, and let a SAT solver do the work of finding a solution. If such a solution is found, we try again, looking for a (n-2) state automaton, etc.  +
DSL design and implementation is booming. There are many approaches to this problem, one is about using the extensibility capabilities of a general-purpose programming language in order to meet specific requirements. Many multi-paradigm approaches (eg functional languages / compile-time meta-programming) also offer benefits. Lisp is a language that is particularly well suited for this type of problem, but it is almost totally absent from the literature on DSLs. Indeed, most researchers are not (or not anymore) familiar with this language. They prefer a language based on a static approach, or have simply forgotten everything Lisp is capable of.  +
R is a programming language for statistics. Because of its historical development, it has many similarities with Scheme (a language from the Lisp family), but also many problems: in particular, it is a language which is not compiled. The biggest complaint of its users is therefore its lack of performance. For this (bad) reason a number of totally esoteric features have been added to it.  +
Keywords: * image processing, * mathematical morphology, * tree-based reasoning, * algorithmic optimization.  +
Keywords: * image processing, * mathematical morphology (connected operators), * tree of shapes, * shaping  +
Keywords: * image processing, * mathematical morphology, * tree-based reasoning, * algorithmic optimization.  +
Climb est une bibliothèque de traitement d'image écrite en Common Lisp. Elle est pourvue d'un ensemble d'abstractions permettant de décrire des traitements génériques (sans connaissance préalable sur la nature des images cibles) et d'un ensemble d'algorithmes prédéfinis basés sur ces abstractions. Il est évidemment possible d'écrire de nouveaux algorithmes. Elle offre également un DSL (Domain Specifique Language) pour la déclaration de chaînes complexes de traitement et une interface graphique pour la programmation visuelle de ces mêmes chaînes. Le haut niveau d'abstraction de la bibliothèque a un impact non négligeable sur les performances.  +
Climb est une bibliothèque de traitement d'image écrite en Common Lisp. Elle est actuellement pourvue d'une interface graphique permettant de concevoir des chaînes de traitement d'images (Cf. capture d'écran) visuellement et à la souris, c'est-à-dire sans avoir besoin de recourir à de la programmation. Ceci est particulièrement utile pour des « clients » non informaticiens. L'interface en question a été développée assez rapidement pour des besoin de démonstration, mais n'est pas une solution satisfaisante sur le long terme. L'interface elle-même est limitée en fonctionnalités, peu ergonomique, pas très aguichante ni bien intégrée avec les différentes plateformes. De plus, Gtk2 est un toolkit ancien dont la couche d'interfaçage avec Lisp n'est plus vraiment maintenue.  +
The Spot library (https://spot.lrde.epita.fr/) written in C++11 offers several algorithms and data structures to build model checkers. Such a tool checks whether the model of a system meets a given specification. One way to perform this verification is to encode both the specification and the model as omega-automata, build the synchronous product of the two previous automata and finally check wether the product automaton has an empty language. This last operation is called an emptiness check and deals with automata of millions of states and transitions. Recently many parallel emptiness checks have been proposed, each of them having strengths an weakness. Nonetheless it is still unknown if one of them outperform the others. Indeed, since all these algorithms are implemented in different tools, a fair comparison is impossible.  +
Le stage proposé s’inscrit dans la thématique “reconnaissance des formes” du laboratoire. Le contexte est l’analyse d’images ou de séquences d’images vidéos contenant des éléments de texte. L’extraction automatique de texte dans des images naturelles ou des vidéos est une fonction essentielle dans de nombreuses applications, notamment l’indexation automatique de documents ou photographies, la dématérialisation de documents, l’assistance aux personnes malvoyantes, etc. Le sujet proposé a pour objet la reconnaissance de texte dans les images naturelles. Des techniques de localisation automatique de texte ont déjà été développées au LRDE. Nous souhaitons maintenant être capable de reconnaître le texte extrait. Il existe déjà des logiciels capables de reconnaître du texte (O.C.R) mais ces logiciels ne sont pas prévus pour le contexte des images naturelles. Les difficultés que présentent ce type d’images (déformation perspective, défauts d’illumination...) rendent la reconnaissance difficile. Plusieurs pistes seront explorées, tant sur les descripteurs, que sur les outils de classification.  +
Le langage Lisp dispose de mécanismes pour la documentation du code (les « docstrings ») et pour l'introspection, permettant ensemble d'extraire suffisamment d'information pour générer des manuels de références automatiquement. Par ailleurs, un système nommé QuickLisp consistue aujourd'hui le standard de-facto pour le téléchargement et la gestion de distributions de bibliothèques. En combinant ces deux idées, il devient envisageable de fournir une plateforme de documentation plus ou moins globable du monde Lisp, générée automatiquement.  +
The Spot library (http://spot.lrde.epita.fr/) contains many algorithms for translating LTL formulas into omega-automata, and to simplify these formulas and automata. It also provides support to build an LTL model checker, through algorithms testing whether the language of such an automaton is empty or not. Omega-automata are used to represent languages over infinite words. These automata can be defined using numerous acceptance conditions such as Büchi, co-Büchi, Rabin, Streett, Parity, etc. Spot actually supports these acceptances condition in a generic way and allow them to be combined as desired.  +
The Spot library (http://spot.lrde.epita.fr/) contains many algorithms for translating LTL formulas into omega-automata, and to simplify these formulas and automata. It also provides support to build an LTL model checker, through algorithms testing whether the language of such an automaton is empty or not. The model-checking process takes a model of a system and a LTL formula to check, and outputs either "correct" if the property holds, or a run of the system on which the property does not hold (a counterexample).  +
Mots-clefs : * polymorphisme paramétrique * programmation générique * C++ * structures de données et interfaces * génie logiciel * traitement d'images.  +
Les langages de programmation généraux fournissent tous un certain nombre de types natifs tels les entiers, flottants, chaînes de caractères etc., des agrégats niveau utilisateur comme les structures ou les classes des languages oritentés-objet, et finalement des types de séquences tels les listes, vecteurs ou tableaux multi-dimensionnels. Dans un langage dynamiquement typé, il est possible de manipuler des séquences hétérogènes, c'est-à-dire dont les éléments sont potentiellement de types différents. Par exemple, la liste (1.5 "foobar" t) est une séquence hétérogène contenant un entier, une chaîne de caractères et un symbole. Partant de là, la question du typage de ces séquences se pose: si une séquence suit un motif particulier de type pour ses éléments, comment exprimer le type de toutes les séquences suivant ce même motif ? Une réponse possible à cette question consiste à utiliser un formalisme proche des expressions rationnelles, que nous appelons « expressions rationnelles de types ». Par exemple, le type (int . string+ . symbol) pourrait représenter l'ensemble de toutes les séquences commençant par un entier, contenant ensuite une ou plusieurs chaînes de caractères, et terminées par un symbole. Un tel système a été implémenté pour le langage Common Lisp. Ce système contient un moteur (une machine à états) permettant de détermniner si une séquence est conforme à un type hétérogène, et s'intègre dans le mécanisme de typage du langage afin d'en produire une extension déclarative.  +
The Spot library (https://spot.lrde.epita.fr/) written in C++14 offers several algorithms and data structures to build model checkers. Such a tool checks whether the model of a system meets a given specification. One way to perform this verification is to encode both the specification and the model as omega-automata, build the synchronous product The model-checking process takes a model of a system and a LTL formula to check, and outputs either "correct" if the property holds, or a run of the system on which the property does not hold (a counterexample).  +
The classical theory of automata, of transducers and of rational expressions, admits a very elegant and extremely useful extension (eg, in natural language processing) taking into account the concept of weighting. The weights are then taken in a semi-ring, which can be classical (⟨B, ∨, ∧⟩, ⟨Z, +, ×⟩, ⟨Q, +, ×⟩, etc..), tropical (⟨Z min, +⟩, etc..), or yet of another type (eg rational expressions). Vaucanson 2 is a project with financial aid from ANR (National Research Agency) developed in partnership between Telecom ParisTech (Jacques Sakarovitch), LaBRI (Sylvain Lombardy) and the LRDE (Alexandre Duret-Lutz and Akim Demaille). It is a platform for the manipulation of automata, transducers and weighted rational expressions. It is written in C++11 avoiding the classical object-oriented programming in favor of generic programming (template) for more performance.  +
La théorie classique des automates, des transducteurs et des expressions rationnelles, admet une extension très élégante et extrêmement utile (e.g., en traitement des langues naturelles) prenant en compte un concept de pondération. Les poids sont alors pris dans un semi-anneau, qu'il soit classique (⟨B,∨,∧⟩, ⟨Z,+,×⟩, ⟨Q,+,×⟩, etc.), tropical (⟨Z,min,+⟩, etc.), ou autre encore (par exemple des expressions rationnelles). Vaucanson 2 est un projet ANR développé en partenariat entre Télécom ParisTech (Jacques Sakarovitch), le LaBRI (Sylvain Lombardy) et le LRDE (Alexandre Duret-Lutz et Akim Demaille). Il s'agit d'une plate-forme de manipulation des automates, transducteurs et expressions rationnelles pondérés. Elle est écrite en C++11 en évitant la programmation orientée-objet classique, au profit de la programmation générique (template) pour les performances.  +
The classical theory of automata, of transducers and of rational expressions, admits a very elegant and extremely useful extension (eg, in natural language processing) taking into account the concept of weighting. The weights are then taken in a semi-ring, which can be classical (⟨𝔹, ∨, ∧⟩, ⟨ℤ, +, ×⟩, ⟨ℚ, +, ×⟩, etc..), tropical (⟨ℤ, min, +⟩, etc..), or yet of another type (e.g. rational expressions). The field 𝔽₂ is a particular interest, and shows quite a few unique properties, as demonstrated by the current active research under various names (e.g., "Symmetric Difference Automata"). Vcsn is a project led by Alexandre Duret-Lutz and Akim Demaille (LRDE). It is a platform for the manipulation of automata, transducers and weighted rational expressions. It is written in C++11 avoiding the classical object-oriented programming in favor of generic programming (template) for more performance. Vcsn is an heir of the Vaucanson 2 project which was developed in partnership with Jacques Sakarovitch (Telecom ParisTech) and Sylvain Lombardy (LaBRI).  +
Many properties and characteristics of an automaton can be easily computed from its syntactic monoids. Such properties are of particular importance to theoreticians. Vcsn is a project led by Alexandre Duret-Lutz and Akim Demaille (LRDE). It is a platform for the manipulation of automata, transducers and weighted rational expressions. It is written in C++11 avoiding the classical object-oriented programming in favor of generic programming (template) for more performance. Vcsn is an heir of the Vaucanson 2 project which was developed in partnership with Jacques Sakarovitch (Telecom ParisTech) and Sylvain Lombardy (LaBRI). Vcsn has a sound base of data structure and algorithms for automata and rational expressions. However, it offers no support for syntactic monoids at all.  +
The classical theory of automata, of transducers and of rational expressions, admits a very elegant and extremely useful extension (eg, in natural language processing) taking into account the concept of weighting. The weights are then taken in a semiring, which can be classical (⟨𝔹, ∨, ∧⟩, ⟨ℤ, +, ×⟩, ⟨ℚ, +, ×⟩, etc..), tropical (⟨ℤ, min, +⟩, etc..), or yet of another type (e.g. rational expressions). Automata are heavily used in computational linguistics, and conversely, automata used in computational linguistics are "heavy". Vcsn is a project led by Alexandre Duret-Lutz and Akim Demaille (LRDE). It is a platform for the manipulation of automata, transducers and weighted rational expressions. It is written in C++11 avoiding the classical object-oriented programming in favor of generic programming (template) for more performance. Vcsn is an heir of the Vaucanson 2 project which was developed in partnership with Jacques Sakarovitch (Telecom ParisTech) and Sylvain Lombardy (LaBRI). Vcsn has a sound base of data structure and algorithms for automata and rational expressions. It is already able to deal with many of the typical needs of linguists. However some specific semirings have not been implemented, and some well-known algorithms are needed.  +
The formal method community uses several types of automata over infinite words (called "omega-automata"): Büchi automata, Streett automata, Rabin automata... These automata differ by their acceptance condition, i.e., the condition under which an infinite run of the automaton is accepted. For each of these different acceptance conditions there exist specialized algorithms, for instance to decide if an automaton is accepting, or to change an acceptance condition into another, or to determinize an automaton... We have recently defined file format for exchanging omega-automata between tools. This format can represent all the above types of automata thanks to a very general way to to represent the acceptance condition. In fact the acceptance condition specification is so general that it allows us to represent combination of existing conditions.  +
Automatic text localization in natural images (still or moving) is an essential task in many applications, including automatic indexing of documents or photographs, the dematerialization of paper-based documents, assistance to visually impaired people, etc..  +
La localisation automatique de texte dans des images naturelles (fixes ou animées) est une fonction essentielle dans de nombreuses applications, notamment l’indexation automatique de documents ou photographies, la dématérialisation de données papier, l’assistance aux personnes malvoyantes, etc.  +
This internship is part of the “genericity and efficiency” research line of the laboratory. Many software tools for image processing are designed with performance issues in mind, related to either the data (many images or videos, or very large ones), the context (real-time constraints, the need to obtain a response in a “reasonable” time frame), or hardware (limited processing power or memory capacity). Besides, more and more software libraries for image processing are built along the lines of an advanced design work, using “abstractions” representing the various concepts of the domain (image, point, value, neighborhood, etc. ). This approach enables a high-level strategy to write image processing algorithms, which are reusable (not restricted to a single use case) and often simpler. Software frameworks from this category are mostly based on object-oriented programming or generic programming (C++ templates, Java or C# generics). Tools that seek to resolve the two previous issues (being efficient while providing a general writing via abstractions) are much more uncommon. The [[Olena]] project, developed for more than fifteen years by the LRDE, proposes a library for generic image processing in C++, Milena, designed for writing reusable and efficient algorithms. It relies both on generic and object-oriented programming. The internship aims to explore ways to extend the capabilities of Milena in the field of high performance computing (in particular in “Big Data” contexts), while preserving its current generic- and abstraction-related features.  +
Ce stage s'inscrit dans l'axe « généricité et performance » du laboratoire. On peut constater d'une part que de nombreux outils logiciels pour le traitement d'image sont conçus en prenant en compte des problématiques de performance relatives aux données (images ou vidéos volumineuses ou nombreuses), au contexte (contraintes de temps réel, besoins d'obtenir une réponse dans un temps « raisonnable ») ou encore liée au matériel (puissance de calcul ou capacité mémoire limitée(s)). Par ailleurs, de plus en plus de bibliothèques logicielles pour le traitement d'images sont construites d'après une modélisation avancée mettant en œuvre des ''abstractions'' représentant les différentes notions du domaine (image, point, valeur, voisinage, etc.). Cette approche permet une écriture « haut niveau » d'algorithmes de traitement d'images, réutilisables (non limités à un unique cas d'utilisation) et souvent plus simples. Les cadres logiciels (''software frameworks'') entrant dans cette catégorie s'appuient le plus souvent sur la programmation orientée objet ou la programmation générique (templates du C++, generics de Java ou C#). Il est cependant beaucoup plus rare d'observer des outils qui cherchent à répondre aux deux préoccupation précédentes (être performant tout en fournissant une écriture générale via des abstractions). Le projet [[Olena]], développé depuis une quinzaine d'années au LRDE, propose une bibliothèque de traitement d'images générique en C++, Milena, permettant l'écriture d'algorithmes réutilisables et performants. Elle s'appuie à la fois sur la programmation générique et la programmation orientée objet. Le stage proposé a pour objet l'exploration de pistes pour étendre les capacités de Milena dans le domaine du calcul performant (notamment dans le contexte des « Big Data »), tout en préservant ses caractéristiques de généricité et d'abstraction actuelles.  +
Keywords: * image processing, * mathematical morphology, * tree-based reasoning, * algorithmic optimization.  +
Keywords: * image processing, * mathematical morphology, * tree-based reasoning, * algorithmic optimization.  +
Keywords: * image processing, * mathematical morphology (connected operators), * tree of shapes, * shaping  +
Keywords: * image processing, * mathematical morphology (connected operators), * tree of shapes, * shaping  +
Keywords: * image processing, * mathematical morphology, * tree-based reasoning, * algorithmic optimization.  +
Keywords: * image processing, * mathematical morphology, * tree-based reasoning, * algorithmic optimization.  +
Différentes techniques de vérification formelle utilisent des formules de logique temporelle pour spécifier des comportements attendus. Par exemple la logique temporelle à temps linéaire (LTL) augmente la logique booléenne classique en y ajoutant des opérateurs temporels tels que F(x) (dans le futur x sera vrai), G(x) (x est toujours vrai), ou x U y (x est vrai jusqu'à ce que y le soit). De telles formules sont ensuite traduites sous forme d'ω-automates, typiquement des automates de Büchi, avant de réaliser un processus de vérification. Les applications d'une telle transformation sont nombreuses: model checking, synthèse de contrôleur, génération de tests, etc.  +
Les ω-automates sont des automates représentant des mots de longueur infinie. Le projet Spot propose différent outils et algorithmes pour la manipulation de ces automates. Pour le moment tous ces algorithmes sont écrits de façon séquentielle, parfois en utilisant des structures de données symboliques (par exemple des diagrammes de décision binaires).  +
Les ω-automates sont des automates qui reconnaissent des mots infinis. Comme ces automates ont un nombre fini d'états, ils utilisent une *condition d'acceptation* pour décider quels chemins sont acceptants ou rejetants. Des conditions d'acceptation classiques sont connues sous le nom de conditions de Büchi, de Rabin, de Streett, de Muller, de parité, etc. Elle correspondent à des contraintes sur des ensembles d'états qui doivent être visités infiniment souvent, ou finiment souvent. On peut aussi faire porter ces conditions sur des ensembles de transitions. Depuis 2014, de nombreux outils académiques produisant des ω-automates se sont accordés sur l'utilisation d'un format d'échange textuel, le format HOA (Hanoi Omega Automata). Dans ce format, les conditions d'acceptation sont spécifiées, non pas par leur nom, mais sous la forme d'une formule Booléenne exprimant exactement quels ensembles d'états (ou de transitions) doivent être vus finiment souvent ou infiniment souvent. Par exemple une condition de Rabin avec 2 paires pourra être exprimée sous la forme (Fin(0)&Inf(1))|(Fin(2)&Inf(3)) signifiant que soit les ensembles (d'états ou transitions) numérotés 0 et 1 doivent être vus respectivement finiment et infiniment souvent, soit ensembles 2 et 3 sont vus finiment et infiniment souvent. Ce type de formule d'acceptation permet de représenter toutes les conditions nommées précédemment, ainsi que toutes leurs combinaisons booléennes. Ces dernières n'ont pas forcément de nom, et peuvent ne pas avoir été étudiées. Une telle expressivité avait déjà été étudiée par Emerson et Lei (1987), avec une classe d'automates nommée ensuite par d'autres auteurs les "EL-automata". On leur doit quelques résultats comme le fait que le test du vide d'un automate "EL" est NP-complet. L'absence d'applications concrètes, d'outillage, et la dominance des conditions d'acceptation plus simples (Büchi, Streett, Rabin, parité) a probablement contribué a faire tomber les automates EL dans l'oubli. Aujourd'hui, le contexte est différent. Le format HOA permet de représenter les automates EL (en les généralisant un peu, car il autorise les conditions d'acceptation à porter sur les transitions au lieu des états, ainsi que les automates alternants). De nouvelles conditions d'acceptations sont apparues. Par exemple l'utilisation d'une version généralisées de la condition d'acceptation de Rabin permet de gagner des ordres de grandeur en model checking probabiliste. Plusieurs outils existent pour traduire des formules de logique en ω-automates dont la condition d'acceptation est choisie pour tenter de réduire le nombre d'états. Il devient donc utile d'avoir des logiciels capables de manipuler des ω-automates avec toutes formes de conditions d'acceptation : c'est ce que cherche à faire le projet Spot.  
Climb est une bibliothèque de traitement d'image écrite en Common Lisp. Elle est actuellement pourvue d'une interface graphique permettant de concevoir des chaînes de traitement d'images (Cf. capture d'écran) visuellement et à la souris, c'est-à-dire sans avoir besoin de recourir à de la programmation. Ceci est particulièrement utile pour des « clients » non informaticiens. L'interface en question a été développée assez rapidement pour des besoin de démonstration, mais n'est pas une solution satisfaisante sur le long terme. L'interface elle-même est limitée en fonctionnalités, peu ergonomique, pas très aguichante ni bien intégrée avec les différentes plateformes. De plus, Gtk2 est un toolkit ancien dont la couche d'interfaçage avec Lisp n'est plus vraiment maintenue.  +