Dans ce mémoire, je présente une technique pour combiner du code de bas niveau à un langage purement fonctionnel avec types dépendants. Par code de bas niveau, je veux dire n’importe quel programme écrit dans un langage qui permet le contrôle direct des ressources de la machine. En particulier, ce texte s’intéresse à la gestion de la mémoire. Plus concrètement, un programmeur C contrôle l’endroit et le moment où un bloc de mémoire est alloué, ainsi que la façon dont l’objet est initialisé. Par exemple, on peut allouer de l’espace sur la pile pour immédiatement l’initialiser avec un memcpy. Alternativement, on peut allouer un bloc sur le tas et l’initialiser champ par champ plus tard. Pour certaines applications où la mémoire est limitée ou la performance importante, ce choix est important. Un tel niveau de contrôle n’est pas disponible dans les langages de haut niveau, sauf pour quelques exceptions. Les langages fonctionnels comme OCaml ou Haskell découragent ou même interdisent de modifier les champs d’un objet. C’est encore plus vrai pour les langages à types dépendants où la mutation est l’éléphant dans le magasin de porcelaine de la cohérence. C’est un choix de design intentionnel. Un programme pur est plus facile à comprendre et analyser, mais comment séparer l’initialisation de l’allocation quand un objet ne peut pas changer ? Ce mémoire essaie de démontrer que ce n’est pas parce que c’est impossible, mais parce que ces langages ne sont pas habituellement utilisés dans un contexte où c’est nécessaire. Par contre, ce n’est pas facile non plus. Pour garantir la sécurité et la cohérence, il faut modéliser l’état d’un objet partiellement initialisé au niveau des types, ce que la plupart des langages ont de la peine à faire. La combinaison du manque de nécessité et de la lourdeur syntaxique et conceptuelle est la raison pour laquelle cette fonctionnalité est souvent absente. Pour y parvenir, nous prenons un langage à types dépendants, Typer, et nous y ajoutons le nécessaire pour récupérer une partie du contrôle abandonné dans le design original. Nous permettons au programmeur d’allouer des blocs de mémoire et de les initialiser graduellement plus tard, sans compromettre les propriétés de sécurité du programme. Concrètement, nous utilisons les monades, un concept de la théorie des catégories déjà utilisé pour la modélisation d’effets de bord, pour limiter les mutations aux endroits sécuritaires. / In this thesis, I will demonstrate how to combine low-level code with dependent types. By low-level code, I mean any program authored in a language that allows direct control of computer resources. In particular, this text will focus on memory management. Specifically, a C programmer has control over the location and time when a block of memory is allocated, as well as how it is initialized. For instance, it is possible to allocate stack space to immediately initialize it with an invocation of memcpy. Alternatively, one can allocate heap spate and initialize it field by field later. For some applications where memory is constrained or performance is important, this choice can matter. This level of control is not available in high-level languages, barring a few exceptions. Functional languages such as OCaml or Haskell discourage or simply forbid the mutation of objects. This is especially the case in dependently typed languages where mutation is the bull in the china shop of consistency. This is a deliberate choice as a pure program is easier to understand and reason about. However, having allocation and initialization done in two distinct steps seems impossible in this situation. This thesis shows that this is not impossible, it is simply done this way because these kinds of languages are seldom used in a context where such control is necessary. This does not mean though that adding this feature is easy. If we are to guarantee both safety and consistency, we need to keep track of the initialization state at the type level. Most languages struggle to do this. Language designers simply forgo this feature because it is not useful to them in addition to being difficult to use. To achieve it, we start with a dependently typed language, Typer, and add back the mechanisms necessary to recover the control relinquished in the original design. We let the programmer allocate blocks of memory to initialize later, without compromising the safety properties of the program. Specifically, we use monads, a concept from category theory, a know technique to model side effects, to limit mutation to situations where it is safe.

Maintaining any software is difficult. Whenever an evolutionary change is made to the base version of a program and the new version of the program is created, changes made to the base version of the software must be made to the new version. The answer is to build the software initially with the knowledge that it will change and that the base version will evolve. In other words, change-merging of software is a possible solution. All the work in this area has been done on program integration, change-merging of PSDL programs and software prototypes. The present work explores the possibility of combining the results of two independent updates of an abstract data type into a merged version that is both correct and safe. This report describes a developing theory for semantics-based change-merging of abstract data types.

Ce travail décrit l’ajout des types quotients dans Typer, un langage avec des types dépendants. Les types quotients permettent aux programmeurs de construire de nouveaux types à base des types existants en redéfinissant la notion d’égalité du type de départ. Typiquement, cela repose sur des relations d’équivalence définies sur le type de base. Les termes qui sont équivalents selon la relation sont donc vus comme égaux dans le type quotient résultant. Par exemple, les nombres rationnels peuvent être définis comme le quotient des paires d’entiers par une relation d’équivalence basée sur le produit en croix. Pour accueillir l’ajout des types quotients dans Typer, on a redéfini et amélioré l’égalité intégré de Typer en s’inspirant de la théorie des types cubique qui a introduit le type d’intervalle et aussi les assistants de preuve qui l’implémentent. De ce fait, la nouvelle égalité de Typer est basé sur les fonctions qui ont comme argument notre nouvelle primitive d’intervalle. Une telle égalité est plus puissante et expressive, elle se prête bien à la construction des preuves liées aux types quotients. Dans ce travail, on s’intéresse également au côté pratique de l’utilisation des types quotients dans un langage tel que Typer, à la fois en termes d’efficacité d’exécution et de facilité d’utilisation pour les développeurs. Les types quotients ne sont pas offerts dans la plupart des langages avec des types dépendants principalement parce que leur utilisation nous entraîne à des obligations de preuves pénibles. Pour faciliter l’utilisation des types quotients, on a fourni une bibliothèque qui simplifie la manipulation des types quotients. On a profité de cette nouvelle addition au langage pour introduire de nouvelles primitives, telle que les nombres rationnels, la troncation propositionnelle, etc. Finalement, ce travail étudie également le développement des preuves en Typer. À notre connaissance, ceci est la première tentative d’écrire une quantité importante de preuves en Typer puisque le langage se veut un langage de programmation à usage général. On décrit notre expérience et les défis auxquels on a dû faire face en cours de route. En outre, on a introduit de nouvelles primitives pour faciliter le développement de preuves en Typer. / This work describes the introduction of quotient types to Typer, a dependently-typed programming language. Quotient types allow programmers to construct new types based on existing types by redefining the notion of equality of the base type. This is typically based on equivalence relations defined on the base type. Terms that are equivalent according to the relation are thus treated as equal in the resulting quotient type. For instance, rational numbers may be defined as the quotient of pairs of integers under an equivalence relation based on cross-multiplication. To better accommodate the introduction of quotient types to Typer, we revamped the built-in equality type by drawing inspiration from cubical type theory that features the interval type and proof assistants that implement it. As such, Typer’s new equality type is based on functions that have our new interval primitive as an argument. Such an equality type is more powerful and expressive, it notably lends itself well to the writing of proofs related to quotient types. In this work, we also investigate the practicality of the usage of quotient types in a language such as Typer, both in terms of run-time efficiency and developer-friendliness. Quotient types do not exist in most modern dependently typed languages, principally because their usage entails burdensome proof obligations. To facilitate the usage of quotient types, we provide a library that helps simplify the manipulation of quotient types. We also leverage this new addition to the language to introduce new built-in types, such as rational numbers, propositional truncation, etc. Finally, this work also explores the development of proofs in Typer, to our knowledge this is the first attempt to write a substantial amount of proofs using the language since the language is primarily intended to be a general-purpose programming language. We describe our experience and the challenges faced in the process. Additionally, we introduce several constructs to streamline proof development in Typer.

Cette thèse décrit comment l'ajout de trois ingrédients à Système Fω permet d'écrire des programmes de façon modulaire dans un système explicite à la Church, tout en gardant un style proche des modules de ML. Le premier chapitre s'intéresse aux types existentiels ouverts, qui confèrent la possibilité d'utiliser des types existentiels sans restriction de portée : cela offre une plus grande flexibilité dans l'organisation des programmes. Le deuxième chapitre est consacré à l'étude des kinds singletons, qui modélisent les définitions de types : dans ce cadre, on donne une caractérisation simple de l'équivalence de types, fondée sur une relation de réduction confluente et fortement normalisante. Le dernier chapitre intègre les deux notions précédentes dans un langage noyau muni d'une relation de sous-typage : cela apporte à Fω un gain de modularité important, de niveau comparable à celui des modules de ML. Une traduction des modules vers ce langage est esquissée, permettant une comparaison précise des deux langages.

De la peau de l’être humain aux écrans d'ordinateur et d'eBook en passant parl'argile, les papyrus, la peau des animaux et le papier, les supports de l'écrit ont varié etévolué tout au long de ces siècles. Le lecteur a dû s'adapter à cette évolution des supports et,par là, de l'écriture et il a changé sa manière de lire.Avec la diffusion des nouvelles technologies, leur présence incontournable dansnotre quotidien et l'apparition de nouveaux outils comme l'eBook et l'iPad, cette rechercheexploratoire s'est intéressée aux changements de stratégies utilisées par des étudiantsuniversitaires qui lisent en situation d'apprentissage du Français Langue Etrangère surdifférents supports : l'écran d'ordinateur, le livre électronique et le support papier.Les types de discours sont également pris en compte. La nouvelle, qui relève dudiscours du raconter, et l'article d'opinion journalistique, qui relève du discours de l'exposer,ont également influencé les stratégies de reconstruction du sens des textes lus. Pour le recueildes données, les principaux outils d'investigation ont été le questionnaire et l'entretien.L'analyse du corpus a débouché sur l'établissement de figures de lecteurs et la miseen évidence de la manière de lire. Sur le plan didactique, ce travail met l'accent surl'importance de l'enseignement des stratégies en fonction des supports et des types dediscours dans le cadre de l'apprentissage d'une langue étrangère ou non. / From human skin to computer screens and eBooks, with clay, papyrus, animal skinsand paper in between writing materials have varied and evolved throughout the centuries.Readres have had to adapt to this evolution in the materials and the wrinting and they havechanged the way they read.With the wide spread use of new technologies and their omnipresence in our dailylives, the arrival of new tools, such as the eBook or the iPad. This study has sought to explorethe changes in the strategies used by university students learning French as a foreignlanguage. When reading with different reading materials : the computer screen, the eBook orpaper.The types of discourse have also been taken into consideration. The short story andthe newspaper editorial influence the strategies of the reconstruction of the meaning of thetexts that were read. To gather the data, the main tolls of investigation were questionnairesand interviews.The analysis of this data has permitted us to establish readers' types and to showhow they read. This study insists on the importance of teaching strategies that take intoconsideration the materials being used as well as the types of discouse being read, whetherin language learning or not.

The objectives of the study were: (1) to determine whether staff and leaders differ significantly in terms of their perceptions of leaders’ emotional intelligence and retention factors; (2) to investigate the relationship between personality types (as measured by the Myers-Briggs Type Indicator), emotional intelligence (as measured by the Emotional Competency Profiler), and retention factors (as measured by the Retention Factor Scale); and (3) to determine whether demographical groups differ significantly in terms of the retention factor variables. A non-probability purposive sample of 160 working adults from an organisation within the asset management industry participated in the study. The research findings indicated that there is a difference in terms of leaders’ and staff’s perceptions of leaders’ emotional intelligence and retention factors. There is a relationship between leaders’ personality types, emotional intelligence and retention factors. Biographical groups (gender, race and age groups, and business units) differed in terms of the retention factors. The findings contributed valuable new knowledge that may be used for organisational retention practices. / Industrial and Organisational Psychology

Based on a natural unification of logic and computation, Martin-Löf’s intuitionistic type theory can be regarded simultaneously as a computationally meaningful higher-order logic system and an expressively typed functional programming language, in which proofs and programs are treated as the same entities. Two modes of programming can then be distinguished: in externalism, we construct a program separately from its correctness proof with respect to a given specification, whereas in internalism, we encode the specification in a sophisticated type such that any program inhabiting the type also encodes a correctness proof, and we can use type information as a guidance on program construction. Internalism is particularly effective in the presence of inductive families, whose design can have a strong influence on program structure. Techniques and mechanisms for facilitating internalist programming are still lacking, however. This dissertation proposes that internalist programming can be facilitated by exploiting an interconnection between internalism and externalism, expressed as isomorphisms between inductive families into which data structure invariants are encoded and their simpler variants paired with predicates expressing those invariants. The interconnection has two directions: one analysing inductive families into simpler variants and predicates, and the other synthesising inductive families from simpler variants and specific predicates. They respectively give rise to two applications, one achieving a modular structure of internalist libraries, and the other bridging internalist programming with relational specifications and program derivation. The datatype-generic mechanisms supporting the applications are based on McBride’s ornaments. Theoretically, the key ornamental constructs — parallel composition of ornaments and relational algebraic ornamentation — are further characterised in terms of lightweight category theory. Most of the results are completely formalised in the Agda programming language.

Le texte poétique devient, au XXe siècle, de plus en plus difficile à définir. Il a perdu plusieurs attributs qui aidaient autrefois à le caractériser (vers, rimes, parallélismes), et ne se laisse pas non plus circonscrire par le biais du lyrisme : bon nombre de poètes, en effet, ont abandonné le programme de la "poésie pure" pour renouer avec un art descriptif, narratif ou argumentatif. Dès lors, faut-il considérer que l'organisation poétique n'est qu'une structure de surface qui se surajoute à un type de texte de base, en entraînant certaines conséquences sur le plan sémantique et grammatical ? N'existe-t-il pas malgré tout des propriétés typiques de l'oeuvre poétique, qui permettent d'instaurer un rapport tout à fait particulier entre le lecteur, le langage et le monde ? Nous avons voulu nous pencher sur ces questions en explorant le phénomène de l'hétérogénéité discursive chez quelques poètes francophones du XXe siècle. Nous constaterons que ceux-ci n'hésitent pas à décrire, à raconter ou à argumenter, mais nous verrons aussi que la poésie tend à transfigurer les schémas de base auxquels elle s'allie, si bien qu'un récit en vers n'est pas du tout semblable à son homologue en prose. C'est par cet angle d'approche que nous espérons contribuer à faire mieux comprendre le mystère poétique, qui déroute terriblement les jeunes lecteurs.

No description available.

A concurrent system is a computer system with components that run in parallel and interact with each other. Such systems are ubiquitous and are notably responsible for supporting the infrastructure for transport, commerce and entertainment. They are very difficult to design and implement correctly: many different modeling languages and verification techniques have been devised to reason about them and verifying their correctness. However, existing languages and techniques can only express a limited range of systems and properties. In this dissertation, we address some of the shortcomings of established models and theories in four ways: by introducing a general modal logic, extending a modelling language with types and a more general operation, providing an automated tool support, and adapting an established behavioural type theory to specify and verify systems with unreliable communication. A modal logic for transition systems is a way of specifying properties of concurrent system abstractly. We have developed a modal logic for nominal transition systems. Such systems are common and include the pi-calculus and psi-calculi. The logic is adequate for many process calculi with regard to their behavioural equivalence even for those that no logic has been considered, for example, CCS, the pi-calculus, psi-calculi, the spi-calculus, and the fusion calculus. The psi-calculi framework is a parametric process calculi framework that subsumes many existing process calculi. We extend psi-calculi with a type system, called sorts, and a more general notion of pattern matching in an input process. This gives additional expressive power allowing us to capture directly even more process calculi than was previously possible. We have reestablished the main results of psi-calculi to show that the extensions are consistent. We have developed a tool that is based on the psi-calculi, called the psi-calculi workbench. It provides automation for executing the psi-calculi processes and generating a witness for a behavioural equivalence between processes. The tool can be used both as a library and as an interactive application. Lastly, we developed a process calculus for unreliable broadcast systems and equipped it with a binary session type system. The process calculus captures the operations of scatter and gather in wireless sensor and ad-hoc networks. The type system enjoys the usual property of subject reduction, meaning that well-typed processes reduce to well-typed processes. To cope with unreliability, we also introduce a notion of process recovery that does not involve communication. This is the first session type system for a model with unreliable communication.