Date/Time
Date(s) - 30/06/2015
2:00 pm - 4:30 pm
Location
The School of Computing, University of Dundee
SICSA DVF Professor Patricia Johann; Interleaving Data and Effects
We are pleased to let you know that Professor Patricia Johann will be visiting the School of Computing at the University of Dundee on 30 June 2015 to give a talk on Interleaving Data and Effects.
Schedule:
14.00 – 15.00: The DVF talk: Interleaving Data and Effects
15.00 – 15.15: Coffee break
15.15 – 16.30: Discussion Session
Abstract:
The study of programming with and reasoning about inductive datatypes such as lists and trees has benefitted from the simple categorical principle of initial algebras. In initial algebra semantics, each inductive datatype is represented by an initial f-algebra for an appropriate functor f. The initial algebra principle then supports the straightforward derivation of definitional principles and proof principles for these datatypes. This technique has been expanded to a whole methodology of structured functional programming, sometimes called origami programming.
This talk will show how to extend initial algebra semantics from pure inductive datatypes to inductive datatypes interleaved with computational effects. Inductive datatypes interleaved with effects arise naturally in many computational settings. For example, incrementally reading characters from a file generates a list of characters interleaved with input/output actions, and lazily constructed infinite values can be represented by pure data interleaved with the possibility of non-terminating computation. Straightforward application of initial algebra techniques to effectful datatypes leads either to unsound conclusions if we ignore the possibility of effects, or to unnecessarily complicated reasoning because the pure and effectful concerns must be considered simultaneously. Pure and effectful concerns can be separated using the abstraction of initial f-and-m-algebras, where the functor f describes the pure part of a datatype and the monad m describes the interleaved effects. Because initial f-and-m-algebras are the analogue for the effectful setting of initial f-algebras, they support the extension of the standard definitional and proof principles to the effectful setting.
This is joint work with Bob Atkey, Neil Ghani, and Bart Jacobs
Bio:
Patricia Johann is Professor of Computer Science at Appalachian State University. Formerly, she was a Reader at the University of Strathclyde, where she was one of the founders of the Mathematically Structured Programming group. She has over 25 years of post-doctoral experience in research and teaching in computer science. Her research interests include functional programming, type theory, category theory, as well as logic programming and automated deduction.
