A Type-Preserving Compiler from System F to Typed Assembly Language

L'utilisation des méthodes formelles est de plus en plus courante dans le développement logiciel, et les systèmes de types sont la méthode formelle qui a le plus de succès. L'avancement des méthodes formelles présente de nouveaux défis, ainsi que de nouvelles opportunités. L'un des défis est d'assurer qu'un compilateur préserve la sémantique des programmes, de sorte que les propriétés que l'on garantit à propos de son code source s'appliquent également au code exécutable. Cette thèse présente un compilateur qui traduit un langage fonctionnel d'ordre supérieur avec polymorphisme vers un langage assembleur typé, dont la propriété principale est que la préservation des types est vérifiée de manière automatisée, à l'aide d'annotations de types sur le code du compilateur. Notre compilateur implante les transformations de code essentielles pour un langage fonctionnel d'ordre supérieur, nommément une conversion CPS, une conversion des fermetures et une génération de code. Nous présentons les détails des représentation fortement typées des langages intermédiaires, et les contraintes qu'elles imposent sur l'implantation des transformations de code. Notre objectif est de garantir la préservation des types avec un minimum d'annotations, et sans compromettre les qualités générales de modularité et de lisibilité du code du compilateur. Cet objectif est atteint en grande partie dans le traitement des fonctionnalités de base du langage (les «types simples»), contrairement au traitement du polymorphisme qui demande encore un travail substantiel pour satisfaire la vérification de type.

A Compiler for the dependently typed language Beluga

Les structures avec des lieurs sont très communes en informatique. Les langages de programmation et les systèmes logiques sont des exemples de structures avec des lieurs. La manipulation de lieurs est délicate, de sorte que l’écriture de programmes qui ma- nipulent ces structures tirerait profit d’un soutien spécifique pour les lieurs. L’environ- nement de programmation Beluga est un exemple d’un tel système. Nous développons et présentons ici un compilateur pour ce système. Parmi les programmes pour lesquels Beluga est spécialement bien adapté, plusieurs peuvent bénéficier d’un compilateur. Par exemple, les programmes pour valider les types (les "type-checkers"), les compilateurs et les interpréteurs tirent profit du soutien spécifique des lieurs et des types dépendants présents dans le langage. Ils nécessitent tous également une exécution efficace, que l’on propose d’obtenir par le biais d’un compilateur. Le but de ce travail est de présenter un nouveau compilateur pour Beluga, qui emploie une représentation interne polyvalente et permet de partager du code entre plusieurs back-ends. Une contribution notable est la compilation du filtrage de Beluga, qui est particulièrement puissante dans ce langage.

Caractéristiques et origine fonctionnelle des propriétés fréquentielles du noeud auriculoventriculaire

Le nœud auriculoventriculaire (AV) joue un rôle vital dans le cœur normal et pathologique. Il connecte les oreillettes aux ventricules et, grâce à sa conduction lente, génère un délai entre les contractions auriculaire et ventriculaire permettant d’optimiser le pompage sanguin. Sa conduction lente et sa longue période réfractaire font du nœud AV un filtre d’impulsions auriculaires lors de tachyarythmies assurant ainsi une fréquence ventriculaire plus lente favorable au débit cardiaque. L’optimisation de ce filtrage est une cible dans le traitement de ces arythmies. Malgré ce rôle vital et de nombreuses études, le nœud AV demeure l’objet de plusieurs controverses qui en rendent la compréhension laborieuse. Nos études expérimentales sur des préparations isolées de cœurs de lapin visent à apporter des solutions à certains des problèmes qui limitent la compréhension des propriétés fréquentielles du nœud AV. Le premier problème concerne la définition de la propriété de récupération nodale. On s’accorde généralement sur la dépendance du temps de conduction nodale (intervalle auriculo-Hissien, AH) du temps de récupération qui le précède mais un débat presque centenaire persiste sur la façon de mesurer ce temps de récupération. Selon que l’on utilise à cette fin la longueur du cycle auriculaire (AA) ou l’intervalle His-auriculaire précédent (HA), la même réponse nodale montre des caractéristiques différentes, un paradoxe à ce jour inexpliqué. Le temps de conduction nodale augmente aussi avec le degré et la durée d'une fréquence rapide, un phénomène appelé fatigue. Or, les caractéristiques de la fatigue mesurée varient avec l’indice de récupération utilisé (AA vs. HA). De plus, une troisième propriété appelée facilitation qui entraîne un raccourcissement du temps de conduction diffère aussi avec l’indice de récupération utilisé. Pour établir l’origine de ce problème, nous avons déterminé les différences entre les courbes de récupération (AH compilé en fonction du AA ou HA) pour 30 états fonctionnels nodaux différents. Ces conditions étaient obtenues à l’aide de protocoles permettant la variation du cycle de base (BCL) et du cycle prétest (PTCL), deux paramètres connus pour altérer la fonction nodale. Nous avons pu établir que pour chaque état fonctionnel, la forme de la courbe de récupération et le niveau de fatigue étaient les mêmes pour les deux indices de récupération. Ceci s’applique aussi aux données obtenues à des BCL et PTCL égaux comme dans les protocoles de stimulation prématurée conventionnels couramment utilisés. Nos résultats ont établi pour la première fois que les propriétés nodales de récupération et de fatigue sont indépendantes de l’indice de récupération utilisé. Nos données montrent aussi que les différences entre les courbes de récupération en fonction de l’indice utilisé proviennent d’effets associés aux variations du PTCL. Notre deuxième étude établit à partir des mêmes données pourquoi les variations du PTCL altèrent différemment les courbes de récupération selon l’indice utilisé. Nous avons démontré que ces différences augmentaient en proportion directe avec l’augmentation du temps de conduction au battement prétest. Cette augmentation cause un déplacement systématique de la courbe construite avec l’intervalle AA vers la droite et de celle construite avec l’intervalle HA vers la gauche. Ce résultat met en évidence l’importance de tenir compte des changements du temps de conduction prétest dans l’évaluation de la fonction nodale, un paramètre négligé dans la plupart des études. Ce résultat montre aussi que chacun des deux indices a des limites dans sa capacité d’évaluer le temps de récupération nodale réel lorsque le temps de conduction prétest varie. Lorsque ces limites sont ignorées, comme c’est habituellement le cas, elles entraînent un biais dans l’évaluation des effets de fatigue et de facilitation. Une autre grande difficulté dans l’évaluation des propriétés fréquentielles du nœud AV concerne son état réfractaire. Deux indices sont utilisés pour évaluer la durée de la période réfractaire nodale. Le premier est la période réfractaire efficace (ERPN) définie comme l’intervalle AA le plus long qui n’est pas conduit par le nœud. Le deuxième est la période réfractaire fonctionnelle (FRPN) qui correspond à l’intervalle minimum entre deux activations mesurées à la sortie du nœud. Paradoxalement et pour des raisons obscures, l’ERPN augmente alors que la FRPN diminue avec l’augmentation de la fréquence cardiaque. De plus, ces effets varient grandement avec les sujets, les espèces et l’âge. À partir des mêmes données que pour les deux autres études, nous avons cherché dans la troisième étude l’origine des variations fréquentielles de l’ERPN et de la FRPN. Le raccourcissement du BCL prolonge l’ERPN mais n’affecte pas la FRPN. L’allongement de l’ERPN provient principalement d’un allongement du temps de conduction prétest. Un PTCL court en comparaison avec un BCL court allonge encore plus substantiellement le temps de conduction prétest mais raccourcit en même temps l’intervalle His-auriculaire, ces deux effets opposés s’additionnent pour produire un allongement net de l’ERPN. Le raccourcissement de l’intervalle His-auriculaire par le PTCL court est aussi entièrement responsable pour le raccourcissement de la FRPN. Nous avons aussi établi que, lorsque la composante du temps de conduction prétest est retirée de l’ERPN, un lien linéaire existe entre la FRPN et l’ERPN à cause de leur dépendance commune de l’intervalle His-auriculaire. Le raccourcissement combiné du BCL et du PTCL produit des effets nets prévisibles à partir de leurs effets individuels. Ces effets reproduisent ceux obtenus lors de protocoles prématurés conventionnels. Ces observations supportent un nouveau schème fonctionnel des variations fréquentielles de l’ERPN et de la FRPN à partir des effets distincts du BCL et du PTCL. Elles établissent aussi un nouveau lien entre les variations fréquentielles de l’ERPN et de la FRPN. En conclusion, la modulation fréquentielle de la fonction du nœud AV provient de la combinaison d’effets concurrents cumulatifs liés au cycle de base et non-cumulatifs liés au cycle prétest. Ces effets peuvent être interprétés de façon consistante indépendamment de l’indice de récupération en tenant compte des changements du temps de conduction au battement prétest. Les effets fréquentiels disparates sur l’ERPN et la FRPN sont aussi grandement liés aux changements du temps de conduction prétest. Lorsque l’analyse tient compte de ce facteur, l’ERPN et la FRPN montrent des variations parallèles fortement liées à celles de l’intervalle His-auriculaire. Le nouveau schème fonctionnel des propriétés fréquentielles du nœud AV supporté par nos données aidera à mieux cibler les études sur les mécanismes cellulaires contrôlant la modulation fréquentielle nodale. Nos données pourraient aider à l’interprétation et au contrôle des réponses nodales diverses associées aux tachyarythmies supraventriculaires et à leur traitement pharmacologique. En bref, nos travaux supportent une compréhension factuelle améliorée du comportement fréquentiel du nœud AV, un domaine aux applications multiples en rythmologie cardiaque.

Incorporating complex cells into neural networks for pattern classification

Dans le domaine des neurosciences computationnelles, l'hypothèse a été émise que le système visuel, depuis la rétine et jusqu'au cortex visuel primaire au moins, ajuste continuellement un modèle probabiliste avec des variables latentes, à son flux de perceptions. Ni le modèle exact, ni la méthode exacte utilisée pour l'ajustement ne sont connus, mais les algorithmes existants qui permettent l'ajustement de tels modèles ont besoin de faire une estimation conditionnelle des variables latentes. Cela nous peut nous aider à comprendre pourquoi le système visuel pourrait ajuster un tel modèle; si le modèle est approprié, ces estimé conditionnels peuvent aussi former une excellente représentation, qui permettent d'analyser le contenu sémantique des images perçues. Le travail présenté ici utilise la performance en classification d'images (discrimination entre des types d'objets communs) comme base pour comparer des modèles du système visuel, et des algorithmes pour ajuster ces modèles (vus comme des densités de probabilité) à des images. Cette thèse (a) montre que des modèles basés sur les cellules complexes de l'aire visuelle V1 généralisent mieux à partir d'exemples d'entraînement étiquetés que les réseaux de neurones conventionnels, dont les unités cachées sont plus semblables aux cellules simples de V1; (b) présente une nouvelle interprétation des modèles du système visuels basés sur des cellules complexes, comme distributions de probabilités, ainsi que de nouveaux algorithmes pour les ajuster à des données; et (c) montre que ces modèles forment des représentations qui sont meilleures pour la classification d'images, après avoir été entraînés comme des modèles de probabilités. Deux innovations techniques additionnelles, qui ont rendu ce travail possible, sont également décrites : un algorithme de recherche aléatoire pour sélectionner des hyper-paramètres, et un compilateur pour des expressions mathématiques matricielles, qui peut optimiser ces expressions pour processeur central (CPU) et graphique (GPU).

Criteria for the validation of specialized verb equivalents : application in bilingual terminography

Multilingual terminological resources do not always include valid equivalents of legal terms for two main reasons. Firstly, legal systems can differ from one language community to another and even from one country to another because each has its own history and traditions. As a result, the non-isomorphism between legal and linguistic systems may render the identification of equivalents a particularly challenging task. Secondly, by focusing primarily on the definition of equivalence, a notion widely discussed in translation but not in terminology, the literature does not offer solid and systematic methodologies for assigning terminological equivalents. As a result, there is a lack of criteria to guide both terminologists and translators in the search and validation of equivalent terms. This problem is even more evident in the case of predicative units, such as verbs. Although some terminologists (L‘Homme 1998; Lerat 2002; Lorente 2007) have worked on specialized verbs, terminological equivalence between units that belong to this part of speech would benefit from a thorough study. By proposing a novel methodology to assign the equivalents of specialized verbs, this research aims at defining validation criteria for this kind of predicative units, so as to contribute to a better understanding of the phenomenon of terminological equivalence as well as to the development of multilingual terminography in general, and to the development of legal terminography, in particular. The study uses a Portuguese-English comparable corpus that consists of a single genre of texts, i.e. Supreme Court judgments, from which 100 Portuguese and 100 English specialized verbs were selected. The description of the verbs is based on the theory of Frame Semantics (Fillmore 1976, 1977, 1982, 1985; Fillmore and Atkins 1992), on the FrameNet methodology (Ruppenhofer et al. 2010), as well as on the methodology for compiling specialized lexical resources, such as DiCoInfo (L‘Homme 2008), developed in the Observatoire de linguistique Sens-Texte at the Université de Montréal. The research reviews contributions that have adopted the same theoretical and methodological framework to the compilation of lexical resources and proposes adaptations to the specific objectives of the project. In contrast to the top-down approach adopted by FrameNet lexicographers, the approach described here is bottom-up, i.e. verbs are first analyzed and then grouped into frames for each language separately. Specialized verbs are said to evoke a semantic frame, a sort of conceptual scenario in which a number of mandatory elements (core Frame Elements) play specific roles (e.g. ARGUER, JUDGE, LAW), but specialized verbs are often accompanied by other optional information (non-core Frame Elements), such as the criteria and reasons used by the judge to reach a decision (statutes, codes, previous decisions). The information concerning the semantic frame that each verb evokes was encoded in an xml editor and about twenty contexts illustrating the specific way each specialized verb evokes a given frame were semantically and syntactically annotated. The labels attributed to each semantic frame (e.g. [Compliance], [Verdict]) were used to group together certain synonyms, antonyms as well as equivalent terms. The research identified 165 pairs of candidate equivalents among the 200 Portuguese and English terms that were grouped together into 76 frames. 71% of the pairs of equivalents were considered full equivalents because not only do the verbs evoke the same conceptual scenario but their actantial structures, the linguistic realizations of the actants and their syntactic patterns were similar. 29% of the pairs of equivalents did not entirely meet these criteria and were considered partial equivalents. Reasons for partial equivalence are provided along with illustrative examples. Finally, the study describes the semasiological and onomasiological entry points that JuriDiCo, the bilingual lexical resource compiled during the project, offers to future users.

Étude de cas sur l’ajout de vecteurs d’enregistrements typés dans Gambit Scheme

Dans le but d’optimiser la représentation en mémoire des enregistrements Scheme dans le compilateur Gambit, nous avons introduit dans celui-ci un système d’annotations de type et des vecteurs contenant une représentation abrégée des enregistrements. Ces derniers omettent la référence vers le descripteur de type et l’entête habituellement présents sur chaque enregistrement et utilisent plutôt un arbre de typage couvrant toute la mémoire pour retrouver le vecteur contenant une référence. L’implémentation de ces nouvelles fonctionnalités se fait par le biais de changements au runtime de Gambit. Nous introduisons de nouvelles primitives au langage et modifions l’architecture existante pour gérer correctement les nouveaux types de données. On doit modifier le garbage collector pour prendre en compte des enregistrements contenants des valeurs hétérogènes à alignements irréguliers, et l’existence de références contenues dans d’autres objets. La gestion de l’arbre de typage doit aussi être faite automatiquement. Nous conduisons ensuite une série de tests de performance visant à déterminer si des gains sont possibles avec ces nouvelles primitives. On constate une amélioration majeure de performance au niveau de l’allocation et du comportement du gc pour les enregistrements typés de grande taille et des vecteurs d’enregistrements typés ou non. De légers surcoûts sont toutefois encourus lors des accès aux champs et, dans le cas des vecteurs d’enregistrements, au descripteur de type.

Studies on lipid production of microalgae under mixotrophic growth, utilizing glycerol as a carbon source, combined with nitrogen starvation

Rampant increases in oil prices and detrimental effects of fossil fuels on the environment have been the main impetus for the development of environmentally friendly and sustainable energy sources. Amongst the many possibilities, microalgae have been proposed as a new alternative energy source to fossil fuels, as their growth is both sustainable and ecologically safe. By definition, microalgae are unicellular photosynthetic microorganisms containing chlorophyll a. These organisms are capable of producing large quantities of oils, surpassing that of traditional oil-seed crops, which can be transformed, through chemical processes, into biofuels such as biodiesel or bio-gasoline. Thus, recent research has gone into discovering high lipid producing algal strains, optimising growth media for increased lipid production and developing metabolic engineering to make microalgae a source of biofuel that is competitive to more traditional sources of biofuel and even to fossil fuel. In this context, the research reported here focused on using a mixotrophic growth mode as a way to increase lipid production for certain strains of microalgae. In addition, nitrogen starvation combined with mixotrophy was studied to analyse its effects on lipid production. Mixotrophy is the parallel usage of two trophic modes, in our case photoautotrophy and heterotrophy. Consequently, 12 algal strains were screened for mixotrophic growth, using glycerol as a carbon source. Glycerol is a waste product of the current biodiesel industry; it is a cheap and abundant carbon source present in many metabolic pathways. From this initial screening, several strains were chosen for subsequent experiments involving nitrogen starvation. Nitrogen starvation has been shown to induce lipid accumulation. The results obtained show that a mixotrophic growth mode, using glycerol as a carbon source, enhances lipid production for certain strains. Moreover, lipid enhancement was shown for nitrogen starvation combined with mixotrophic growth mode. This was dependant on time spent under nitrogen starvation and on initial concentrations of the nitrogen source.

Abitbol : un langage sur mesure pour la métaprogrammation

Ce mémoire a pour thèse que les fonctions devraient être transparentes lors de la phase de métaprogrammation. En effet, la métaprogrammation se veut une possibilité pour le programmeur d’étendre le compilateur. Or, dans un style de programmation fonctionnelle, la logique du programme se retrouve dans les définitions des diverses fonctions le composant. Puisque les fonctions sont généralement opaques, l’impossibilité d’accéder à cette logique limite les applications possibles de la phase de métaprogrammation. Nous allons illustrer les avantages que procurent les fonctions transparentes pour la métaprogrammation. Nous donnerons notamment l’exemple du calcul symbolique et un exemple de nouvelles optimisations désormais possibles. Nous illustrerons également que la transparence des fonctions permet de faire le pont entre les datatypes du programme et les fonctions. Nous allons également étudier ce qu'implique la présence de fonctions transparentes au sein d'un langage. Nous nous concentrerons sur les aspects reliés à l'implantation de ces dernières, aux performances et à la facilité d'utilisation. Nous illustrerons nos propos avec le langage Abitbol, un langage créé sur mesure pour la métaprogrammation.

On the fly type specialization without type analysis

Les langages de programmation typés dynamiquement tels que JavaScript et Python repoussent la vérification de typage jusqu’au moment de l’exécution. Afin d’optimiser la performance de ces langages, les implémentations de machines virtuelles pour langages dynamiques doivent tenter d’éliminer les tests de typage dynamiques redondants. Cela se fait habituellement en utilisant une analyse d’inférence de types. Cependant, les analyses de ce genre sont souvent coûteuses et impliquent des compromis entre le temps de compilation et la précision des résultats obtenus. Ceci a conduit à la conception d’architectures de VM de plus en plus complexes. Nous proposons le versionnement paresseux de blocs de base, une technique de compilation à la volée simple qui élimine efficacement les tests de typage dynamiques redondants sur les chemins d’exécution critiques. Cette nouvelle approche génère paresseusement des versions spécialisées des blocs de base tout en propageant de l’information de typage contextualisée. Notre technique ne nécessite pas l’utilisation d’analyses de programme coûteuses, n’est pas contrainte par les limitations de précision des analyses d’inférence de types traditionnelles et évite la complexité des techniques d’optimisation spéculatives. Trois extensions sont apportées au versionnement de blocs de base afin de lui donner des capacités d’optimisation interprocédurale. Une première extension lui donne la possibilité de joindre des informations de typage aux propriétés des objets et aux variables globales. Puis, la spécialisation de points d’entrée lui permet de passer de l’information de typage des fonctions appellantes aux fonctions appellées. Finalement, la spécialisation des continuations d’appels permet de transmettre le type des valeurs de retour des fonctions appellées aux appellants sans coût dynamique. Nous démontrons empiriquement que ces extensions permettent au versionnement de blocs de base d’éliminer plus de tests de typage dynamiques que toute analyse d’inférence de typage statique.

Du terme prédicatif au cadre sémantique : méthodologie de compilation d'une ressource terminologique pour les termes arabes de l'informatique

La description des termes dans les ressources terminologiques traditionnelles se limite à certaines informations, comme le terme (principalement nominal), sa définition et son équivalent dans une langue étrangère. Cette description donne rarement d’autres informations qui peuvent être très utiles pour l’utilisateur, surtout s’il consulte les ressources dans le but d’approfondir ses connaissances dans un domaine de spécialité, maitriser la rédaction professionnelle ou trouver des contextes où le terme recherché est réalisé. Les informations pouvant être utiles dans ce sens comprennent la description de la structure actancielle des termes, des contextes provenant de sources authentiques et l’inclusion d’autres parties du discours comme les verbes. Les verbes et les noms déverbaux, ou les unités terminologiques prédicatives (UTP), souvent ignorés par la terminologie classique, revêtent une grande importance lorsqu’il s’agit d’exprimer une action, un processus ou un évènement. Or, la description de ces unités nécessite un modèle de description terminologique qui rend compte de leurs particularités. Un certain nombre de terminologues (Condamines 1993, Mathieu-Colas 2002, Gross et Mathieu-Colas 2001 et L’Homme 2012, 2015) ont d’ailleurs proposé des modèles de description basés sur différents cadres théoriques. Notre recherche consiste à proposer une méthodologie de description terminologique des UTP de la langue arabe, notamment l’arabe standard moderne (ASM), selon la théorie de la Sémantique des cadres (Frame Semantics) de Fillmore (1976, 1977, 1982, 1985) et son application, le projet FrameNet (Ruppenhofer et al. 2010). Le domaine de spécialité qui nous intéresse est l’informatique. Dans notre recherche, nous nous appuyons sur un corpus recueilli du web et nous nous inspirons d’une ressource terminologique existante, le DiCoInfo (L’Homme 2008), pour compiler notre propre ressource. Nos objectifs se résument comme suit. Premièrement, nous souhaitons jeter les premières bases d’une version en ASM de cette ressource. Cette version a ses propres particularités : 1) nous visons des unités bien spécifiques, à savoir les UTP verbales et déverbales; 2) la méthodologie développée pour la compilation du DiCoInfo original devra être adaptée pour prendre en compte une langue sémitique. Par la suite, nous souhaitons créer une version en cadres de cette ressource, où nous regroupons les UTP dans des cadres sémantiques, en nous inspirant du modèle de FrameNet. À cette ressource, nous ajoutons les UTP anglaises et françaises, puisque cette partie du travail a une portée multilingue. La méthodologie consiste à extraire automatiquement les unités terminologiques verbales et nominales (UTV et UTN), comme Ham~ala (حمل) (télécharger) et taHmiyl (تحميل) (téléchargement). Pour ce faire, nous avons adapté un extracteur automatique existant, TermoStat (Drouin 2004). Ensuite, à l’aide des critères de validation terminologique (L’Homme 2004), nous validons le statut terminologique d’une partie des candidats. Après la validation, nous procédons à la création de fiches terminologiques, à l’aide d’un éditeur XML, pour chaque UTV et UTN retenue. Ces fiches comprennent certains éléments comme la structure actancielle des UTP et jusqu’à vingt contextes annotés. La dernière étape consiste à créer des cadres sémantiques à partir des UTP de l’ASM. Nous associons également des UTP anglaises et françaises en fonction des cadres créés. Cette association a mené à la création d’une ressource terminologique appelée « DiCoInfo : A Framed Version ». Dans cette ressource, les UTP qui partagent les mêmes propriétés sémantiques et structures actancielles sont regroupées dans des cadres sémantiques. Par exemple, le cadre sémantique Product_development regroupe des UTP comme Taw~ara (طور) (développer), to develop et développer. À la suite de ces étapes, nous avons obtenu un total de 106 UTP ASM compilées dans la version en ASM du DiCoInfo et 57 cadres sémantiques associés à ces unités dans la version en cadres du DiCoInfo. Notre recherche montre que l’ASM peut être décrite avec la méthodologie que nous avons mise au point.