[Alta-Logic] Talk by Brigitte Pientka (McGill)

[Robin Cockett]

Time: 2:00pm Tuesday 31st May

Place: ICT616

Title: Programming Coinductive Proofs Using Observations

Speaker: Brigitte Pientka (McGill)

Abstract:
Coinduction is a key proof technique to establish properties about systems
that continue to run and produce results (i.e. network or communications
protocols, I/O interaction, data streams, or processes) . Yet, mechanizing
coinductive proofs about formal systems and representing, generating and
manipulating such proofs remains challenging. In this talk, we develop the
idea of programming coinductive proofs dual to the idea of programming
inductive proofs. Unlike properties about finite data which can be defined
by constructing a derivation, properties about infinite data can be
described by the possible observations we can make. Dual to pattern
matching, a tool for analyzing finite data, we develop the concept of
copattern matching, which allows us to describe properties about infinite
data. This leads to a symmetric proof language where pattern matching on
finite and infinite data can be mixed.

Bio:
Brigitte Pientka is an Associate Professor in the School of Computer
Science at McGill University, Montreal, Canada. She received her Ph.D. from
Carnegie Mellon University and recently has been awarded a Humboldt
Research Fellowship.  Her research interest lies in developing a
theoretical and practical foundation for building and reasoning about
reliable safe software systems. To achieve this goal, she combines
theoretical research on the logical foundations of computer science in
programming languages and verification with system building.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.ucalgary.ca/pipermail/alta-logic-l/attachments/20160529/960d8bfd/attachment.html