Posts by Collection

projects

Vergrep - Verified Regular Expression String Search Utility

The main objective of the Vergrep project is to develop a provably correct and efficient regular expression string search tool using type theory-based proof assistants.

VerMedia - A formally verified theory for temporal media

Temporal media is information that is directly consumed by a user, and that varies with time. Examples of temporal media include music, video clips and computer animations. The main objective of this project is to develop a formally certified library of polymorphic functions to handle temporal media data.

publications

Iteradores, Templates e Consultas na Análise e Manipulação de Programas.

Published in II Workshop de Manutenção Moderna de Software, 2005

A engenharia reversa e a reestruturação de programas são uteís em tarefas de manutenção e evolução de software. As ferramentas e meta-ferramentas para análise e manipulação de código-fonte têm um papel importante nestas atividades, contudo seu desenvolvimento é difícil dada à complexidade intrínsica desta classe de ferramentas. A existência de meta-ferramentas melhores poderia facilitar a construção das ferramentas para análise e manipulação de código. Apesar de diversas meta-ferramentas já terem sido propostas, ainda não existe uma solução definitiva. Este trabalho propõe o uso integrado de iteradores, templates, e consultas relacionais para facilitar a construção de módulos para análise e manipulação de programas. Estes mecanismos são baseados nas noções de referências tipadas para código-fonte e de casamento de padrões em árvores sintáticas. Para demonstrar a efetividade desta abordagem, apresenta-se um construtor de grafos de semântica estática baseada em declarações, escopo e uso de símbolos. Para avaliar a performance das abordagens iterativas e declarativas, foram implementadas e analisadas duas refatorações. As meta-ferramentas apresentadas neste artigo apresentaram vantagens sobre outras meta-ferramentas, portanto podendo ser consideradas viáveis de serem introduzidas em processos de manutenção de software.

Download here

Compreensão de programas apoiada por uma linguagem de consulta em código fonte

Published in IV Workshop de Manutenção Moderna de Software, 2008

Software maintenance is an stage of software development process that consumes great developers effort, raising total cost of the project. Du- ring this process, a comprehension task of the system implementation is requi- red. Therefore, tools supporting this proccess may facilitate the developer work. This paper shows a query language for source code based on relational concepts which works on a syntactic representation augmented with static semantics of the program (scopes, declarations and symbols use). It is presented, as vali- dation, how this source code query language may be applied in the program comprehension activity.

Download here

A Solution to Haskell’s Multi-Parameter Type Class Dilemma

Published in XIII Simpósio Brasileiro de Linguagens de Programação, 2009

The introduction of multi-parameter type classes in Haskell has been hindered because of problems associated to ambiguity, which occur due to the lack of type specialization during type inference. This paper proposes a minimalist, simple solution to this problem, which requires only a small change to the type inference algorithm and to what has been considered ambiguity in Haskell. It does not depend on the use of programmer specified functional dependencies between type class parameters nor any other extra mechanism, such as associated types. A type system and a type inference algorithm, sound and complete with respect to the type system, are presented.

Download here

Uma Abordagem Híbrida de SAT e Busca Tabu para o Problema da Programação de Horários Escolares

Published in XLIII Simpósio Brasileiro de Pesquisa Operacional, 2011

O Problema da Programação de Horários Escolares (PPHE) é classificado como NP-Difícil e heurísticas para sua solução são alvo de diversas pesquisas na área de computação, matemática e pesquisa operacional. Normalmente, o problema é resolvido através de abordagens metaheurísticas como Algoritmos Genéticos, Simulated Annealing e GRASP. O presente trabalho propõe uma abordagem alternativa. Pretende-se reduzir do problema ao problema da Satisfazibilidade Proposicional (SAT) e resolvê-lo usando um resolvedor SAT para geração de uma solução inicial. Como não é viável tratar todos os requisitos PPHE através de satisfazibilidade, posteriormente, aplicar-se-á uma Busca Tabu para otimização da solução obtida. A eficiência da abordagem é avaliada comparando-a a abordagens conhecidas na literatura.

Download here

Programação de Horários Escolares Através de SAT e Metaheurísticas

Published in X Simpósio Brasileiro de Inteligência Computacional, 2011

O Problema da Programação de Horários Escolares (PPHE) é classificado como NP-Difícil e heurísticas para sua solução são alvo de diversas pesquisas na área de computação, matemática e pesquisa operacional. Normalmente, o problema é resolvido através de metaheurísticas como Algoritmos Genéticos, Simulated Annealing e GRASP. O presente trabalho propõe uma abordagem alternativa. Pretende-se reduzir do problema ao problema da Satisfazibilidade Proposicional (SAT) e resolvê- lo usando um resolvedor SAT para geração de uma solução inicial. Como não é viável tratar todos os requisitos PPHE através de satisfazibilidade, posteriormente, aplicar-se-á as metaheurísticas Busca Tabu e Simulated Annealing para otimização da solução obtida. Por fim serão apresentados os resultados de cada algoritmos e uma comparação com outro trabalho do gênero.

Download here

Resolvedores SAT para Verificação de Consistência em Modelos de Características

Published in Simpósio Mineiro de Computação, 2012

Linhas de produtos de software é uma nova abordagem de desenvolvimento de sistemas voltada ao reuso de software. As principais razões para se criar uma linha de produtos são a redução dos custos do processo, software mais confiável e de qualidade. Os modelos de características são uma forma diagramática de se modelar uma linha de produtos de software. Como os modelos estão crescendo em termos de suas características, um forte apoio ferramental se faz necessário para suportar o processo de modelagem,como por exemplo, a verificação de consistência dos mesmos. Assim, este trabalho tem como objetivo propor um algoritmo resolvedor SAT especializado para depurar modelos de características. O algoritmo proposto possui pontos de extensão para o desenvolvimento de novos algoritmos e para integração com ferramentas de modelagem de características. É esperado contribuir, desta forma, com a comunidade de SPL incluindo desenvolvedores de ferramentas de modelagem e usuários destas ferramentas.

Download here

Mechanized metatheory for a λ-calculus with trust types

Published in Journal of the Brazilian Computer Society, 2013

As computer programs become increasingly complex, techniques for ensuring trustworthiness of information manipulated by them become critical. In this work, we use the Coq proof assistant to formalise a λ-calculus with trust types, originally formulated by Ørbæk and Palsberg. We give formal proofs of type soundness, erasure and simulation theorems and also prove decidability of the typing problem. As a result of our formalisation a certified type checker is derived.

Download here

Terminating Constraint Set Satisfiability and Simplification Algorithms for Context-Dependent Overloading

Published in Journal of the Brazilian Computer Society, 2013

Algorithms for constraint set satisfiability and simplification of Haskell type class constraints are used during type inference in order to allow the inference of more accurate types and to detect ambiguity. Unfortunately, both constraint set satisfiability and simplification are in general undecidable, and the use of these algorithms may cause non-termination of type inference. This paper presents algorithms for these problems that terminate on any given input, based on the use of a criterion that is tested on each recursive step.

Download here

Ambiguity and context-dependent overloading

Published in Journal of the Brazilian Computer Society, 2013

This paper discusses ambiguity in the context of languages that support context-dependent overloading, such as Haskell. A type system for a Haskell-like programming language, that supports context-dependent overloading and follow the Hindley-Milner approach of providing context-free type instantiation, allows distinct derivations of the same type for ambiguous expressions. Such expressions are usually rejected by the type inference algorithm, which is thus not complete with respect to the type system. Following the standard definition of ambiguity, satisfiability is tested - i.e. “the world is closed” — if only if overloading is (or should have been) resolved, that is, if and only if there exist unreachable variables in the constraints on types of expressions. Nowadays satisfiability is tested in Haskell, in the presence of multi-parameter type classes, only upon the presence of functional dependencies or an alternative mechanism that specifies conditions for closing the world, and that may happen when there exist or not unreachable type variables in constraints. The satisfiability trigger condition is then given automatically, by the existence of unreachable variables in constraints, and does not need to be specified by programmers, using an extra mechanism.

Download here

Type inference for GADTs and anti-unification

Published in Programming Languages - 19th Brazilian Symposium on Programming Languages., 2015

Nowadays the support of generalized algebraic data types (GADTs) in extensions of Haskell allows functions defined over GADTs to be written without the need for type annotations in some cases and requires type annotations in other cases. In this paper we present a type inference algorithm for GADTs that is based on a closed-world approach to overloading and uses anti-unification and constraint-set satisfiability to infer the relationship between the types of function arguments and result. Through some examples, we show how the proposed algorithm allows more functions defined over GADTs to be written without the need for type annotations.

Download here

Ambiguity and constrained polymorphism

Published in Science of Computer Programming, 2016

This paper considers the problem of ambiguity in Haskell-like languages. The relation between ambiguity and overloading resolution and the disadvantages of following the standard notion of ambiguity in the con- text of constrained polymorphism are exposed and discussed. A new definition of ambiguity is presented, where existence of more than one instance for an expression type is considered only after overloading resolution. We identify overloading resolution by the presence of unreachable variables in constraints on the type of the expression. We discuss advantages of adopting this ambiguity definition in Haskell.

Download here

A Mechanized textbook proof of a type unification algorithm

Published in Formal Methods: Foundations and Applications - 18th Brazilian Symposium on Formal Methods., 2016

Unification is the core of type inference algorithms for mod- ern functional programming languages, like Haskell. As a first step towards a formalization of a type inference algorithm for such programming languages, we present a formalization in Coq of a type unification algorithm that follows classic algorithms presented in programming language textbooks.

Download here

Optional type classes for Haskell

Published in Programming Languages - 20th Brazilian Symposium on Programming Languages., 2016

This paper explores an approach for allowing type classes to be optionally declared by programmers, i.e. programmers can overload symbols without declaring their types in type classes. The type of an overloaded symbol is, if not explicitly defined in a type class, automatically determined from the anti-unification of instance types defined for the symbol in the relevant module. This depends on a modularization of instance visibility, as well as on a redefinition of Haskell’s ambiguity rule. The paper presents the modifications to Haskell’s module system that are necessary for allowing instances to have a modular scope, based on previous work by the authors. The definition of the type of overloaded symbols as the anti-unification of available instance types and the redefined ambiguity rule are also based on previous works by the authors. The added flexibility to Haskell-style of overloading is illustrated by defining a type system and by showing how overloaded record fields can be easily allowed with such a type system.

Download here

Certified derivative based parsing of regular expressions

Published in Programming Languages - 20th Brazilian Symposium on Programming Languages., 2016

We describe the formalization of a certified algorithm for regular expression parsing based on Brzozowski derivatives, in the dependently typed language Idris. The formalized algorithm produces a proof that an input string matches a given regular expression or a proof that no matching exists. A tool for regular expression based search in the style of the well known GNU grep has been developed with the certified algorithm, and practical experiments were conducted with this tool.

Download here

Compilação parcial de programas escritos em C

Published in Programming Languages - 20th Brazilian Symposium on Programming Languages., 2016

Há situações em que é desejável compilar programas cujo código fonte não está totalmente disponível. Tal necessidade aparece em ambientes integrados de desenvolvimento que auto-completam partes do programa, por exemplo, e já levou à criação de compiladores parciais para linguagens como Java e Python. Por outro lado, até o momento não existe um compilador parcial de programas escritos em C. Este artigo preenche essa lacuna. Com tal propósito, descreve-se um parser capaz de escanear código fonte C incompleto, e um inferidor de tipos capaz de reconstruir definições de tipos cujas declarações não estão presentes naquele código fonte. Ao contrário de algoritmos de inferência de tipos usados em linguagens funcionais, a técnica proposta neste trabalho reconstrói declarações ausentes de tipos algébricos, criando novas definições que tendem a aproximar aquelas presentes no programa original. Um protótipo descrevendo a nova abordagem é apresentado. Tal protótipo é capaz de reconstruir trechos não triviais de programas parcialmente disponíveis, permitindo a geração de código binário executável a partir deles.

Download here

Certified bit-coded regular expression parsing

Published in 21th Brazilian Symposium on Programming Languages, 2017

We describe the formalization of a regular expression (RE) parsing algorithm that produces a bit representation of its parse tree in the dependently typed language Agda. The algorithm computes bit-codes using Brzozowski derivatives and we prove that produced codes are equivalent to parse trees ensuring soundness and completeness w.r.t an inductive RE semantics. We include the certified algorithm in a tool developed by us, named verigrep, for regular expression based search in the style of the well known GNU grep. Practical experiments conducted with this tool are reported.

Download here

A domain specific language for drum beat programming.

Published in Brazilian Symposium on Computer Music 2017, 2017

This paper describes HDrum, a Domain Specific Language for writing drum patterns. Programs written in HDrum look similar to the grids, available in sequencers and drum machines, used to program drum beats, but as the language has an inductive definition we can write abstractions to manipulate drum patterns. HDrum is embedded in the Haskell functional program- ming language, hence it is possible to implement Haskell functions that manipulate patterns generating new patterns. The paper also presents a case study using HDrum, an implementation of The Clapping Music, a minimalistic music written by Steve Reich in 1972. The HDrum language is currently compiled into midi files.

Download here

Inference of Static Semantics for Incomplete C Programs

Published in ACM POPL - Principles of Programming Languages, 2018

Incomplete source code naturally emerges in software development: during the design phase, while evolving, testing and analyzing programs. Therefore, the ability to understand partial programs is a valuable asset. However, this problem is still unsolved in the C programming language. Difficulties stem from the fact that parsing C requires, not only syntax, but also semantic information. Furthermore, inferring types so that they respect C’s type system is a challenging task. In this paper we present a technique that lets us solve these problems. We provide a unification-based type inference capable of dealing with C intricacies. The ideas we present let us reconstruct partial C programs into complete well-typed ones. Such program reconstruction has several applications: enabling static analysis tools in scenarios where software components may be absent; improving static analysis tools that do not rely on build-speci cations; allowing stub-generation and testing tools to work on snippets; and assisting programmers on the extraction of reusable data-structures out of the program parts that use them. Our evaluation is performed on source code from a variety of C libraries such as GNU’s Coreutils, GNULib, GNOME’s GLib, and GDSL; on implementations from Sedgewick’s books; and on snippets from popular open-source projects like CPython, FreeBSD, and Git.

Download here

Formal Semantics for Java-like Languages and Research Opportunities

Published in Revista de Informática Teórica e Aplicada, 2018

Currently, Java is one of the most used programming languages, being adopted in many large projects, where applications reach a level of complexity for which manual testing and human inspection are not enough to guarantee quality in software development. Because of that, there is a growing research field that concerns the formalization of small subsets of Java-like languages aimed to conduct studies that were impossible to achieve through informal approaches. In this context, the objective of this paper is twofold: the discussion of the state-of-the-art on Java-like semantics and the presentation of research opportunities in this area. For the first goal, we present a research about Java-like formal semantics, filtering those that provide some insights in type-safety proofs, choosing the four most cited projects to be presented in details. We also briefly present some related studies that extended the originals aggregating useful features. Additionally, we provide a comparison between the most cited projects in order to show which functionalities are covered by each one of them. As for the second goal, we discuss possible future studies that can be performed by using the presented formal semantics.

Download here

Generating Random Well-Typed Featherweight Java Programs Using QuickCheck

Published in CLEI - The Latin American Computing Conference, 2018

Currently, Java is one of the most used programming language, being adopted in many large projects, where applications reach a level of complexity for which manual testing and human inspection are not enough to guarantee quality in software development. Even when using automated unit tests, such tests rarely cover all interesting cases of code, which means that a bug could never be discovered, once the code is tested against the same set of rules over and over again. This paper addresses the problem of generating random well-typed programs in the context of Featherweight Java, a well-known object-oriented calculus, using QuickCheck, a Haskell library for property-based testing.

Download here

Type Inference for GADTs, OutsideIn and Anti-unification

Published in SBLP - Brazilian Syposium on Programming Languages, 2018

Support for generalized algebraic data types (GADT) in extensions of Haskell allows functions defined over GADTs to be written without the need for type annotations in some cases, but it requires type annotations in most of them. This paper presents a type inference algorithm for GADTs that extends OutsideIn algorithm using anti-unification to capture the relationship between the types of arguments and result of GADT functions. This approach allows inference in cases where the relationship between types of pattern matches is explicit in the code, allowing the type annotation in cases where the relationship is not explicit.

Download here

Towards certified virtual machine-based regular expression parsing

Published in SBLP - Brazilian Syposium on Programming Languages, 2018

Regular expressions (REs) are pervasive in computing. We use REs in text editors, string search tools (like GNU-Grep) and lexical analysers generators. Most of these tools rely on converting regular expressions to its corresponding finite state machine or use REs derivatives for directly parse an input string. In this work, we investigate the suitability of another approach: instead of using derivatives or generate a finite state machine for a given RE, we developed a virtual machine (VM) for parsing regular languages, in such a way that a RE is merely a program executed by the VM over the input string. We developed a prototype implementation in Haskell, tested it using QuickCheck and provided proof sketches of its correctness with respect to RE standard inductive semantics.

Download here

Property-Based Testing for Lambda Expressions Semantics in Featherweight Java

Published in SBLP - Brazilian Syposium on Programming Languages, 2018

The release of Java 8 represents one of the most significant updates to the Java language since its inception. The addition of lambda-expressions allows the treatment of code as data in a compact way, improving the language expressivity. This paper addresses the problem of defining rigorous semantics for new features of Java, such as lambda-expressions and default methods, using Featherweight Java (FJ), a well-known object-oriented calculus. To accomplish this task, we embed the formalization of these new features in two different semantics, checking them for safety properties using QuickCheck, a property-based testing library for Haskell.

Download here

A Type-Directed Algorithm to Generate Well-Typed Featherweight Java Programs

Published in SBMF - Brazilian Syposium on Formal Methods, 2018

Property-based testing of compilers or programming languages semantics is difficult to accomplish because it is hard to design a random generator for valid programs. Most compiler test tools do not have a well-specified way of generating type-correct programs, which is a requirement for such testing activities. In this work, we formalize a type-directed procedure to generate random well-typed programs in the context of Featherweight Java, a well-known object-oriented calculus for the Java programming language. We implement the approach using the Haskell programming language and verify it against relevant properties using QuickCheck, a library for property-based testing.

Download here

Transactional Boosting no Glasgow Haskell Compiler

Published in WSCAD2018 - XIX Simpósio Brasileiro de Computação de Alto Desempenho, 2018

Transactional Boosting é uma técnica que pode ser usada para transformar ações linearmente concorrentes em ações transacionalmente concorrentes, possibilitando assim sua utilização em blocos transacionais. Esta técnica pode ser utilizada para resolução de falsos conflitos, evitando assim a perda de desempenho de algumas aplicações. O objetivo deste trabalho é apresentar uma extensão do STM Haskell, bem como as modificações necessárias ao Run-Time System do compilador, para permitir o desenvolvimento de aplicações que utilizam Transactional Boosting, e assim apresentar a viabilidade desta técnica em Haskell.

Download here

talks

Programação com tipos dependentes em Agda

Published: April 01, 2014

Tipos dependentes permitem codificar a espeficação de funções em seus tipos, permitindo o desenvolvimento de software correto por construção. Nesta palestra apresentarei uma introdução à linguagem Agda e como tipos dependentes permitem codificar no tipo de funções suas propriedades de correção.

Rodrigo Ribeiro

Posts by Collection

projects

publications

talks

teaching