No description available.

This research involves the construction of a programming system, HASKEU, to support end-user programming in a purely functional programming language. An end-user programmer is someone who may program a computer to get their job done, but has no interest in becoming a computer programmer. A purely functional programming language is one that does not require the expression of statement sequencing or variable updating. The end-user is offered two views of their functional program. The primary view is a visual one, in which the program is presented as a collection of boxes (representing processes) and lines (representing data flow). The secondary view is a textual one, in which the program is presented as a collection of written function definitions. It is expected that the end-user programmer will begin with the visual view, perhaps later moving on to the textual view. The task of the programming system is to ensure that the visual and textual views are kept consistent as the program is constructed. The foundation of the programming system is a implementation of the Model-View-Controller (MVC) design pattern as a reactive program using the elegant Functional Reactive Programming (FRP) framework. Human-Computer Interaction (HCI) principles and methods are considered in all design decisions. A usabilty study was made to �find out the effectiveness of the new system.

Dans cette thèse, notre défi sera de trouver la réponse à la question : comment répondre à des requêtes XPath sur des flux XML avec une faible latence, une couverture complète, une grande efficacité temporelle et un faible coût mémoire? Dans cette thèse, nous proposons dans un premier temps une approximation de l’algorithme de réponse au plus-tôt pour les requêtes XPath par une compilation en un automate de mots imbriqués. Nous rapproche ainsi de la latence et d’une empreinte mémoire optimales. Dans un deuxième temps, nous proposons une définition formelle de XPath 3.0. Celle-ci est obtenue en faisant correspondre XPath au nouveau langage λXP que nous introduirons. Nous montrons par la suite comment compiler des requêtes λXP en des réseaux d’automates de mots imbriqués, et développons des algorithmes de streaming pour ces derniers. Dans un troisième temps, nous allons développer un algorithme pour la projection de flux XML en fonction de la requête définie par un automate de mots imbriqués. Ainsi serons- nous en mesure de faire en sorte que notre algorithme soit temporellement très efficace. Nous avons implémenté tous nos algorithmes avec l’objectif visé d’obtenir un outil de streaming applicable dans l’industrie, et les avons testés sur les benchmarks habituels. Notre algorithme surpasse toutes les approches précédemment établies en termes d’efficacité temporelle, de couverture et de latence. / The challenge that we tackle in this thesis is the problem of how to answer XPath queries on XML streams with low latency, full coverage, high time efficiency, and low memory costs. We first propose to approximate earliest query answering for navigational XPath queries by compilation to early nested word automata. It turns out that this leads to almost optimal latency and memory consumption. Second, we contribute a formal semantics of XPath 3.0. It is obtained by mapping XPath to the new query language λXP that we introduce. We then show how to compile λXP queries to networks of early nested word automata, and develop streaming algorithms for the latter. Thereby we obtain a streaming algorithm that indeed covers all of XPath 3.0. Third, we develop an algorithm for projecting XML streams with respect to the query defined by an early nested word automaton. Thereby we are able to make our streaming algorithms highly time efficient. We have implemented all our algorithms with the objective to obtain an industrially applicable streaming tool. It turns out that our algorithms outperform all previous approaches in time efficiency, coverage, and latency.

Aujourd'hui, les smartphones intègrent une grande variété de capteurs tel que l’accéléromètre, le capteur de lumière, le capteur d'orientation, etc. Créé pour détecter les informations du contexte, ces capteurs ont permis également l’apparition des nouvelles modalités d'interaction comme par exemple le secouage du téléphone ou la modification de son orientation. L’utilisation de ces modalités réduit les restrictions d’interaction avec les smartphones et ouvrent la voie à une grande expansion des interactions multimodales sous mobiles. Malheureusement, le contexte actuel de développement des logiciels mobiles rend difficile le développement d'applications multimodales. Dans cette thèse, notre challenge consiste à aider les développeurs pour faire face à cette difficulté. Nous proposons une solution à base des modèles qui vise à faciliter le développement d'interfaces mobiles multimodales. Nous adoptons les principes de l’Ingénierie Dirigée par les Modèles (IDM), qui convient parfaitement avec un tel contexte. Notre proposition consiste en un langage de modélisation nommé M4L (mobile multimodalité Modeling Language), ainsi qu’un framework nommé MIMIC (mobiles multimodalité Créateur) qui se base sur M4L pour permettre la modélisation graphique et la génération automatique des interfaces mobiles multimodales (en entrée et en sortie). Notre approche respecte les principaux critères de l’IDM afin d‘être efficace. Les résultats de nos évaluations suggèrent que l'utilisation de MIMIC (basé sur le langage M4L) facilite le développement des interfaces mobiles multimodales. / Today, smartphones present a great variety of features and embed an important number of sensors (accelerometer, touchscreen, light sensor, orientation sensor…). Created for giving context-aware abilities, these sensors also allow new types of interaction like shaking the phone or changing its orientation. Such type of interaction reduces limitation of mobile phones and paves the way to a great expansion of multimodal mobile interactions. Unfortunately, the current context of mobile software development makes difficult the development of multimodal applications. In this thesis, we intend to help developers to deal with this difficulty by providing a mode-lbased solution that aims to facilitate the development of multimodal mobile interfaces. We adopt the principles of the Model Driven Engineering (MDE), which is particularly fitted for such context. Our proposition includes M4L (Mobile MultiModality Modeling Language) modeling language to model the (input/output) multimodal interactions and the MIMIC (MobIle MultImodality Creator) framework that allows the graphical modeling and automatic generation of multimodal mobile interfaces. Our approach respects the main criteria of the MDE in order to define an efficient model-based approach. The results of our evaluations suggest that using our approach facilitates the development of sensor-based multimodal mobile interfaces. With our contributions, we aim to facilitate the penetration of multimodal applications and benefit from their advantages.

Equation-based modelling languages have become a vital tool in many areas of science and engineering. Functional Hybrid Modelling (FHM) is an approach to equation-based modelling that allows the behaviour of a physical system to be expressed as a modular hierarchy of undirected equations. FHM supports a variety of advanced language features — such as higher-order models and variable system structure — that sets it apart from the majority of other modelling languages. However, the inception of these new features has not been accompanied by the semantic tools required to effectively use and understand them. Specifically, there is a lack of static safety assurances for dynamic models and the semantics of the aforementioned language features are poorly understood. Static safety guarantees are highly desirable as they allow problems that may cause an equation system to become unsolvable to be detected early, during compilation. As a result, the use of static analysis techniques to enforce structural invariants (e.g. that there are the same number of equations as unknowns) is now in use in main-stream equation-based languages like Modelica. Unfortunately, the techniques employed by these languages are somewhat limited, both in their capacity to deal with advanced language features and also by the spectrum of invariants they are able to enforce. Formalising the semantics of equation-based languages is also important. Semantics allow us to better understand what a program is doing during execution, and to prove that this behaviour meets with our expectation. They also allow different implementations of a language to agree with one another, and can be used to demonstrate the correctness of a compiler or interpreter. However, current attempts to formalise such semantics typically fall short of describing advanced features, are not compositional, and/or fail to show correctness. This thesis provides two major contributions to equation-based languages. Firstly, we develop a refined type system for FHM capable of capturing a larger number of structural anomalies than is currently possible with existing methods. Secondly, we construct a compositional semantics for the discrete aspects of FHM, and prove a number of key correctness properties.

This dissertation is about effects and type theory. Functional programming languages such as Haskell illustrate how to encapsulate side effects using monads. Haskell compilers provide a handful of primitive effectful functions. Programmers can construct larger computations using the monadic return and bind operations. These primitive effectful functions, however, have no associated definition. At best, their semantics are specified separately on paper. This can make it difficult to test, debug, verify, or even predict the behaviour of effectful computations. This dissertation provides pure, functional specifications in Haskell of several different effects. Using these specifications, programmers can test and debug effectful programs. This is particularly useful in tandem with automatic testing tools such as QuickCheck. The specifications in Haskell are not total. This makes them unsuitable for the formal verification of effectful functions. This dissertation overcomes this limitation, by presenting total functional specifications in Agda, a programming language with dependent types. There have been alternative approaches to incorporating effects in a dependently typed programming language. Most notably, recent work on Hoare Type Theory proposes to extend type theory with axioms that postulate the existence of primitive effectful functions. This dissertation shows how the functional specifications implement these axioms, unifying the two approaches. The results presented in this dissertation may be used to write and verify effectful programs in the framework of type theory.

This thesis is about Martin-Löf's intuitionistic theory of types (type theory). Type theory is at the same time a formal system for mathematical proof and a dependently typed programming language. Dependent types are types which depend on data and therefore to type check dependently typed programming we need to perform computation(normalisation) in types. Implementations of type theory (usually some kind of automatic theorem prover or interpreter) have at their heart a type checker. Implementations of type checkers for type theory have at their heart a normaliser. In this thesis I consider type checking as it might form the basis of an implementation of type theory in the functional language Haskell and then normalisation in the more rigorous setting of the dependently typed languages Epigram and Agda. I investigate a method of proving normalisation called Big-Step Normalisation (BSN). I apply BSN to a number of calculi of increasing sophistication and provide machine checked proofs of meta theoretic properties.

A key advantage of BDI-based agent programming is that agents can deliberate about which course of action to adopt to achieve a goal or respond to an event. However while state-of-the-art BDI-based agent programming languages provide flexible support for expressing plans, they are typically limited to a single, hard-coded, deliberation strategy(perhaps with some parameterisation) for all task environments. In this thesis, we describe a novel agent programming language, meta-APL, that allows both agent programs and the agent’s deliberation strategy to be encoded in the same programming language. Key steps in the execution cycle of meta-APL are reflected in the state of the agent and can be queried and updated by meta-APL rules, allowing a wide range of BDI deliberation strategies to be programmed. We give the syntax and the operational semantics of meta-APL, focussing on the connections between the agent’s state and its implementation. Finally, to illustrate the flexibility of meta-APL, we show how Jason and 3APL programs and deliberation strategy can be translated into meta-APL to give equivalent behaviour under weak bisimulation equivalence.

The most widely available high performance platforms today are hierarchical, with shared memory leaves, e.g. clusters of multi-cores, or NUMA with multiple regions. The Glasgow Haskell Compiler (GHC) provides a number of parallel Haskell implementations targeting different parallel architectures. In particular, GHC-SMP supports shared memory architectures, and GHC-GUM supports distributed memory machines. Both implementations use different, but related, runtime system (RTS) mechanisms and achieve good performance. A specialised RTS for the ubiquitous hierarchical architectures is lacking. This thesis presents the design, implementation, and evaluation of a new parallel Haskell RTS, GUMSMP, that combines shared and distributed memory mechanisms to exploit hierarchical architectures more effectively. The design evaluates a variety of design choices and aims to efficiently combine scalable distributed memory parallelism, using a virtual shared heap over a hierarchical architecture, with low-overhead shared memory parallelism on shared memory nodes. Key design objectives in realising this system are to prefer local work, and to exploit mostly passive load distribution with pre-fetching. Systematic performance evaluation shows that the automatic hierarchical load distribution policies must be carefully tuned to obtain good performance. We investigate the impact of several policies including work pre-fetching, favouring inter-node work distribution, and spark segregation with different export and select policies. We present the performance results for GUMSMP, demonstrating good scalability for a set of benchmarks on up to 300 cores. Moreover, our policies provide performance improvements of up to a factor of 1.5 compared to GHC- GUM. The thesis provides a performance evaluation of distributed and shared heap implementations of parallel Haskell on a state-of-the-art physical shared memory NUMA machine. The evaluation exposes bottlenecks in memory management, which limit scalability beyond 25 cores. We demonstrate that GUMSMP, that combines both distributed and shared heap abstractions, consistently outper- forms the shared memory GHC-SMP on seven benchmarks by a factor of 3.3 on average. Specifically, we show that the best results are obtained when shar- ing memory only within a single NUMA region, and using distributed memory system abstractions across the regions.

Martin-Lof's intuitionistic type theory (Type Theory) is a formal system that serves not only as a foundation of constructive mathematics but also as a dependently typed programming language. Dependent types are types that depend on values of other types. Type Theory is based on the Curry-Howard isomorphism which relates computer programs with mathematical proofs so that we can do computer-aided formal reasoning and write certified programs in programming languages like Agda, Epigram etc. Martin Lof proposed two variants of Type Theory which are differentiated by the treatment of equality. In Intensional Type Theory, propositional equality defined by identity types does not imply definitional equality, and type checking is decidable. In Extensional Type Theory, propositional equality is identified with definitional equality which makes type checking undecidable. Because of the good computational properties, Intensional Type Theory is more popular, however it lacks some important extensional concepts such as functional extensionality and quotient types. This thesis is about quotient types. A quotient type is a new type whose equality is redefined by a given equivalence relation. However, in the usual formulation of Intensional Type Theory, there is no type former to create a quotient. We also lose canonicity if we add quotient types into Intensional Type Theory as axioms. In this thesis, we first investigate the expected syntax of quotient types and explain it with categorical notions. For quotients which can be represented as a setoid as well as defined as a set without a quotient type former, we propose to define an algebraic structure of quotients called definable quotients. It relates the setoid interpretation and the set definition via a normalisation function which returns a normal form (canonical choice) for each equivalence class. It can be seen as a simulation of quotient types and it helps theorem proving because we can benefit from both representations. However this approach cannot be used for all quotients. It seems that we cannot define a normalisation function for some quotients in Type Theory, e.g. Cauchy reals and finite multisets. Quotient types are indeed essential for formalisation of mathematics and reasoning of programs. Then we consider some models of Type Theory where types are interpreted as structured objects such as setoids, groupoids or weak omega-groupoids. In these models equalities are internalised into types which means that it is possible to redefine equalities. We present an implementation of Altenkirch's setoid model and show that quotient types can be defined within this model. We also describe a new extension of Martin-Lof type theory called Homotopy Type Theory where types are interpreted as weak omega-groupoids. It can be seen as a generalisation of the groupoid model which makes extensional concepts including quotient types available. We also introduce a syntactic encoding of weak omega-groupoids which can be seen as a first step towards building a weak omega-groupoids model in Intensional Type Theory. All of these implementations were performed in the dependently typed programming language Agda which is based on intensional Martin-Lof type theory.