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.
Published:
After a long silence, I decided to blog again. Now, I’ll start a series on implementing Category Theory using Agda.
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:
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:
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.
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.
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.
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.
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:
Published:
Nesta seção apresentaremos como demonstrar resultados conhecidos da lógica proposicional e de predicados utilizando Coq.
Published:
Published:
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.
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:
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…).