Programação com tipos dependentes em Agda

Date:

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.

Slides

Source code