Talk "Modeling and reasoning with I-polynomial data types"

by Peter Padawitz

Fri, 01 April 2016 at 11:50 am in Eindhoven, The Netherlands

Abstract: Most constructor-or destructor-based models can be presented as I-polynomial data types. I is a set that consists of the base sets (constant functors) and the index sets of the sum or product types involved in the model's signature. The trees representing the elements of a (co)free model of an I-polynomial data type reveal the duality between constructors and destructors more clearly than previous (co)term notions do. Well-known methods of equational, first-order or modal specification and reasoning - such as the solution of iterative equations - can be generalized smoothly to I-polynomial data types.