# Sitemap

A list of all the posts and pages found on the site. For you robots out there is an XML version available for digesting as well.

## Markdown

This is a page not in th emain menu

Published:

Published:

Published:

Published:

# Introdução

## Formalizing a list-zipper library in Coq

Published:

These days I’ve been thinking a lot about formalizations about low level code, specially about AVR microcontrollers. When you think about low level code, one annoying thing is how to implement jump-like instructions in a purely functional way. One possible solution is to use functional zippers. In this post, I’ll discuss a simple implementation of functional zippers, inspired by ListZipper Haskell package. In fact, the formalization that I’ll describe is a certification of this library using Coq proof assistant.

## Estudo de caso - Formalizando o Insertion sort

Published:

O insertion sort é um conhecido algoritmo de ordenação que consiste em repetidamente inserir um elemento em uma lista previamente ordenada. Uma possível implementação em Coq deste algoritmo seria:

Published:

Não é incomum gastarmos muitas horas de esforço na prova de uma propriedade incorreta, ou mesmo com suposições inadequadas. Uma maneira para contornar essa situação é o uso de testes baseados em propriedades para encontrar contra-exemplos de propriedades de interesse o quanto antes.

## Classes de tipos em Coq

Published:

Classes de tipos são dos um das mais distintivas características da linguagem Haskell. De maneira simples, classes de tipos permitem ao programador definir novos símbolos sobrecarregados na linguagem. Até recentemente, Coq não suportava a definição de classes de tipos. Em versões mais recentes, esse mecanismo foi incluído e permite a definição de funções (e também provas) sobrecarregadas, o que possibilita uma maior reutilização de formalizações.

## Formalizando uma linguagem simples

Published:

Uma das aplicações que popularizou o uso de assistentes de prova foi a formalização de resultados sobre semântica formal de linguagens de programação. Atualmente, a maioria dos trabalhos publicados sobre semântica formal em conferências como o ACM Principles on Programming Languages usa algum assistente de prova para formalização de seus resultados. Nesta seção utilizaremos Coq para formalizar uma pequena linguagem de expressões.

## Programação com tipos dependentes

Published:

Até o presente momento devotamos nossa atenção a usar Coq para demonstrar simples fatos matemáticos e a explicar o uso da ferramenta. A partir deste ponto, vamos apresentar como o uso de automação de provas e tipos indutivos fornece um arcabouço apropriado para desenvolver programas em conjunto com suas respectivas provas de correção.

Published:

Published:

## Lógica em Coq

Published:

Nesta seção apresentaremos como demonstrar resultados conhecidos da lógica proposicional e de predicados utilizando Coq.

Published:

## Records, Modules and Instance Arguments in Agda

Published:

Lately, I’m having some trouble with records and its relation with modules in Agda. Basically, I’m trying to formalize some results from category theory and algebra in Agda and I’m using records to represent a hierarchy of algebraic structures.

## Understanding Category Theory Using Agda - Part 1

Published:

After a long silence, I decided to blog again. Now, I’ll start a series on implementing Category Theory using Agda.

## Developing Dependently Typed Programs in Agda - Part 3

Published:

And finally I’ve decided to start the third part of my post series on Developing Dependently Typed Programs in Agda. In this post, I’ll explain how to use Agda to develop a certified interpreter for the simply typed $\lambda$-calculus.

## New blog layout and Kindle Paperwhite

Published:

As you can see, I’ve updated my blog to use pure Jekyll instead of Jekyll Bootstrap. The main reason for the change was the lack of updates of Jekyll Bootstrap. But, since blogging process and structure was the same, I just decide to use plain Jekyll. In order to get this beautiful layout, I google for some templates and find Poole, a ready template for Jekyll blogs.

## Maniac Spring Results

Published:

So, after a long pause, I’ll start to blog again. And, since my last post was about the so called Maniac Spring, where I’ve set some ambitious objectives, let’s see what I’ve finished:

## Maniac Spring

Published:

Inspired by Brent Yourgey’s post, I’ve decided to setup not a Maniac week, but a Maniac Spring! The idea is just to eliminate as many distractions as possible, and just work (yes, I’ll reduce coffee time…).

Published:

Published:

# Fist things, first…

## 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.

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

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

## 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.

## 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.

## 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.

## 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.

## 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.

## 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.

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.

Published in Journal of the Brazilian Computer Society, 2013

## 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.

## Ambiguity and constrained polymorphism

Published in Science of Computer Programming, 2016

## 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.

## 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.

## 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.

## 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.

## 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.

## 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.

## 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.

## 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.

## 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.

## 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.

## 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.

## 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.

## 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.

## 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.

## Programação com tipos dependentes em Agda

Published:

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.

## Mechanized textbook proof of a type unification algorithm

Published:

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.

## Certified bit-coded regular expression parsing

Published:

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.

## Verificação de Software

Published:

Essa palestra apresenta a importância da verificação de software e alguns problemas em aberto na área. Palestra para alunos do primeiro período do curso de ciência da computação da UFOP.

## Towards certified virtual machine based regular expression parsing

Published:

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.

## Teaching duties in 2017/2

Courses, Universidade Federal de Ouro Preto, Department of Computing, 2017

Information about the classes in Moodle.

## Teaching duties in 2018/1

Courses, Universidade Federal de Ouro Preto, Department of Computing, 2018

Information about the classes in Moodle.

## Teaching duties in 2018/2

Courses, Universidade Federal de Ouro Preto, Department of Computing, 2018

Information about the classes in Moodle.

## Teaching duties in 2019/1

Courses, Universidade Federal de Ouro Preto, Department of Computing, 2019

Information about the classes in Moodle.

## Teaching duties in 2019/2

Courses, Universidade Federal de Ouro Preto, Department of Computing, 2019

Information about the classes in Moodle.