(This text includes Japanese characters.)

--------------------------------------------------------------------
プログラミング言語セミナーのお知らせ

以下のようなセミナーを行います。
みなさまの御参加をお待ちしております。

問い合わせ先：
長谷川真人（京都大学数理解析研究所）
hassei@kurims.kyoto-u.ac.jp

--------------------------------------------------------------------
日時	８月５日（月）１６：００〜
会場	京都大学数理解析研究所２階２０２号室

	１６：００〜 五十嵐淳 氏（京大・情報）
	「On Variance-Based Subtyping for Parametric Types」

	１７：００〜 住井英二郎 氏（東大・情報）
	「Syntactic Logical Relations for Perfect Encryption,
	  Higher-Order References and First-Class Channels」

--------------------------------------------------------------------
On Variance-Based Subtyping for Parametric Types

We develop the mechanism of variant parametric types, inspired by
structural virtual types by Thorup and Torgersen, as a means to
enhance synergy between parametric and inclusive polymorphism in
object-oriented languages. Variant parametric types are used to
control both subtyping between different instantiations of one generic
class and the visibility of their fields and methods. On one hand, one
parametric class can be used as either covariant, contravariant, or
bivariant by attaching a variance annotation---which can be either +,
-, or *, respectively---to a type argument. On the other hand, the
type system prohibits certain method/field accesses through variant
parametric types, when those accesses can otherwise make the program
unsafe. By exploiting variant parametric types, a programmer can write
generic code abstractions working on a wide range of parametric types
in a safe way. For instance, a method that only reads the elements of
a container of strings can be easily modified so that it can accept
containers of any subtype of string.

The theoretical issues are studied by extending Featherweight GJ---an
existing core calculus for Java with generics---with variant
parametric types. By exploiting the intuitive connection to bounded
existential types, we develop a sound type system for the extended
calculus.

This is joint work with Mirko Viroli.

--------------------------------------------------------------------
Syntactic Logical Relations for Perfect Encryption, Higher-Order
References and First-Class Channels

\emph{Logical relations} are relations between values in a programming
language, defined by induction on their types.  They were developed in
the domain of denotational semantics for proving various relationships
among mathematical models of typed lambda-calculi.  In particular,
they are known to be useful for proving contextual equivalence of
different implementations of abstract types [Reynolds 83] and deriving
so-called "free theorems" about polymorphic functions [Wadler 89].

This talk presents the definitions and applications of logical
relations for a broader range of programming constructs such as
(perfect) encryption, (higher-order) references, and (first-class)
channels in concurrent languages.  In spite of this diversity, the
logical relations are based on a single idea of associating each
\emph{generative name} $n$ with a relation $\phi(n)$ between values
involved in $n$.  All of these developments are syntactic and
operational: that is, there are no CPOs and no categories.

Half of this talk is about premature work.  Suggestions and
discussions are welcome.

--------------------------------------------------------------------