$B:y0f5.J8(B ($B@iMUBg3X(B), 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.
$BO!Hx0lO:(B ($B5~ETBg3X(B), 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$B!G(Bs 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.
$B>!8T?3Li(B ($B5~ETBg3X(B), On the biadjunction between 2-categories of traced monoidal categories and tortile monoidal categories
Craig Pastro ($B5~ETBg3X(B), 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].
$B@uEDOBG7(B ($B5~ETBg3X(B), Introduction of arrows with profunctors
$BN)LZ=( $B55;39,5A(B ($BC^GHBg3X(B),
Shifting the Stage Starting with Delimited Control $BLZB
$B55;39,5A(B ($BC^GHBg3X(B), Shifting the Stage Starting with Delimited Control
$B8MED5.5W(B ($B5~ETBg3X(B), $B
$B@1LnD>I'(B ($B5~ETBg3X(B), Int construction and biproducts