Talk "Compositional Coinduction in Agda"

by Andreas Abel

Tue, 10 January 2017 at 10:30 am in Binz (Rügen), Germany

Abstract: Agda is a dependently-typed functional programming language based on Martin-Löf Type Theory, and at the same time, a proof assistant for the formalization and verification of mathematical theories and systems. In the last couple of years, Agda has been extended by sized types and definition by copattern matching to facilitate programming and reasoning by well-founded coinduction. In this talk, I briefly review the theoretical foundations of well-founded coinduction and present a recent case-study: the formalization of formal languages in Agda, and proofs of Kleene algebra laws by well-founded coinduction and equational reasoning with bisimilarity.