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.