[logic-ml] 講演会 (Andreas Abel 氏，Andrea Vezzosi 氏)

[Atsushi Igarashi]

皆様，

京都大学の五十嵐です．

以下の要領で Chalmers 大の Andreas Abel さん，Andrea Vezzosi さんの講演
会を実施いたしますので，ふるってご参加ください．

どうぞよろしくお願いいたします．
--
五十嵐 淳 (IGARASHI Atsushi)
E-mail: igarashi at kuis.kyoto-u.ac.jp
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