A Modal Proof Theory for Polynomial Coalgebras Export

@mastersthesis{citeulike:566417, abstract = {The abstract mathematical structures known as coalgebras are of increasing interest in computer science for their use in modelling certain types of data structures and programs. Traditional algebraic methods describe objects in terms of their construction, whilst coalgebraic methods describe objects in terms of their decomposition, or observational behaviour. The latter techniques are particularly useful for modelling infinite data structures and providing semantics for object-oriented programming languages, such as Java. There have been many different logics developed for reasoning about coalgebras of particular functors, most involving modal logic. We define a modal logic for coalgebras of polynomial functors, extending RossŸiger'€™s logic [34], whose proof theory was limited to using finite constant sets, by adding an operator from Goldblatt [11]. From the semantics we define a canonical coalgebra that provides a natural construction of a final coalgebra for the relevant functor. We then give an infinitary axiomatization and syntactic proof relation that is sound and complete for functors constructed from countable constant sets.}, author = {Friggens, David}, citeulike-article-id = {566417}, keywords = {coalgebra, final\_coalgebra, modal\_logic, polynomial\_functor, thesis-msc}, posted-at = {2006-03-28 03:21:12}, priority = {0}, school = {Victoria University of Wellington}, title = {A Modal Proof Theory for Polynomial Coalgebras}, year = {2004} }

TY - THES ID - citeulike:566417 L3 - citeulike-article-id:566417 N2 - The abstract mathematical structures known as coalgebras are of increasing interest in computer science for their use in modelling certain types of data structures and programs. Traditional algebraic methods describe objects in terms of their construction, whilst coalgebraic methods describe objects in terms of their decomposition, or observational behaviour. The latter techniques are particularly useful for modelling infinite data structures and providing semantics for object-oriented programming languages, such as Java. There have been many different logics developed for reasoning about coalgebras of particular functors, most involving modal logic. We define a modal logic for coalgebras of polynomial functors, extending RossŸiger'€™s logic [34], whose proof theory was limited to using finite constant sets, by adding an operator from Goldblatt [11]. From the semantics we define a canonical coalgebra that provides a natural construction of a final coalgebra for the relevant functor. We then give an infinitary axiomatization and syntactic proof relation that is sound and complete for functors constructed from countable constant sets. TI - A Modal Proof Theory for Polynomial Coalgebras PB - Victoria University of Wellington KW - coalgebra KW - final_coalgebra KW - modal_logic KW - polynomial_functor KW - thesis-msc AU - Friggens, David PY - 2004/// ER -