皆様，
京都大学の五十嵐です．
以下の要領で Chalmers 大の Andreas Abel さん，Andrea Vezzosi さんの講演 会を実施いたしますので，ふるってご参加ください．
どうぞよろしくお願いいたします． -- 五十嵐 淳 (IGARASHI Atsushi) E-mail: [email protected] url: http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/
====================================================================== 日時: 3/2(水) 13:30～15:30 場所: 京都大学 吉田キャンパス 総合研究７号館１階セミナー室１(１２７号室)
講演その１(13:30～14:30)
Speaker: Andrea Vezzosi (Chalmers) Title: Open Problems with Sized Types in Agda
Abstract:
Sized Types let us give recursive definitions by well-founded induction on an the abstract type "Size", and so ensuring totality through types.
This talk will discuss two problems that arise when using Sized Types in a dependently typed language:
- Totality tells us that closed programs will not go wrong, but when typechecking a dependently typed language we also reduce terms with free variables, and go under binders, to reach a normal form. The current restrictions on definitions to guarantee every term has a normal form hurt expressivity, we propose a closer interaction of sizes and reduction instead.
- When reasoning about programs defined with sizes types one often wishes to show that the size used doesn't affect the result in a significant way. We show a parallel with parametric polymorphism that could lead to more powerful reasoning principles for sizes.
講演その２(14:30～15:30)
Speaker: Andreas Abel
Title: Interactive Programs and Objects, Functionally --- Via Coinduction with Copatterns and Sized Types in Agda
Abstract:
Copattern matching is an extension of pattern matching in functional languages. It allows us to define an infinite structure (e.g. a stream) by what we can observe of it (e.g., what is its head?, what is its tail?). This has an analogue in object-oriented programming languages where an object is defined on how it responds to messages or method invocation, resp. Following Setzer, objects can be implemented coinductively in type theory; they are entities that respond to a message with some result and a new version of themselves. Similarly, following Hancock and Setzer, interactive programs can be seen as infinite processes that issue a command and continue in accordance with the response their received, potentially for all eternity.
In this talk, we give an introduction to coinduction in the type-theoretic language Agda. We show how copatterns and sized types enable us to elegantly encode objects and interactive programs in type theory. The talk might close with a short demo of 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