o objetivo deste trabalho é apresentar a implementação em Java de uma máquina abstrata para execução distribuída de programas funcionais. Mostra-se como as facilidades da linguagem Java foram utilizadas para a implementação de uma linguagem funcional paralela que roda os programas funcionais de forma distribuída em uma rede de computadores. Linguagens Funcionais geralmente são implementadas usando uma máquina abstrata para a execução dos programas. Essas máquinas são usualmente máquinas de redução de grafos. Para se rodar os programas funcionais na máquina virtual Java implementou-se a máquina de redução de grafos G-Machine em Java. Nesta dissertação, apresenta-se inicialmente a implementação da G-Machine em Java, realizada como primeira etapa do trabalho e discute-se a abordagem utilizada para essa implementação. Mostra-se em seguida, como os programas funcionais podem ser compilados para rodar nessa G-Machine. Na segunda etapa do trabalho, modifica-se o sistema implementado para permitir a execução distribuída dos programas funcionais. Finalmente apresenta-se uma avaliação de desempenho e mostra-se possíveis trabalhos futuros. / The objective of this work is to present the implementation in the Java language of an abstract machine for distributed execution of functional programs. We show how the Java facilities were used to implement a parallel functional programming language with a distributed runtime system. Functional Languages are usually implemented using an abstract machine to execute programs. These abstract machines are usually graph reduction machines. To mn the functional programs on the Java Virtual Machine we have implemented the G-Machine graph reduction machine in Java. In this text, we first present the implementation of the G-Machine in J ava, and discuss its implementation. Then we show how this implementation was modified to allow distributed execution of functional programs. Finally some benchmarks, possible future works and conclusions are presented.

Approximation algorithms are widely used for problems related to computational geometry, complex optimization problems, discrete min-max problems and NP-hard and space hard problems. Due to the complex nature of such problems, imperative languages are perhaps not the best-suited solution when it comes to their actual implementation. Functional languages like Haskell could be a good candidate for the aforementioned mentioned issues. Haskell is used in industries as well as in commercial applications, e.g., concurrent applications, statistics, symbolic math and financial analysis. Several approximation algorithms have been proposed for different problems that naturally arise in the DNA clone classifications. In this thesis, we have performed an initial and explorative study on applying functional languages for approximation algorithms. Specifically, we have implemented a well known approximate clustering algorithm both in Haskell and in Java and we discuss the suitability of applying functional languages for the implementation of approximation algorithms, in particular for graph theoretical approximate clustering problems with applications in DNA clone classification. We also further explore the characteristics of Haskell that makes it suitable for solving certain classes of problems that are hard to implement using imperative languages. / Muhammad Imran Shafi: 29A Sodergatan 19547 Marsta, 0737171514, Muhammad Akram C/O Saad Bin Azhar Folkparksvagen 20/10 Ronneby, 0762899111

OCaml est un langage fonctionnel statiquement typé, qui génère après inférence de types un arbre de syntaxe abstraite dans lequel chacun des noeuds est annoté avec un ensemble d’informations issues de cette inférence. Ces informations, en particulier les types inférés, constituent une preuve de typage de l’expression annotée.Ce manuscrit de thèse s’intéresse à la vérification de ces arbres annotés en les considérant comme des preuves de typages du programme, et décrit un ensemble de règles permettant d’en vérifier la cohérence. La formalisation de ces règles de vérification de preuves de types peut être vue comme une représensation du système de types du langage étudié.Cette thèse présente plusieurs aspects de la vérification d’arbres de syntaxe annotés. Le premier cas étudié est la formalisation d’un dérivé de MiniML où toutes les expressions sont annotées de manière théoriquement parfaite, et montre qu’il est possible d’écrire des règles de vérification de manière algorithmique, rendant directe la preuve de correction vis-à-vis de la spécification. La seconde partie s’intéresse à la formalisation de règles de vérification pour un sous-ensemble du premier langage intermédiaire d’OCaml, le TypedTree, accompagné d’un vérificateur implémentant ces règles. Ces règles constituent alors une représentation du système de types d’OCaml, document jusqu’alors inexistant, au mieux disséminé dans diverses publications. / OCaml is a statically typed programming language that generates typed annotated abstract syntax trees after type inference. Each of their nodes contains information derived from the inference like the inferred type and the environment used to find this information. These annotated trees can then be seen as typing proofs of the program.In this thesis, we introduce a consistency checking of type-annotated trees, considering them as typing proof, and we describe a set of rules that defines the consistency property.Such consistency checking rules can then be seen as a formalized representation of the type system, since consistency ensures the typing invariants of the language.This thesis introduces multiple aspects of checking type-annotated trees. First of all, it considers a simplified and ideal version of MiniML and formalizes a set of rules to check consistency. In this formalism, we consider ideally type-annotated trees, which might not be the case for OCaml typed trees. Such type checking rules are presented in an algorithmic form, reducing as much as possible the gap from formalism to implementation. As such, they ease the correction proof between the implementation of the type checker and the specification of the type system. The second part of this thesis is dedicated to the formalization of a set of rules for a subset of the OCaml annotated trees: the TypedTree. The formalism described in these chapters is implemented as a type checker working on large subset of the language, leaving the formalization of some aspects for a further work. These rules constitute a formalized representation of the OCaml type system in a single document.

System-on-Chip (SoC) and other complex distributed hardware/software systems contain heterogeneous components whose behavior are best captured by different models of computations (MoCs). As a result, any system design framework for such systems requires the capability to express heterogeneous MoCs. Although a number of system level design languages (SLDL)s and frameworks have proliferated over the last few years, most of them are lacking in multiple ways. Some of the SLDLs and system design frameworks we have worked with are SpecC, Ptolemy II, SystemC-H, etc. From our analysis of these, we identify their following shortcomings: First, their dependence on specific programming language artifacts (Java or C/C++) make them less amenable to formal analysis. Second, the refinement strategies proposed in the design flows based on these languages lack formal semantics underpinnings making it difficult to prove that refinements preserve correctness, and third, none of the available SLDLs are easily customizable by users. In our work, we address these problems as follows: To alleviate the first problem, we follow Axel Jantsch's paradigm of function-based semantic definitions of MoCs and formulate a functional programming framework called SML-Sys. We illustrate through a number of examples how to model heterogenous computing systems using SML-Sys. Our framework provides for formal reasoning due to its formal semantic underpinning inherited from SML's precise denotational semantics. To handle the second problem and apply refinement strategies at a higher-level, we propose a refinement methodology and provide a semantics preserving transformation library within our framework. To address the third shortcoming, we have developed EWD, which allows users to customize MoC-specific visual modeling syntax defined as a metamodel. EWD is developed using a metamodeling framework GME (Generic Modeling Environment). It allows for automatic design-time syntactic and semantic checks on the models for conformance to their metamodel. Modeling in EWD facilitates saving the model in an XML-based interoperability language (IML) we defined for this purpose. The IML format is in turn automatically translated into Standard ML, or Haskell models. These may then be executed and analyzed either by our existing model analysis tools SMLSys, or the ForSyDe environment. We also generate SMV-based template from the XML representation to obtain verification models. / Master of Science

Racket is a modern, general-purpose programming language with a language-oriented focus. To date, Racket has found notable uses in research and education, among other applications. To expand the reach of the language, there has been a desire to develop an efficient platform for running Racket in a web-based environment. WebAssembly (Wasm) is a binary executable format for a stack-based virtual machine designed to provide a fast, efficient, and secure execution environment for code on the web. Wasm is primarily intended to be a compiler target for higher-level languages. Providing Wasm support for the Racket project may be a promising way to bring Racket to the browser. To this end, we present an incremental approach to the development of a Racket- to-Wasm compiler. We make use of an existing backend for Racket that targets a portable bytecode known as PB, along with the associated PB interpreter. We per- form an ahead-of-time static translation of sections of PB into native Wasm, linking the chunks back to the interpreter before execution. By replacing portions of PB with native Wasm, we can eliminate some portion of interpretation overhead and move closer to native Wasm support for Chez Scheme (Racket’s Backend). Due to the use of an existing backend and interpreter, our approach already supports nearly all features of the Racket language – including delimited continuations, tail-calling behavior, and garbage collection – and excluding threading and FFI support for the time being. We perform benchmarks against a baseline to validate our approach, to promising results.

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. / Our main thesis is that functions should be transparent during the metaprogramming stage. Metaprogramming is intended as a possibility for the programmer to extend the compiler. But in a functional programming style, the program logic is found in the definition of its functions. Since functions are generally opaque, it is impossible for the programmer to access this information and this limits the metaprogramming possibilities. We will illustrate the benefits of transparent functions for metaprogramming. We will give the example of symbolic computation and also show new forms of optimizations now available at the metaprogramming stage. We will also illustrate that transparency allows us to bridge the gap between the datatypes of a program and its functions. We will also examine how transparent functions affects other aspects of the language. We will focus on how to implement them, their performance impact and their ease of use. We illustrate our thesis with Abitbol, a language designed for metaprogramming.

We discuss the development of a number of algorithms and techniques to allow object oriented virtual machines to support many of the features needed by functional and other higher level languages. These features include non-strict evaluation, partial function application, higher ranked and higher kinded types. To test the mechanisms that we have developed we have also produced a compiler to allow the functional language Haskell to be compiled to a native executable for the Common Language Runtime. This has allowed us to demonstrate that the techniques we have developed are practically viable.

Les logiciels critiques nécessitent l’obtention d’une évaluation de conformité aux normesen vigueur avant leur mise en service. Cette évaluation est obtenue après un long travaild’analyse effectué par les évaluateurs de logiciels critiques. Ces derniers peuvent être aidéspar des outils utilisés de manière interactive pour construire des modèles, en faisant appel àdes analyses de flots d’information. Des outils comme SPARK-Ada existent pour des sous-ensembles du langage Ada utilisés pour le développement de logiciels critiques. Cependant,des langages émergents comme ceux de la famille ML ne disposent pas de tels outils adaptés.La construction d’outils similaires pour les langages ML demande une attention particulièresur certaines spécificités comme les fonctions d’ordre supérieur ou le filtrage par motifs. Cetravail présente une analyse de flot d’information pour de tels langages, spécialement conçuepour répondre aux besoins des évaluateurs. Cette analyse statique prend la forme d’uneinterprétation abstraite de la sémantique opérationnelle préalablement enrichie par desinformations de dépendances. Elle est prouvée correcte vis-à-vis d’une définition formellede la notion de dépendance, à l’aide de l’assistant à la preuve Coq. Ce travail constitue unebase théorique solide utilisable pour construire un outil efficace pour l’analyse de toléranceaux pannes. / Critical software needs to obtain an assessment before commissioning in order to ensure compliance tostandards. This assessment is given after a long task of software analysis performed by assessors. Theymay be helped by tools, used interactively, to build models using information-flow analysis. Tools likeSPARK-Ada exist for Ada subsets used for critical software. But some emergent languages such as thoseof the ML family lack such adapted tools. Providing similar tools for ML languages requires specialattention on specific features such as higher-order functions and pattern-matching. This work presentsan information-flow analysis for such a language specifically designed according to the needs of assessors.This analysis is built as an abstract interpretation of the operational semantics enriched with dependencyinformation. It is proved correct according to a formal definition of the notion of dependency using theCoq proof assistant. This work gives a strong theoretical basis for building an efficient tool for faulttolerance analysis.

<p dir="ltr">Protecting personal information is growing increasingly important to the general public, to the point that major tech companies now advertise the privacy features of their products. Despite this, it remains challenging to implement applications that do not leak private information either directly or indirectly, through timing behavior, memory access patterns, or control flow side channels. Existing security and cryptographic techniques such as secure multiparty computation (MPC) provide solutions to privacy-preserving computation, but they can be difficult to use for non-experts and even experts.</p><p dir="ltr">This dissertation develops the design, theory and implementation of various language-based techniques that help programmers write privacy-critical applications under a strong threat model. The proposed languages support private structured data, such as trees, that may hide their structural information and complex policies that go beyond whether a particular field of a record is private. More crucially, the approaches described in this dissertation decouple privacy and programmatic concerns, allowing programmers to implement privacy-preserving applications modularly, i.e., to independently develop application logic and independently update and audit privacy policies. Secure-by-construction applications are derived automatically by combining a standard program with a separately specified security policy.</p><p><br></p>

The aim of this thesis is to research how the functional paradigm can be used for hardware acceleration with an emphasis on data-parallel tasks. The level of abstraction of the traditional hardware description languages, such as VHDL or Verilog, is becoming to low. High-level languages from the domains of software development and modeling, such as C/C++, SystemC or MATLAB, are experiencing a boom for hardware description on the algorithmic or behavioral level. Functional Languages are not so commonly used, but they outperform imperative languages in verification, the ability to capture inherent paralellism and the compactness of code. Data-parallel task are often accelerated on FPGAs, GPUs and multicore processors. In this thesis, we use a library for general-purpose GPU programs called Accelerate and extend it to produce VHDL. Accelerate is a domain-specific language embedded into Haskell with a backend for the NVIDIA CUDA platform. We use the language and its frontend, and create a new backend for high-level synthesis of circuits in VHDL.