Por Diogo Poças (LASIGE, DI-FCUL).

Between a world of darkness (finite, inductive types), and a world of light (infinite, coinductive types), there are different shades of grey. We systematically study these shades by means of parameterised equational definitions. We identify four such hues: recursive, 1-counter, pushdown, and 2-counter; and show that they are all dissimilar by establishing correspondences with classes of automata. This allows us to obtain decidability and undecidability results for the problems of type formation, type equivalence and type duality under the different classes of types. [Joint work with Simon Gay and Vasco T. Vasconcelos]

Zoom