桜井貴文 (千葉大学), Reduction-Preserving Translations from Classical to Intuitionistic Logic
We present strict reduction-preserving translations from classical type systems to intuitionistic type systems. The classical type systems we consider are lambda-bar-mu, call-by-name lambda-bar-mu-mu-tilde, and call-by-value lambda-bar-mu-mu-tilde (subsystems of lambda-bar-mu-mu-tilde) by Curien and Herbelin, and lambda-mu by Parigot. The contributions of this work are the new translations of lambda-mu and call-by-name lambda-bar-mu-mu-tilde and the systematic view of the various translations. To achieve these results, we introduce several simple translations and derive our new translations and the known translations by composing the simple translations. The immediate consequence of our translations is the strong normalization property of each type system.
蓮尾一郎 (京都大学), The Microcosm Principle and 2-Dimensional SOS
We extend the well-developed framework of structural operational semantics (SOS) into another dimension. Focusing on well-behaved GSOS rules, we present their new interpretation that derives process operations that act on labeled transition systems themselves. The conventional interpretation arises canonically from ours. The situation is much like a classical one where algebraic operations are defined both on NFAs and on regular languages. Relating the two dimensions, we prove a general compositionality result that supports modular design of systems. Our framework is categorical; it is based on the author’s previous work on the microcosm principle with Jacobs and Sokolova, and it extends the bialgebraic studies of SOS originated by Rutten, Turi and Plotkin and further developed by many authors.
勝股審也 (京都大学), On the biadjunction between 2-categories of traced monoidal categories and tortile monoidal categories
Craig Pastro (京都大学), Tambara profunctors and the centre of functor categories (Joint work with Ross Street)
The centre of a monoidal category C was introduced by Joyal and Street and consists of pairs of objects (A,u) where A is an object of C and u: A # - ---> - # A is a natural transformation expressing a form of commutativity. Morphisms in the centre preserve this structure. Functor categories of the form [C,Set], or more generally [C,V] for suitable V, are monoidal via the Day convolution tensor product so it is natural to ask what the centre of this category looks like, and when it is again a functor category. D. Tambara has shown that the centre of [C,Vect] is equivalent to a certain category of endo-profunctors, which we call Tambara profunctors, Tamb(C). Starting with his work, we extend this to arbitrary (suitable) V, and describe a category DA, which we call the double of A, such that we have equivalences between the centre of [A,V], Tamb(A), and [DA,V].
浅田和之 (京都大学), Introduction of arrows with profunctors
立木秀樹 (京都大学), On Finite-time Computability Prserving Conversions
亀山幸義 (筑波大学), Shifting the Stage Starting with Delimited Control
木村大輔 (国立情報学研究所), 古典S4論理に対応する計算体系
戸田貴久 (京都大学), 実射影空間における凸概念とへリー型の定理
CSCAT2006にて”射影空間における凸概念について”という タイトルで講演した内容の続編です。 オリジナルのへリーの定理はR^dの凸集合の組合せ的な性質を表す 基本定理です。実射影空間に定義した凸集合に関して、 これと似た形の定理が成り立つことを証明したいと思っています。
星野直彦 (京都大学), Int construction and biproducts
西澤弘毅 (鳥取環境大学), A new characterization of closed type of multirelation