Talks and presentations

Towards certified virtual machine based regular expression parsing

September 20, 2018

XXII Brazilian Symposium on Programming Languages, SBLP, São Carlos - SP

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.

Verificação de Software

January 19, 2018

Palestra para a disciplina Introdução à ciência da computação, UFOP, Ouro Preto - MG

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.

Certified bit-coded regular expression parsing

September 21, 2017

Conference proceedings talk, XX Brazilian Symposium on Programming Languages, Fortaleza - CE

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.

Mechanized textbook proof of a type unification algorithm

September 22, 2015

Talk, Brazilian Symposium on Formal Methods, London, UK

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.

Programação com tipos dependentes em Agda

April 01, 2014

Talk, UDESC, Department of Computing, Joinville, Santa Catarina

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.