# Posts by Tags

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

Published:

Published:

# Fist things, first…

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

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:

## QuickChick - Testes baseado em propriedades em Coq

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:

Published:

# Introduction

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

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: