FLOPS

日曜から水曜までFLOPS 2006という関数型・論理型言語の国際学会へいってきます。JavaやSchemeで有名なGuy Steele (invited speaker)とか、Haskellのmonadやtype classで有名なPhilip Wadler (program co-chair)がきます。僕も一応はプログラム委員なのですが、session chairの割り当てが来ないのは、やらなくて良いということだろうか。いや、メインの仕事である査読と議論は以前にちゃんとやりましたけど。どきどき。

追記：FLOPSで日本へ来る方々の、他の場所での講演。転載に問題があったらいってください。こういう情報はJSSST-PROとかSonotenoとか、関連するメーリングリストにアナウンスされます。関連研究室にいれば入れと言われるでしょうし、そうでなくても耳にタコができるほど「聞きに行け」と言われるかもしれませんが。

Guy Steele博士の講演（問い合わせ先：東京大学 萩谷昌巳先生 hagiya アットマーク is.s.u-tokyo.ac.jp）

日時: 4月27日(木) 15:30〜
場所: 理学部7号館214号室
タイトル: Parallel Programming and Parallel Abstractions in Fortress
要旨
The Programming Language Research Group at Sun Microsystems Laboratories seeks to apply lessons learned from the Java (TM) Programming Language to the next generation of programming languages. The Java language supports platform-independent parallel programming with explicit multithreading and explicit locks. As part of the DARPA program for High Productivity Computing Systems, we are developing Fortress, a language intended to support large-scale scientific computation. One of the design principles is that parallelism be encouraged everywhere (for example, it is intentionally just a little bit harder to write a sequential loop than a parallel loop). Another is to have rich mechanisms for encapsulation and abstraction; the idea is to have a fairly complicated language for library writers that enables them to write libraries that present a relatively simple set of interfaces to the application programmer. We will discuss ideas for using a rich polymorphic type system to organize multithreading and data distribution on large parallel machines. The net result is similar in some ways to data distribution facilities in other languages such as HPF and Chapel, but more open-ended, because in Fortress the facilities are defined by user-replaceable libraries rather than wired into the compiler.

Benjamin Werner教授［今までにも出てきたCoqの偉い人］の講演（問い合わせ先：国立情報学研究所 龍田真先生 tatsuta アットマーク nii.ac.jp）

Date: April 27, 14:00--16:00
場所: 国立情報学研究所 12階 講義室2
Title: Computational Formal Proofs
Abstract:
The idea of formal mathematical proofs is that every logical step of reasoning is made explicit, so that the proof can be formally verified by a computer using a so called proof-assistant. On the other hand, large computations performed by a computers are necessary in order to establish some mathematical results like the primality of large numbers, the four colour theorem or Kepler's conjecture. I will explain how computational formalisms, like the one implemented in Coq allow to reconcile these two roles of the computer for mathematics. I will illustrate this through examples coming from primality proofs and the recent formalization of the four colour theorem in Coq.

Philip Wadler教授の講演（問い合わせ先：京都大学 長谷川真人先生 hassei アットマーク kurims.kyoto-u.ac.jp）

Links: Web Programming without Tiers.
２００６年４月２８日（金）１４時〜
京都大学数理解析研究所１階１１５号室
Links is a programming language for web applications. Links generates code for all three tiers of a web application from a single source, compiling into JavaScript to run on the client and into SQL to run on the database. Links provides support for rich clients running in what has been dubbed `Ajax' style. Links programs are scalable in the sense that session state is preserved in the client rather than the server, in contrast to other approaches such as Java Servlets or PLT Scheme.

Philip Wadler教授の講演２（問い合わせ先：国立情報学研究所 龍田真先生 tatsuta アットマーク nii.ac.jp）

Date: May 1, 14:00--16:00
場所: 国立情報学研究所 12階 講義室2
Title: Call-by-Value is Dual to Call-by-Name Reloaded
Abstract:
The rules of classical logic may be formulated in pairs corresponding to De Morgan duals: rules about "and" are dual to rules about "or". Wadler (2003), inspired by Curien and Herbelin (2000), presents a dual calculus in which exchanging "and" with "or" in types also exchanges call-by-value with call-by-name in evaluations. Just as the lambda calculus (of Church 1932,1940) corresponds to the intuitionistic natural deduction (of Gentzen 1935), the dual calculus corresponds to the classical sequent calculus (also of Gentzen 1935). This talk describes dual calculus, discusses its relationship to the mu calculus of Parigot (1992) and the Symmetric Lambda Calculus of Barbanera and Berardi (1996), and suggests further directions of research that may be of interest to the rewriting community.

Guy Steele博士の講演２（問い合わせ先：京都大学 八杉昌宏先生 yasugi アットマーク kuis.kyoto-u.ac.jp）［東大での講演と同じに見えますが、要旨をよく読むと後半が違う！］

日時: 2006年5月2日（火） 13:00--14:30
場所: 京都大学 工学部10号館 1階 第1講義室
タイトル: The Fortress Programming Language
講演要旨:
The Programming Language Research Group at Sun Microsystems Laboratories is trying to apply lessons learned from the Java (TM) Programming Language to the next generation of programming languages. The Java language supports platform-independent parallel programming with explicit multithreading and explicit locks. As part of the DARPA program for High Productivity Computing Systems, we are developing Fortress, a language intended to support large-scale scientific computation. One of the design principles is that parallelism be encouraged everywhere (for example, it is intentionally just a little bit harder to write a sequential loop than a parallel loop). Another design principle is to have rich mechanisms for encapsulation and abstraction; the idea is to have a fairly complicated language for library writers that enables them to write libraries that present a relatively simple set of interfaces to the application programmer. A third design principle is to try to use standard mathematical notation as part of the programming language wherever possible; this is an old idea that failed in the 1960s, but the modern widespread acceptance of Unicode makes it easier to revisit the idea. We will discuss these design principles and show some examples of Fortress code to illustrate them.