Compositional Coinduction with Sized Types – Dr. Andreas Abel

Event details

  • When: 16th February 2018 12:00 - 13:00
  • Where: Cole 1.33b
  • Format: Seminar

Abstract:

Formal languages and automata are taught to every computer science
student.  However, the student will most likely not see the beautiful
coalgebraic foundations, which use coindutive reasoning.

In this talk, I recapitulate how infinite tries can represent formal
languages (sets of strings).  I explain Agda’s coinduction mechanism
based on copatterns and sized types demonstrate that it allows an
elegant representation of the usual language constructions like union,
concatenation, and Kleene star, with the help of Brzozowski
derivatives.

Leave a Reply