Rodrigo Ribeiro

Rodrigo Ribeiro

Lecturer at Computer Science Departament

Blog posts

2019

2018

Formalizing a list-zipper library in Coq

10 minute read

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

4 minute read

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:

QuickChick - Testes baseado em propriedades em Coq

13 minute read

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

6 minute read

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

19 minute read

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

18 minute read

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.

Lógica em Coq

18 minute read

Published:

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

2016

Records, Modules and Instance Arguments in Agda

7 minute read

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.

2015

Developing Dependently Typed Programs in Agda - Part 3

13 minute read

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

less than 1 minute read

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

1 minute read

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:

2014

Maniac Spring

less than 1 minute read

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…).