module TalkKyoto2016 where

--             Interactive Programs and Objects, Functionally
--        Via Coinduction with Copatterns and Sized Types in Agda

--                              Andreas Abel
--             Department of Computer Science and Engineering
--                   Chalmers and Universität Göteborg

--                           Talk given at the
--            Department of Communications and Computer Engineering
--            Graduate School of Informatics, Kyoto University
--                              Kyoto, Japan
--                              2 March 2016

-- In this talk, I give an introduction to coinduction in the
-- type-theoretic language Agda.  I show how copatterns and sized types
-- enable us to elegantly encode objects and interactive programs in type
-- theory.  As a case study, we have implemented a rudimentary graphical
-- program written in Agda using a foreign-function interface to Haskell.

-- This is joint work with Stephan Adelsberger and Anton Setzer.
-- An accompanying draft is available at
--
--          http://www.cse.chalmers.se/~abela/index.html#ooAgda


import Coalgebras  -- 1. Coalgebras in Agda

import SizedTypes  -- 2. Sized version of coalgebras

import IOTrees     -- 3. Interaction trees

import IOObjects   -- 4. Objects doing I/O