Search

The analysis of information flow is a popular technique for ensuring the confidentiality of data. It is in this context that confidentiality policies arise for giving guarantees that private data cannot be inferred by the inspection of public data. One of those policies is non-interference, a semantic condition that ensures the absence of illicit information flow during program execution by not allowing to distinguish the results of two computations when they only vary in their confidential inputs. A remarkable feature of non-interference is that it can be enforced statically by the definition of information flow type systems. In those type systems, if a program type-checks, then it means that it meets the security policy. In this paper we focus on the preservation of non-interference through program translation. Concretely, we formalize the proof of security preservation of Hunt and Sands' translation that transforms high-level While programs typable in a flow-sensitive type system into equivalent high-level programs typable in a flow-insensitive type system. Our formalization is performed in the dependently-typed language Agda. We use the expressive power of Agda's type system to encode the security type systems at the type level. A particular aspect of our formalization is that it follows a fully internalist approach where we decorate the type of the abstract syntax with security type information in order to obtain the representation of well-typed (i.e secure) programs. A benefit of this approach is that it allows us to directly express the property of security preservation in the type of the translation relation. In this manner, apart from inherently expressing the transformation of programs, the translation relation also stands for an inductive proof of security preservation.

Elixir is a functional programming language with dynamic typing. We propose a gradual type system that makes it possible to perform type-checking on a significant fragment of the language. An important feature of the type system is that it does not require any syntactic change to Elixir. Type information is provided by means of function signatures which are declared in terms of Elixir typespec directives. The proposed type system is based on subtyping and is backward compatible, as it allows the presence of untyped code fragments. We have a prototype implementation of the type-checker in Elixir itself and a formalization in Idris of the fragment considered.

AspectAG is a domain specific language embedded in Haskell to represent modular attribute grammars. In AspectAG attribute grammar fragments can be defined independently (even in separate modules) and then combined in a safe way. This flexibility is achieved through the use of extensible records, which are implemented using type-level programming techniques. Type-level programming support has remarkably evolved in Haskell since the first version of AspectAG was designed; having incorporated new features like data promotion and kind polymorphism, among others, which allows to program in a "strongly typed" way at the level of types in a similar way as when programming at the level of values. In this paper we redefine AspectAG applying the new type-level programming techniques. As a consequence, we obtain a more robust system with better error messages.

This paper presents TensorSafe, a dependently typed Haskell library which makes possible the definition and structural validation of deep neural networks architectures. Nowadays, the development process of deep learning models has been notably simplified due to the availability of sophisticated tools in the industry. However, most of these tools do not provide any security controls at compilation time, making the developers deal with unexpected run-time errors and uncertainties. In particular, validating the structure of deep neural networks at compilation time is a complex subject which involves the mathematical validation of all operations that a deep learning model will perform. Moreover, this structural checking requires an advanced usage of types systems theories to manipulate abstract type definitions capable of modeling neural networks constructions. Many different programming techniques were involved in the specification of TensorSafe. Primarily, the application of the functional programming paradigm and the use of dependent types were of great importance for the development process and to probe the correctness of the neural network models. The experimental evaluation showed that by using TensorSafe it is possible to correctly create well known deep neural network architectures, such like MNIST or ResNet50.

In this paper, we show how stream fusion, a program transformation technique used in functional programming, can be adapted for an Object-Oriented setting. This makes it possible to have more Stream operators than the ones currently provided by the Java Stream API. The addition of more operators allows for a greater deal of expressiveness. To this extent, we show how these operators are incorporated in the stream setting. Furthermore, we also demonstrate how a specific set of optimizations eliminates overheads and produces equivalent code in the form of for loops. In this way, programmers are relieved from the burden of writing code in such a cumbersome style, thus allowing for a more declarative and intuitive programming approach., This work is financed by the ERDF European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 Programme and by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia within project POCI-01-0145-FEDER016718.

Attribute grammars are a powerfull, well-known formalism to implement and reason about programs which, by design, are conveniently modular. In this work we focus on a state of the art zipper-based embedding of classic attribute grammars and higher-order attribute grammars. We improve their execution performance through controlling attribute (re)evaluation by means of memoization techniques. We present the results of our optimizations by comparing their impact in various implementations of different, well-studied, attribute grammars and their Higher-Order extensions. (C) 2018 Elsevier B.V. All rights reserved., (undefined)

Functional programmers are strong enthusiasts of modular solutions to programming problems. Since software characteristics such as readability or maintainability are often directly proportional to modularity, this programming style naturally contributes to the beauty of functional programs. Unfortunately, in return of this beauty we often sacrifice efficiency: modular programs rely, at runtime, on the creation, use and elimination of intermediate data structures to connect its components. In this tutorial paper, we study an advanced technique that attempts to retain the best of this two worlds: (i) it allows programmers to implement beautiful, modular programs (ii) it shows how to transform such programs, in a way that can be incorporated in a compiler, into programs that do not construct any intermediate structure., (undefined)

In this paper, we present an embedding of attribute grammars in Haskell, that is both modular and type-safe, while providing the user with domain specific error messages.Our approach involves to delay part of the safety checks to runtime. When a grammar is correct, we are able to extract a function that can be run without expecting any runtime error related to the EDSL.

In this paper we present a methodology to organize the construction of a correct compiler, taking advantage of the power of full dependently type systems. The basic idea consists in decorating the abstract syntax of languages with their semantics, allowing to express the correctness of the compiler at type level. We show our methodology in a first small example and then explore how it can be promoted to more realistic languages, realizing that our internalistic approach is feasible for defining a correct-by-construction compiler from an imperative language with conditional iteration to a stack based intermediate language. We also show how this methodology can be combined with the externalist approach, compiling from the intermediate language to an assembly-like low level code and separately proving its correctness.

Extensible records are records structures that can be dynamically extended with new fields. In some languages, extensible records are supported as a primitive, in others they are implemented as a user library, each alternative with its benefits and drawbacks. This paper presents a library to strongly-typed extensible records in Idris, a functional programming language with dependent types. Like HList, a Haskell library for extensible records, we use heterogeneous lists to represent our records, but now exploiting the power of dependent types. We show the benefits of our solution by means of examples.

International audience; The methodology for producing Systematic Mapping Studies (SMS) defines the following workflow: (i) defining research questions; (ii) querying bibliography data sources using a key-word complex query; (iii) selecting relevant documents from data sources; (iv) key-wording of documents and defining a classification scheme; (v) classifying the documents and (vi) producing the mapping and answers to the research questions. Frequently these steps are performed manually and some how empirically. This paper introduces an approach for semi-automating some of the steps of SMS and enhancing them with quality criteria.

Attribute Grammars are a powerfull, well-known formalism to implement and reason about programs which, by design, are conveniently modular.In this work we focus on a state of the art Zipper-based embedding of Attribute Grammars and further improve its performance through controlling attribute (re)evaluation by using memoization techniques. We present the results of our optimization by comparing their impact in various implementations of different, well-studied Attribute Grammars., (undefined)

The adoption of Cloud Computing technologies by the organizations has profound consequences on the way software applications are developed and used. The migration to the Cloud may be accompanied by the revision of the business process, to integrate tasks over big data. In this way, existing workflow implementations may be extended with calls to operations in Hadoop or other tools. In this work, we define a framework to implement business process over heterogeneous technologies. Our framework is based on a novel workflow engine, called μBP-AM. Workflow execution in μBP-AM is performed by successively transforming the graph obtained from a workflow definition. μBP-AM has a formal semantics, which gives a precise definition of how the workflow is implemented. μBP-AM is at the core of an extensible framework capable of supporting not only Web service operations but also Hadoop operation calls (among others). The tool described here was conceived to increase reliability and to promote interoperability. We describe a prototype implementation of our framework, as well as some experimental results. Experiments using this prototype show that compositions run in μBP-AM using about the same resources as those run by using other tools.

We use a functional framework designed for parallel programming with linear algebra applications to leverage the computing power of heterogeneous hardware. Our work is performed in the context of the pure functional programming language Haskell. The framework allows the manipulation of arbitrary representations for matrices and the definition of multiple implementations of BLAS operations based on different algorithms and parallelism strategies. We perform some benchmarks for representative BLAS operations on three different platforms (multi-core CPU, ARM and GPU), where we apply different parallelism strategies and employ several representations.

The analysis of information flow has become a popular technique for ensuring the confidentiality of data. An end-to-end confidentiality policy guarantees that private data cannot be inferred by the inspection of public data. A security property that ensures a kind of confidentiality is the noninterference property, which can be enforced by the use of security type systems where types correspond to security levels. In this paper we show the development of a compiler (written in Haskell) between a simple imperative language and semi-structured machine code, which preserves the property of noninterference. The compiler is based on the use of typed abstract syntax (implemented in terms of Haskell GADTs and type-level functions) to encode the security type system of both the source and target language. This makes it possible to use Haskell’s type checker to verify two things: that programs in both languages satisfy the security property, and that the compiler is correct by construction (in the sense that it preserves noninterference).

We investigate the use of functional programming to develop a numerical linear algebra run-time; i.e. a framework where the solvers can be adapted easily to different contexts and task parallelism can be attained (semi-) automatically. We follow a bottom up strategy, where the first step is the design and implementation of a framework layer, composed by a functional version of BLAS (Basic Linear Algebra Subprograms) routines. The framework allows the manipulation of arbitrary representations for matrices and vectors and it is also possible to write and combine multiple implementations of BLAS operations based on different algorithms and parallelism strategies. Using this framework, we implement a functional version of Cholesky factorization, which serves as a proof of concept to evaluate the flexibility and performance of our approach.

Web Services have become the standard for exposing services on the Internet. Since many operations require the collaboration between two or more services, the need to have languages to express Web Services compositions has emerged. In this paper, we focus on PEWS, a Web Service composition language. We present an operational semantics of PEWS and propose some minor extensions to it in order to support most common workflow patterns. The extended version of PEWS is able to fully support 36 out of the 43 control-flow patterns as defined in the literature, compared to 17 fully supported by the industry standard BPEL.

The library for strongly typed heterogeneous collections HList provides an implementation of extensible records in Haskell that needs only a few common extensions of the language. In HList, records are represented as linked lists of label-value pairs with a lookup operation that is linear-time in the number of fields. In this paper, we use type-level programming techniques to develop a more efficient representation of extensible records for HList. We propose two internal encodings for extensible records that improve lookup at runtime without needing a total order on the labels. One of the encodings performs lookup in constant time but at a cost of linear time insertion. The other one performs lookup in logarithmic time while preserving the fast insertion of simple linked lists. Through staged compilation, the required slow search for a field is moved to compile time in both cases.

Functional programs often combine separate parts using intermediate data structures for communicating results. Programs so defined are modular, easier to understand and maintain, but suffer from inefficiencies due to the generation of those gluing data structures. To eliminate such redundant data structures, some program transformation techniques have been proposed. One such technique is shortcut fusion, and has been studied in the context of both pure and monadic functional programs. In this paper, we study several shortcut fusion extensions, so that, alternatively, circular or higher-order programs are derived. These extensions are also provided for effect-free programs and monadic ones. Our work results in a set of generic calculation rules, that are widely applicable, and whose correctness is formally established., Fundação para a Ciência e a Tecnologia

Functional programs often combine separate parts using intermediate data structures for communicating results. Programs so defined are modular, easier to understand and maintain, but suffer from inefficiencies due to the generation of those gluing data structures. To eliminate such redundant data structures, some program transformation techniques have been proposed. One such technique is shortcut fusion, and has been studied in the context of both pure and monadic functional programs. In this paper, we study several shortcut fusion extensions, so that, alternatively, circular or higher-order programs are derived. These extensions are also provided for effect-free programs and monadic ones. Our work results in a set of generic calculation rules, that are widely applicable, and whose correctness is formally established., (undefined)

This paper presents the definition of a language with reflection primitives. The language is a homogeneous multi-stage language that provides the capacity of code analysis by the inclusion of a pattern matching mechanism that permits inspection of the structure of quoted expressions and their destruction into component subparts. Quoted expressions include an explicit annotation of their context which is used for dynamic inference of type, where a dynamic typing discipline based on Hinze and Cheney's approach is used for typing quoted expressions.This paper follows the approach of Sheard and Pasalic about the use of the meta-language Ωmega as a tool for language design. In this sense, it is shown how to represent the syntax, the static as well as the dynamic semantics of the proposed language in terms of Ωmega constructs.