京都大学数理解析研究所計算機科学研究分野

より非公式な， Logic and Semantics Seminar も並行して行っています．

2012 2012 2011 2010 2009 2008 2007 2006 2005 2004 2003 2002 2001

星野直彦(京都大学数理解析研究所) Step Indexed Realizability Semantics for a Call-by-Value Language Based on Basic Combinatorial Objects 11.00-12.00,21 Jun, 2012 General Research Building 2 (next to the CS room) (map) Abstract

We propose a mathematical framework for step indexed realizability semantics of a call-by-value polymorphic lambda calculus with recursion, existential types and recursive types. Our framework subsumes step indexed realizability semantics by untyped call-by-value lambda calculi as well as categorical abstract machines. Starting from an extension of Hofstra’s basic combinatorial objects, we construct a step indexed categorical realizability semantics. Our main result is soundness and adequacy of our step indexed realizability semantics. As an application, we show that a small step operational semantics captures the big step operational semantics of the call-by-value polymorphic lambda calculus. We also give a safe implementation of the call-by-value polymorphic lambda calculus into a categorical abstract machine.
宮部賢志 (京都大学数理解析研究所) Schnorr triviality is equivalent to being a basis for tt-Schnorr randomness 11.00-12.00, 7 Jun, 2012 General Research Building 2 (next to the CS room) (map) Abstract

ランダムの概念として最も有名なMartin-L\"ofランダムネスは，テスト，複雑性，マルチンゲールなどにより特徴付けられる．一方，ランダムではない（遠い）という概念として，low,trivial,basisなどの概念が存在し，これらが同値になる事が知られている．(Nies 2005, Hirschfeldt et al. 2007)この Schnorrランダムネス版について，適当な相対化を行えば，lowとtrivialは同値になる．(Franklin-Stephan 2010)一方，basisによる(自然な)同値な定義は知られていなかった．本講演では，basisによる特徴付けなど，Schnorr trivialityに関するいくつかの新しい結果を紹介する．
前半30分は日本語で，Martin-L\"ofランダムネスに対する， low,triviality,basisなどの概念を紹介する．後半30分は英語で，Schnorrランダムネスに関する講演者の結果を発表する．後半はCCR2012で発表する予定である．
スライドなどは以下のページからダウンロードできます． http://kenshi.miyabe.name/wordpress/?p=726&lang=ja
Vivek Nigam (Ludwig Maximilian University of Munich) An Extended Framework for Specifying and Reasoning about Proof Systems 14.30 - 15.30,28 May 2012 General Research Building 2 (next to the CS room) (map) Abstract

It has been shown that linear logic can be successfully used as a framework for both specifying proof systems for a number of logics, as well as proving fundamental properties about the specified systems. In this paper, we show how to extend the framework with subexponentials in order to be able to declaratively encode a wider range of proof systems, including a number of non-trivial proof systems such as a multi-conclusion intuitionistic logic, classical modal logic S4, and intuitionistic Lax logic. Moreover, we propose methods for checking whether an encoded proof system has important properties, such as if it admits cut-elimination, the completeness of atomic identity rules, and the invertibility of its inference rules. Finally, we present a tool implementing some of these specification/verification methods.
This is a joint work with Giselle Reis and Elaine Pimentel.
Hugo Herbelin (Laboratoire PPS, CNRS, INRIA & Universite Paris Diderot) Classical call-by-need sequent calculi: The unity of semantic artifacts 16.00 - 17.00,28 May 2012 General Research Building 2 (next to the CS room) (map) Abstract

We systematically derive a classical call-by-need sequent calculus, which does not require an unbounded search for the standard redex, by using the unity of semantic artifacts proposed by Danvy et al. The calculus serves as an intermediate step toward the generation of an environment-based abstract machine. The resulting abstract machine is context-free, so that each step is parametric in all but one component. The context-free machine elegantly leads to an environment-based CPS transformation. This transformation is observationally different from a natural classical extension of the transformation of Okasaki et al., due to duplication of un-evaluated bindings. We further demonstrate the usefulness of a systematic approach by deriving an abstract machine and CPS for an alternative classical call-by-need calculus.
(Joint work with Zena M. Ariola, Paul Downen, Keiko Nakata & Alexis Saurin)
照井一成 (京都大学数理解析研究所) Semantic evaluation, intersection types and complexity of simply typed lambda calculus 11.00 -,17 May 2012 General Research Building 2 (next to the CS room) (map) Abstract

Consider the following problem: given a simply typed lambda term of Boolean type and of order r, does it normalize to “true”? A related problem is: given a term M of word type an d of order r together with a finite automaton D, does D accept the word represented by the normal form of M? We prove that these problems are n-EXPTIME complete for r = 2n + 2, and n-EXPSPACE complete for r = 2n + 3.
While the hardness part is relatively easy, the membership part is not so obvious; in particular, simply applying beta reduction does not work. Some preceding works employ semantic evaluation in the category of sets and functions, but it is not efficient enough for our purpose. We present an algorithm for the above type of problem that is a fine blend of beta reduction, Krivine abstract machine and semantic evaluation in a category based on preorders and order ideals, also known as the Scott model of linear logic. Semantic evaluation in that category can also be presented as intersection type checking.
Chung-chieh Shan (Cornell大学/筑波大学) Functional modularity in the lambda calculus 11.00 -,15 May 2012 General Research Building 2 (next to the CS room) (map) Abstract

A module is a part of a _description_ of a system, not necessarily a physical part. For example, a program that is stored only in compiled form by the computer running it may nevertheless be better described by source code, so the program may have source modules that are hard to recover at run time. This functional notion of modularity is relevant for organisms, species, and scientists because they all need to adapt to changes in the environment without re-learning, re-evolving, or re-discovering each new system from scratch.
Lambda calculi and type systems offer expressive ways to describe natural language and thus carve out its modules. In particular, lambda calculi can express modules that operate on other modules, and type systems can circumscribe information flow among modules whose operation is tightly intertwined. I will illustrate the use of this expressivity with two examples: First, Abstract Categorial Grammars can carve out sound and meaning as a collection of modules mediated by syntax. Second, monad transformers can carve out side effects such as continuations and state as a collection of modules mediated by lexical items.
Paul-Andre Mellies (CNRS, Paris VII) Braided notions of dialogue categories 11.00 -,19 April 2012 General Research Building 2 (next to the CS room) (map) Abstract

A dialogue category is a monoidal category equipped with an exponentiating object. In this talk, I will introduce a notion of braided dialogue category, and explain how this notion provides a functorial bridge between proof theory and knot theory.
Stefano Berardi (University of Torino) A Topology over a set of Knowledge States and a Fixed Point Problem 11.00 -,February 2nd 2012 General Research Building 2 (next to the CS room) (map) Abstract

We give an abstract formulation of the termination problem for realizer of Heyting Arithmetic plus various subsystem of classical logic. This termination problem is expressed as the existence of a fixed point for a class of continuous maps in a suitable topology.
Rune Harder Bak The absolute Galois group - a number theoretic introduction to the Langlands program 11.00 -,Thursday January 19th General Research Building 2 (next to the CS room) (map) Abstract

What is the absolute Galois group? Why do we want to compute it? And how are we doing it? If there is time in the end I will talk about modular forms, and how the help towards the answer to this question. This is intended to serve as a view into the fascinating world of algebraic numbers for the non-specialist. Nor prior exposure to algebraic number theory is required.
Jean-Yves Girard(IML Marseille & RIMS Kyoto) A SECOND LOOK AT PROOF-NETS １月１２日１１：００～総合研究2号館 478号室(CS室のとなりです)(map) Abstract

In logic, we have a reasonable answer to the question :
"What is a typable object?"
but none so far to the question :
"What is a typed object?"
By a second look at proof-nets, especially the ones involving quantifiers, we shall propose an answer to the second question.

2012 2011 2010 2009 2008 2007 2006 2005 2004 2003 2002 2001

宮部賢志 (京都大学数理解析研究所) Kurtzランダムネスの微分定理による特徴付け 11.00 - 12.00, Thursday 17 November 2011 総合研究2号館 478号室(CS室のとなりです)(map) Abstract

Brattka, Miller, Niesらによって、主要なランダムの概念が微分可能性によって特徴づけられることが知られるようになった。その後いくつかの研究がなされ、これまでMartin-L?"of randomness, weak 2-randomness, Schnorr randomness, computable randomness などが同様に微分可能性により特徴づけられることが分かっていた。本発表ではKurtz randomnessの特徴付けについて主に話をする。特に今までと異なる点として、
(1)computable metric space上という非常に一般的な空間で示された
(2)微分定理という微分可能性よりも強い形で示された
(3)証明の方法がintegral testによる特徴付けを経由しており、
randomnessと微分の関係が分かりやすくなっているなどが挙げられる。この証明方法は他のランダムの概念に容易に応用できることが期待される。またこの結果から関数の同値性にランダムネスの概念が現れるという興味深い系が導かれることにも触れる。
Sebastian Fischer (国立情報学研究所) Generate, Test, and Aggregate A Calculational Framework for Systematic Parallel Programming with MapReduce (Joint work with Kento Emoto (Tokyo University) and Zhenjiang Hu (NII Tokyo)) 11.00 - 12.00, Thursday 1 September 2011 総合研究2号館 478号室(map) Abstract

MapReduce, developed by Google, is a popular and successful framework to implement massively parallel algorithms. It can be used to distribute the execution of data intensive tasks, hiding implementation details of parallelization and data distribution. However, it is often difficult to define MapReduce programs because realistic problems do not match its simple divide and conquer form. Although (too!) many case studies are being published that show non-trivial applications of MapReduce, no generalized theory has been developed that captures underlying common ideas. I will present a framework for systematic parallel programming with MapReduce that generalizes existing implementation ideas for parallel algorithms and is applicable to a wide class of search problems. Parallel algorithms can be specified as generate-and-test problems combined with result aggregation and we provide two calculational theorems that allow to implement such specifications efficiently using MapReduce. Our approach brings MapReduce programming, which is inspired by the map and reduce primitives available in many functional languages, back to its roots by providing a calculational framework for program development. It makes expert knowledge available to a broader group of programmers by automatically bridging the gap between intuitive specifications and efficient implementations.
末永幸平 (JSPS Research Fellow (PD), Kyoto University) Programming with Infinitesimals: A WHILE-Language for Hybrid (Joint work with Ichiro Hasuo) 11.00 - 12.00, Thursday 21 July 2011 総合研究2号館 478号室(map) Abstract

We add, to the common combination of a WHILE-language and a Hoare-style program logic, a constant dt that represents an infinitesimal (i.e. infinitely small) value. The outcome is a framework for modeling and verification of hybrid systems: hybrid systems exhibit both continuous and discrete dynamics and getting them right is a pressing challenge.We rigorously define the semantics of programs in the language of nonstandard analysis, on the basis of which the program logic is shown to be sound and relatively complete.
長谷川真人 (京都大学数理解析研究所) もつれたソフトウェアを解きほぐす数学 2011年6月30日 11:00 - 12:00 総合研究2号館 478号室(map) Abstract

コンピュータソフトウェアは現代社会の縁の下の力持ちです。ソフトウェアの力を借りない日はほとんどないと言っても過言ではありません。私はコンピュータなんて触らないよ、という方でも、実は、携帯電話、自動車、家電、などなど、目に見えないところで知らず知らずソフトウェアの恩恵を受けているはずです。もちろん、企業や役所、公共交通機関などでは、より目につくかたちでソフトウェアが活躍しています。
それらのソフトウェアには数百万行に及ぶ巨大なものも珍しくありません。そして、その中のほんの小さな不具合が、社会に致命的な影響を与えたという事例は山のようにあります。入り組んだ巨大なソフトウェアを上手に設計し、解析・検証し、さらに改良するためには、どのようにしたらよいのでしょうか？この講演では、数学を武器にしてソフトウェアに立ち向かう研究の、最近の動向についてご紹介します。特に、ソフトウェアを数学的に正確に捉えることと、現代数学が得意とする抽象化の考え方を用いてソフトウェアの本質に迫ることに重点をおいて、数学がコンピュータソフトウェアの研究開発において果たす役割についてお話ししたいと思います。
星野直彦 (京都大学数理解析研究所) Semantics for higher-order quantum computation via Geometry of Interaction 2011年6月16日 11:50? - 12:40? 総合研究2号館 478号室(map) Abstract

Quantum computation attracts growing attention as a new computing paradigm. While much of its current study employs low-level formalisms such as quantum circuits, several high-level languages/calculi have been recently proposed aiming at structured quantum programming. The current work contributes to the semantical study of such high-level quantum languages, by providing adequate GoI-based semantics of a functional quantum programming language that is based on a linear lambda calculus equipped with recursion.
宮部賢志 (京都大学数理解析研究所) Characterizing randomness by integral tests 2011年6月16日 11:00 - 11:50? 総合研究2号館 478号室(map) Abstract

A randomness notion is usually characterized by tests, complexity and martingales. By recent researches it comes to be known that differentiability characterizes some randomness notions. We need to investigate why this characterization is possible. It is also known that integral tests characterize Martin-L'of randomness. Since the integral tests are tests using the integration, further study on integral tests will help us to study the relation between differentiability and randomness. In this talk we give characterizations of weak-2 randomness, Schnorr randomness and Kurtz randomnessusing the integral tests.
Michele Basaldella (京都大学数理解析研究所) A gentle introduction to ludics11.00 - 12.00, Thursday 21 April 2011総合研究2号館 478号室 (地図) 概要

When one is interested in understanding the duality between syntax (proofs) and semantics (models) in logic, a primary obstacle is that proofs are finite and concrete objects, while models are infinite and abstract structures. Since proofs and models are so different by their nature, they hardly interact together. This lack of interaction between the two worlds prevents a deeper analysis of the relations between syntax and semantics.

Ludics is a research program started by Girard aimed to explain various logical and computational phenomena from an interactive point of view. The universe of ludics consists of designs: partial and infinitary proofs in which the logical type-information has been almost erased. In this vast universe, both proofs and models can be homogeneously represented as designs. Moreover, since designs come from proofs, we can make them interact together via normalization (cut-elimination). This induces an orthogonality relation, based on the termination of the computation of the normal form, which allows to reconstruct the logical types, as bi-orthogonality-closed sets of designs.

In this talk we introduce and discuss the basic concepts of ludics and show some completeness results for proofs.
Yde Venema (Institute for Logic, Language and Computation Universiteit van Amsterdam) Coalgebra automata (towards a universal theory of automata) 11.00 - 12.00, Thursday 17 March 2011総合研究2号館 478号室 (地図) 概要

Automata operating on infinite objects provide an invaluable tool for the spcification and verification of programs. Many of the infinite objects studied in this area, such as words/streams, trees, graphs or transition systems, represent ongoing behaviour in some way, and provide key specimens of coalgebras. Hence it make sense to develop a universal theory of coalgebra automata: automata operating on coalgebras. The motivation underlying the introduction of coalgebra automata is to gain a deeper understanding of this branch of automata theory by studying properties of automata in a uniform manner, parametric in the type of the recognized structures. Coalgebraic automata theory thus contributes to Universal Coalgebra as a mathematical theory of state-based evolving systems.

In the talk we give a quick introduction to coalgebra, and we introduce the notion of a coalgebra automaton. We will see that in fact a large part of the theory of parity automata can be lifted to a coalgebraic level of generality, and thus indeed belongs to the theory of Universal Coalgebra. More specifically, coalgebra automata satisfy various closure properties: under some conditions on the coalgebraic type, the collection of recognizable languages are closed under taking union, intersection, complementation, and existential projections. We will discuss two kinds of coalgebra automata, corresponding to approaches in coalgebraic logic that are based on, respectively, relation lifting and predicate liftings. Our results have many applications in the theory of (coalgebraic fixpoint logics), but these will only be discussed tangentially.
丸山善宏 (Department of Humanistic Informatics, Kyoto Univ.) Natural Duality, Modality and Coalgebra 11.00 - 12.00, Tuesday 8 March 2011総合研究2号館 478号室 (地図) 概要

The theory of natural dualities is a general theory of Stone-type dualities based on the machinery of universal algebra. In this talk, by introducing a new notion of modal power, we extend the theory of natural dualities so that it encompasses Jonsson-Tarski's duality and Kupke-Kurz-Venema's coalgebraic duality for the class of all modal algebras. In a broader context, this work is concerned with a tension between generality and particularity. A preprint with the same title is available in:http://researchmap.jp/ymaruyama/
長谷川立 (東京大学) Combinatorial enumeration model を用いた Church-Rosser 性の証明 111.00 - 12.00, Februrary 24th (Thu)総合研究2号館 478号室 (地図) 概要

Combinatorial enumeration model は, Joyal-Girard による解析関手を用いたラムダ計算のモデルのことであり, ここではそれを線形論理のモデルに改変したものを指している. ある意味で数え上げの個数を与えており, その事実を用いたシンプルな解析を可能にしている。ここでは, linear category 上に構成された計算体系 LC の Church-Rosser 性の証明に, このモデルを応用する技術を紹介する。
西村進 (京都大学数学教室) Calculating Tree Navigation with Symmetric Relational Zipper11.00 - 12.00, Thursday 20 January 2011総合研究2号館 478号室 (地図) 概要

Navigating through tree structures is a core operation in tree processing programs. Most notably, XML processing programs intensively use XPath, the path specification language that locates particular nodes in a given document structure.

In this talk, a calculational method for deriving certain equalities of XPath expressions is presented. Tree navigation operations in XPath expressions, making the symmetries of those operations explicit. By exploiting the symmetry, certain equalities that are useful for optimizing XPath evaluation are derided by simple calculation. The point-free, algebraic reasoning on relations not only leads to a concise justification of some known results but also establishes equations over XPath expressions with negative predicates and those beyond XPath expressibility.

This is joint work with Yuta Ikeda.

2012 2011 2010 2009 2008 2007 2006 2005 2004 2003 2002 2001

末永幸平（リスボン大学）Fractional Ownerships for Safe Memory Deallocation11.00 - 12.00, Thu 2 Dec 2010総合研究2号館 478号室 (地図) 概要

We propose a type system for a programming language with memory allocation/deallocation primitives, which prevents memory-related errors such as double-frees and memory leaks. The main idea is to augment pointer types with fractional ownerships, which express both capabilities and obligations to access or deallocate memory cells. By assigning an ownership to each pointer type constructor (rather than to a variable), our type system can properly reason about list/tree- manipulating programs. Furthermore, thanks to the use of fractions as ownerships, the type system admits a polynomial-time type inference algorithm, which serves as an algorithm for automatic verification of lack of memory-related errors. A prototype verifier has been implemented and tested for C programs.

This is joint work with Naoki Kobayashi.
照井一成 (京都大学数理解析研究所) Church => Scott = Ptime: an application of resource sensitive realizability11.00 - 12.00, Thu 25 Nov 2010総合研究2号館 478号室 (地図) 概要

We introduce a variant of linear logic with second order quantifiers and type fixpoints, both restricted to purely linear formulas. The Church encodings of binary words are typed by a standard non-linear type `Church,' while the Scott encodings (purely linear representations of words) are by a linear type `Scott.'

We then give a characterization of polynomial time functions, which is derived from (Leivant and Marion 93): a function is computable in polynomial time if and only if it can be represented by a term of type Church => Scott.

To prove soundness, we employ a resource sensitive realizability technique developed by Hofmann and Dal Lago.

This is a joint work with Alois Brunel.
石田和 (京都大学数理解析研究所) 非可換線型論理と第二量子化11.00 - 12.00, Thursday 28 Oct 2010総合研究2号館 478号室 (地図) 概要

本講演では、一般の線型論理のモデルを少し弱めた非可換なlinear category に関する基本的な結果を紹介します。線型論理におけるlinear exponentialが、ボソン的な空間の表現に利用されるという所見は、例えば『Fock space: a model of linear exponential types RF Blute, P Panangaden, RAG Seely - MSCS, 1994』などに見ることができます。またOxfordのJamie Vicaryさんによる、dagger categoryの言葉を用いたFock spaceの公理化(Fock adjunction)があります。非可換線型論理の応用例としてFock adjuntionの、dagger categoryの言葉を用いない、再定式化についてお話しします。
蓮尾一郎 (京都大学数理解析研究所) Generic Forward and Backward Simulations II: Probabilistic Simulation11.00 - 12.00, Thursday 26 Aug 2010総合研究2号館 478号室 (地図) 概要

Jonsson and Larsen’s notion of probabilistic simulation is studied from a coalgebraic perspective. The notion is compared with two generic coalgebraic definitions of simulation: Hughes and Jacobs’ one, and the one introduced previously by the author. We show that the first almost coincides with the second, and that the second is a special case of the last.We investigate implications of this characterization; notably the Jonsson-Larsen simulation is shown to be sound, i.e. its existence implies trace inclusion.

This is work to be presented at CONCUR 2010.
勝股審也 (京都大学数理解析研究所) Categorical Descriptional Composition11.00 - 12.00, Thursday 29 July 2010総合研究2号館 478号室 (地図) 概要

The descriptional composition is a method to fuse two term transformation algorithms described by attribute couplings (AC, attribute grammars over terms) into one. In this talk, we provide a general categorical framework for the descriptional composition based on traced symmetric monoidal categories and the Int construction by Joyal et al. We demonstrate that this framework can handle the descriptional composition of SSUR-ACs, nondeterminisitic SSUR-ACs, quasi-SSUR ACs and stack ACs.
長谷川真人 (京都大学数理解析研究所) Small-step and big-step semantics for call-by-need (joint work with Keiko Nakata)11.00 - 12.00, Thursday 15 July 2010総合研究2号館 478号室 (地図) 概要

We present natural semantics for acyclic as well as cyclic call-by-need lambda calculi, which are proved equivalent to the reduction semantics given by Ariola and Felleisen. The natural semantics are big-step and use global heaps, where evaluation is suspended and memorized. The reduction semantics are small-step, and evaluation is suspended and memorized locally in let-bindings. Thus two styles of formalization describe the call-by-need strategy from different angles.

The natural semantics for the acyclic calculus is revised from the previous presentation by Maraist et al., and its adequacy is ascribed to its correspondence with the reduction semantics, which has been proved equivalent to call-by-name by Ariola and Felleisen. The natural semantics for the cyclic calculus is inspired by that of Launchbury and Sestoft, and we state its adequacy using a denotational semantics in the style of Launchbury; adequacy of the reduction semantics for the cyclic calculus is in turn ascribed to its correspondence with the natural semantics.

Reference: Keiko Nakata and Masahito Hasegawa, Small-step and big-step semantics for call-by-need. Journal of Functional Programming (2009), 19(6): 699--722.
星野直彦 (京都大学数理解析研究所) A modification of GoI interpretation for DILL11.00 - 12.00, Thursday 24 June 2010総合研究2号館 478号室 (地図) 概要
Girard's Geometry of Interaction (GoI) provides a degenerated "model" of the linear logic:
- tensor =~ par
- ! =~ !!
The second degeneracy disturbs adequacy for the intuitionistic linear lambda calculus. We modify the standard interpretation of ! and show adequacy of the interpretation for DILL.
浦本武雄 (京都大学数学教室) ++-construction and filtration11.00 - 12.00, Thursday 17 June 2010総合研究2号館 478号室 (地図) 概要

In topos theory, ++-construction is a method of completion of presheaves and induces the best approximate sheaf. In this talk, we simulate the ++-completion in more general situations, and pursue possibilities of examples and applications in several contexts.
宮部賢志 (京都大学数理解析研究所) 一般位相空間上のランダムネス11.00 - 12.00, Thursday 10 June 2010総合研究2号館 478号室 (地図) 概要

Algorithmic randomness is well studied over a Cantor space, whose base is computability theory on natural numbers. Computability theories over real numbers, a metric space and a topological space also have been developed. So algorithmic randomness over such spaces can be considered. There are three approaches to define randomness, that is, by test, by complexity and by martingales. Randomness by tests on a computable topological space was defined by Hertling and Weihrauch 1998. Randomness by complexity on a compact computable metric space was by G\'acs 2005 and randomness by complexity on a computable metric space was by Hoyrup and Rojas 2009. In this talk we define randomness by martingales and by complexity on a computable topological space and investigate the relations among three definitions. In the end we prove van Lambalgen's theorem under two natural conditions. So these randomness can be said to be natural under these conditions.
長谷川真人 (京都大学数理解析研究所) Traced monoidal categories and semantics of programming languages10.00 - 10.45, Thursday 3 June 2010総合研究2号館 478号室 (地図) 概要

An introduction to the applications of traced monoidal categories in computer science, with particular emphasis on the relation to semantics of recursive programs. This talk is intended for those new to this topic (and will likely be given in Japanese).
長谷川真人 (京都大学数理解析研究所) A quantum double construction in Rel11.00 - 12.00, Thursday 3 June 2010総合研究2号館 478号室 (地図) 概要

In last 15 years, many interesting traced monoidal categories were discovered in the study of semantics of logic and computation, including domain theory, term graphs, geometry of interaction, game semantics and models of linear logic. However, these examples in computer science are quite different from the leading examples in mathematics, namely the ribbon categories arising from quantum groups, many of which feature non-symmetric braidings while most CS examples are just symmetric. As an initial attempt to fill this gap between CS and Math, in this talk I will demonstrate that some key ideas from quantum group theory can be directly applied to a category frequently used in the study of semantics. Specifically, for any group G, I will derive a ribbon Hopf algebra in the category Rel of sets and binary relations using the quantum double construction of Drinfel'd. The category of modules of this Hopf algebra turns out to be isomorphic to a braided ribbon category of crossed G-sets.
Pierre-Marié Pedrot (ENS Lyon & RIMS, Kyoto Univ.) Yet another effect-manipulating language11.00 - 12.00, Thursday 27 May 2010総合研究2号館 478号室 (地図) 概要

It has been experimentally witnessed that some monads where particularly well-behaved whenever they respected some form of linearity. Two particularly famous monads do so: the linearly-used continuation monad and the linearly-used state monad. Møgelberg and Simpson presented a language, the Extended Effect Calculus, that naturally dealt with those two monads through the use of a DILL-like type system. EEC was in turn designed as a close relative to Levy's call-by-push-value. In this talk, we present a refinement of EEC restricted to pseudo-multiplicative linear connectors that emphasizes dualities, and at the same time underlines the CBPV-inherited absence of choice relatively to the CBV-CBN feud. We will then present its categorical model and relate it to other famous effect models.
蓮尾一郎 (京都大学数理解析研究所) Crash Introduction to Coalgebra (A primer to the subsequent talk)10.00 - 11.00, Thursday 20 May 2010総合研究2号館 478号室 (地図) 概要

The very basics of coalgebraic modeling in computer science are covered as a primer to my subsequent talk.
蓮尾一郎 (京都大学数理解析研究所) Coalgebraic Representation Theory of Fractals (Act 2)11.00 - 12.00, Thursday 20 May 2010総合研究2号館 478号室 (地図) 概要

We develop a representation theory in which a point of a fractal specified by metric means (by a variant of an iterated function system, IFS) is represented by a suitable equivalence class of infinite streams of symbols. The framework is categorical: symbolic representatives carry a final coalgebra; an IFS-like metric specification of a fractal is an algebra for the same functor. Relating the two there canonically arises a representation map, much like in America and Rutten's use of metric enrichment in denotational semantics. A distinctive feature of our framework is that the canonical representation map is bijective. In the technical development, gluing of shapes in a fractal specification is a major challenge. On the metric side we introduce the notion of injective IFS to be used in place of conventional IFSs. On the symbolic side we employ Leinster's presheaf framework that uniformly addresses necessary identification of streams--such as .0111...= .1000... in the binary expansion of real numbers. Our leading example is the unit interval I = [0,1].

This is a joint work with Bart Jacobs (Nijmegen) and Milad Niqui (CWI, Amsterdam), presented at MFPS 2010.
Alexis Saurin (PPS, Univ. Paris 7)A hierarchy for delimited control in call-by-name 11.00 - 12.00, Tuesday 26 April 2010総合研究2号館 478号室 (地図) 概要

It has been noticed in recent years that Lambda-mu-calculus, contrarily to Parigot's original formulation of lambda-mu-calculus, corresponds to delimited control in call-by-name. While considering delimiters, it arose very naturally in Danvy and Filisnki's work that those delimiters could be organized as a hierarchy, the CPS hierarchy. I shall present a natural extension of Lambda-mu to a family of calculi, the Stream hierarchy, which is a CBN correspondent of the CPS hierarchy. This talk will hopefully shed some new light on relations between classical lambda-calculi and delimited control.
Bart Jacobs (Radboud Univ. Nijmegen)Scalars, monads and categories 10.30 - 11.15, Thursday 11 March 2010理学部3号館 305号室 (地図) 概要

Interrelatedness will be described between: (1) algebraic structure on sets of scalars, (2) properties of monads associated with such sets of scalars, and (3) structure in categories (esp. Lawvere theories) associated with these monads. These interrelations will be expressed in terms of ``triangles of adjunctions'', involving for instance various kinds of monoids (non-commutative, commutative, involutive) and semirings as scalars. It will be shown to which kind of monads and categories these algebraic structures correspond via adjunctions.

A link to the underlying paper will soon be available via http://www.cs.ru.nl/~bart/PAPERS/index.html
Bart Jacobs (Radboud Univ. Nijmegen)Basics of involutive categories and monoids 11.15 - 12.00, Thursday 11 March 2010理学部3号館 305号室 (地図) 概要

The notion of involutive monoid will be described abstractly using the "microcosm principle" of Hasuo et al: an involution on an outer category is used internally to define the notion of involutive monoid. This extends the idea that an outer monoidal category is needed to define internally what a monoid is. Some basic results about involutions on categories of Eilenberg-Moore algebras are presented, with conjugation on categories of modules/vector spaces as main example. It will be shown how the essence of the so-called Gelfand-Naimark-Segal (GNS) construction can be described using involutive categories.
中田景子 (Institute of Cybernetics, Tallinn University of Technology) A Hoare logic for the trace-based coinductive semantics of While 11.00 - 12.00, Monday 8 March 2010理学部3号館 305号室 (地図) 概要

In search for a foundational framework for reasoning about observable behavior of programs that may not terminate, we have previously studied a trace-based big-step semantics for the While language. In this semantics, both traces and evaluation (relating initial states of program runs to traces they produce) are defined coinductively. On terminating runs, it agrees with the standard inductive state-based semantics. Recently we devised a Hoare logic counterpart of our coinductive trace-based semantics and prove it sound and complete. Our logic subsumes both the partial correctness Hoare logic and the total correctness Hoare logic: they are embeddable. Since we work with a constructive underlying logic, the range of expressible program properties has a rich structure; in particular, we can distinguish between termination and nondivergence, e.g., unbounded total search fails to be terminating but is nonetheless nondivergent. Our metatheory is entirely constructive as well, and we have formalized it in Coq.

In this talk, I will present the big-step semantics and the Hoare logic, and demonstrate the expressivity of our logic by an example of unbounded total search inspired by Markov's principle.
Ross Duncan (Oxford University Computing Laboratory) Quantum Logic, Quantum Computation and the Proof Theory of Compact Categories 10.30 - 12.30, Friday 12 February 2010理学部3号館 305号室 (地図) 概要

Quantum computation has reawakened interest in the underlying logic of quantum mechanics. We briefly examine the "old school" Birkhoff-von Neumann style quantum logic, and discuss why it is not a suitable basis for quantum computation. We then discuss a newer approach, initiated by Abramsky and Coecke and based on a view of logic informed by the Curry-Howard correspondence between proofs and programs. Abstract: Just as conventional functional programs may be understood as proofs in an intuitionistic logic, so quantum processes can also be viewed as proofs in a suitable logic. We describe such a logic, the logic of compact closed categories and biproducts, presented both as a sequent calculus and as a system of proof-nets. This logic captures much of the necessary structure needed to represent quantum processes under classical control, while remaining agnostic to the fine details. We demonstrate how to represent quantum processes as proof-nets, and show that the dynamic behaviour of a quantum process is captured by the cut-elimination procedure for the logic. We show that the cut elimination procedure is strongly normalising: that is, that every legal way of simplifying a proof-net leads to the same, unique, normal form. Finally, taking some initial set of operations as non-logical axioms, we show that that the resulting category of proof-nets is a representation of the free compact closed category with biproducts generated by those operations.

The main part of this talk is based on book chapter http://arxiv.org/abs/0903.5154.
Ross Duncan (Oxford University Computing Laboratory) Complementarity in Categorical Quantum Mechanics 14.45 - 16.45, Friday 12 February 2010理学部3号館 305号室 (地図) 概要

The fundamental feature of quantum mechanics is the existence of incompatible observables. This is usually phrased in a negative way: operators are NOT commuting; the lattice of observables is NON-distributive etc. In this talk I will present the positive content to be found in the existence of complementary quantum observables. We will see that each such pair gives rise to an incredibly rich zoo of algebraic structures all of which can be presented graphically. The resulting graphical language is expressive enough to denote any quantum physical state of an arbitrary number of qubits, and any processes thereof. The rules for manipulating these result in very concise and straightforward computations with elementary quantum gates, translations between distinct quantum computational models, and simulations of quantum algorithms such as the quantum Fourier transform. They enable the description of the interaction between classical and quantum data in quantum informatic protocols. I will describe this formalism in detail, and if time permits explain some applications in the study of measurement based quantum computation and the local hidden variable models.

The main part of this talk can be found in http://arxiv.org/abs/0906.4725.

2012 2011 2010 2009 2008 2007 2006 2005 2004 2003 2002 2001

Irek Ulidowski (University of Leicester) Reverse Bisimulations on Stable Event Structures 11.00 - 12.00, Thursday 10 December 2009理学部6号館 203P号室 (地図) 概要

The relationships between various equivalences on stable event structures, including interleaving bisimulation (IB), step bisimulation (SB) and hereditary history-preserving (HH) bisimulation, have been investigated by van Glabbeek and Goltz. Since HH bisimulation may be characterised by the use of reverse as well as forward transitions, it is of interest to investigate forms of IB and SB (and other more complex bisimulations) where both forward and reverse transitions are allowed.

Bednarczyk asked whether SB with reverse steps (which we shall call reverse SB and write RSB) is as strong as HH bisimulation. This question remained open until very recently. We give various characterisations of RSB, showing that forward steps do not add extra power. We strengthen Bednarczyk's result that, in the absence of auto-concurrency, reverse IB is as strong as HH bisimulation, by showing that we need only exclude auto-concurrent events at the same depth in the configuration. Finally, we present a lattice of many forms of bisimulations where both forward and reverse observations are allowed. The lattice has HH at the top and IB at the bottom, and we briefly explain the relationships between other forms of bisimulations.
Etienne Duchesne (RIMS, Kyoto University) Geometry of interaction and denotational semantics 11.00 - 12.00, Thursday 19 November 2009理学部6号館 203P号室 (地図) 概要

We study the GoI for classical linear logic defined by Girard in "GoI III" and in particular which invariant of reduction it computes. To do so we introduce the relational semantics of finite families (RelLoc). It is a non-extensional semantics of which experiments are closely related to the indexed linear logic of Bucciarelli and Ehrhard. Next we give a definition of GoI in the framework of partial permutations. It is then possible to make GoI "act" on points of RelLoc and this action enables to compute points of the RelLoc interpertation.
Claudia Faggian (PPS, Paris 7) Partial orders, event structures, and linear strategies (Joint work with Mauro Piccolo)11.00 - 12.00, Thursday 12 November 2009理学部6号館 203P号室 (地図) 概要

We study and generalize ideas introduced by Girard in the setting of Ludics, in particular linear composition. We introduce a game-semantical model where strategies are partial orders, and composition is merging of orders. In this setting, the composition of Ludics results as a special case, while definitions and proofs are simpler. Moreover, several extensions, such as a parallel version, fit nicely.

On this basis, to bridge between Game Semantics and Concurrency, we explore the relation between Event Structures and Linear Strategies. The former are a true concurrency model introduced by Nielsen, Plotkin, Winskel, the latter a family of linear innocent strategies developed starting from Girard's work.

We will also discuss the close correspondence between Ludics and the Linear Pi-calculus [Honda Yoshida Berger].
蓮尾一郎 (京都大学数理解析研究所) Coalgebraic Representation Theory of Fractals11.00 - 12.00, Thursday 1 October 2009理学部6号館 203P号室 (地図) 概要

We establish a canonical bijective correspondence between a ``metric'' fractal induced by an IFS-like specification and a ``coalgebraic'' fractal induced by a combinatorial specification. This is a representation of the former by the latter: the latter consists of (equivalence classes of) infinite streams hence is of symbolic nature. Gluing of shapes calls for careful mathematical treatment: for coalgebraic fractals we employ the presheaf framework by Leinster; for metric fractals we introduce the notion of injective IFS as means of specifying metric fractals. Our leading example is the unit interval [0,1] and its representation by binary streams.

This is a joint work with Bart Jacobs (Nijmegen) and Milad Niqui (CWI, Amsterdam).
西村進 (京都大学数学教室) Refining Exceptions in Four-Valued Logic11.00 - 12.00, Thursday 9 July 2009CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; see direction ) 概要

We discuss refinement of programs featuring exception mechanisms and develop a refinement framework based on Arieli and Avron's four-valued logic. We show that exception features, and other standard programming features as well, are naturally expressed by a class of four-valued predicate transformers. The resulting framework enjoys several refinement laws that are useful for stepwise refinement of programs involving exception handling and partial predicates. We show a few examples of transformation of programs, by which we demonstrate some typical usages of the refinement laws in the proposed framework.
Chris Heunen (Radboud Univ. Nijmegen) An embedding theorem for Hilbert categories11.00 - 12.00, Tuesday 16 June 2009CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; see direction ) 概要

We axiomatically define Hilbert categories. The axioms resemble those for monoidal Abelian categories with the addition of an involutive functor, so that a Hilbert category is a model for reversible (quantum) computation. We then prove that a Hilbert category embeds into the category of Hilbert spaces, preserving adjoint morphisms, preserving all finite (co)limits, and weakly preserving tensor products. An intermediate result that is important in its own right is that the scalars in such a category necessarily form an involutive field.
Bartek Klin (Cambridge Univ. & Warsaw Univ.) SOS for weighted transition systems11.00 - 12.00, Tuesday 9 June 2009CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; see direction ) 概要

Weighted transition systems (WTSs) generalize ordinary labeled transition systems in that transitions are equipped with weights, taken from a commutative monoid. Examples of WTSs include labeled, probabilistic, stochastic, cost-labeled and other kinds of systems.

WTSs can be uniformly understood as coalgebras for functors of a certain shape. Using bialgebraic techniques, I will present a syntactic format of Stuctural Operational Semantics for well-behaved inductive definition of WTSs. The format generalizes previously known formats defined for specific kinds of systems.
Chris Heunen (Radboud Univ. Nijmegen) A (topo)logical structure for state spaces10.00 - 11.00, Tuesday 9 June 2009CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; see direction ) 概要

Topology can be generalised in at least two directions: pointless topology, leading ultimately to topos theory, or noncommutative geometry. The former has the advantage that it also carries a logical structure, the latter captures quantum settings, of which the logic is not well understood generally. We discuss a construction making a generalised space in the latter sense into a generalised space in the former sense, i.e. making a noncommutative C*-algebra into a locale. This construction has the flavour of microcosm techniques.
Rasmus Møgelberg (IT Univ. Copenhagen)A nominal relational model for local state11.00 - 12.00, Thursday 4 June 2009CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; see direction ) 概要

Nominal sets are a tool for modelling theories with names and binders. Work by Pitts and Shinwell, and further developments by Benton and Leperchey have shown how local state can be modelled in nominal sets using a cps style interpretation. The use of nominal sets provides a more elementary and simpler model than the traditional presheaf models for local state in which a type is interpreted as a family of sets indexed by shapes of state. In the nominal sets model, a type is simply a set (with a group action).

In this paper we present a relational model construction for local state in nominal sets capturing relational reasoning principles useful for showing equivalence of programs. Such reasoning principles have hitherto been modelled using families of relations indexed by relations on state. By replacing the families of relations with relations in the usual sense, this model provides a simplification over the previous models similar to that provided by the nominal sets models over the presheaf models for local state.
Michele Basaldella (RIMS, Kyoto Univ.)On the meaning of logical completeness11.00 - 12.00, Thursday 28 May 2009CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; see direction ) 概要

Goedel’s completeness theorem is concerned with provability, while Girard’s theorem in ludics (as well as full completeness theorems in game semantics) is concerned with proofs. Our purpose is to look for a connection between these two disciplines. Following a previous work (B-.Faggian) we consider an extension of the original ludics with contraction and universal nondeterminism, which play dual roles, in order to capture a polarized fragment of linear logic and thus a constructive variant of classical propositional logic. We then prove a completeness theorem for proofs in this extended setting: for any behaviour (formula) A and any design (proof attempt) P, either P is a proof of A or there is a model M in the orthogonal of A which beats P. Compared with proofs of full completeness in game semantics, ours exhibits a striking similarity with proofs of Goedel’s completeness, in that it explicitly constructs a countermodel essentially using Koenig’s lemma, proceeds by induction on formulas, and implies an analogue of Loewenheim-Skolem theorem.
春名太一（神戸大学大学院理学研究科 & JST さきがけ）システム生物学研究におけるカテゴリー論の使い方11.00 - 12.00, Thursday 21 May 2009CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; see direction ) 概要
カテゴリー論を用いた考察を通じて、
1. ネットワークの新しい解析方法、
2. ネットワークモチーフに関する新しい仮説、
を議論する。有向グラフとして表現されるネットワークは構造のない頂点とその間の矢印からなるため、頂点の機能はそのままでは議論できない。しかし、現実のネットワークでは頂点には機能がある。例えば、遺伝子転写制御のネットワークやニューロンのネットワークなどでは、頂点においては情報処理が行われていると考えられる。情報処理のような頂点における機能を含めた形の表現を考えることができれば、現実のネットワークのより深い理解が得られる可能性がある。ここでは簡単に、頂点における機能も有向グラフで表現する。その際、元のネットワークの矢印に対応した有向グラフも用意する。これは頂点の機能間の関係の仕方を表現する。これらに対してカテゴリー論におけるdistributorを使うと様々な構成ができる。例えば、与えられたネットワークを機能のネットワークへと対応させる変換は、有向グラフの圏からそれ自身への函手となり、右随伴を持つ。この函手を用いた現実のネットワークのデータ解析、及びそれに基づくbi-fanと呼ばれるネットワークモチーフに関する新しい仮説について述べる。
Aloïs Brunel (ENS Lyon)An introduction to Classical Realizability11.00 - 12.00, Thu 14 May 2009CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; see direction ) 概要

Different ways of extending the Curry-Howard correspondence to Classical Logic have been intensively studied since the 90's and Griffin's discovery, giving rise to several systems such as lambda-mu-calculus. We will here expose lambda_c-calcul and Classical Realizability (or Krivine Realizability), a powerful tool used to extend the Curry-Howard correspondence to Classical Logic, but also to Set Theory (+ Full Choice Axiom) or Calculus of Construction (classical CoC with universes).

After a presentation of the basics, we will see how this technique is used to extend the Curry-Howard correspondence to Classical Analysis. We will then briefly browse some various applications of the Classical Realizability, such as automated program extraction in the Proof Assistant Coq, safe network protocol specification, model theory and links with Cohen's forcing.
Kazushige Terui (RIMS, Kyoto U.)Expanding the realm of systematic proof theory11.00 - 12.00, Thu 7 May 2009CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; see direction ) 概要
I will report on a joint work with Agata Ciabattoni (TU Wien) and Lutz Strassburger (LIX). In my previous work with Agata and Nick Galatos, we launched a general project of algebraic proof theory for substructural logics, whose main purposes are
- to classify nonclassical axioms into a hierarchy
- to algebraize proof theoretic techniques such as cut elimination and interpolation (they are "algebraic completions")
- to identify a boundary in the hierarchy, below which proof theory works well and above which one finds negative results given by algebraic considerations.
In this talk, we will discuss in our setting a curious boundary case, that is abelian logic of Meyer and Slaney. It is a logic for compact closed categories with binary products and coproducts (but not with initial and terminal objects). It also underlies Lukaciewicz's many valued logic. With this example, we illustrate how our theory works as a heuristic principle for finding a cut-free (hyper)sequent calculus for a given axiomatic system.

Though the current work only takes care of provability (not of proofs), we strongly hope that it will extend to a categorical setting in future, in particular as a useful tool for solving coherence problems for monoidal closed categories. Your suggestions will be welcome.
Bart Jacobs (Radboud Univ. Nijmegen)Coalgebraic and Monoidal Traces11.00 - 12.00, Thu 9 Apr 2009CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; see direction ) 概要

It will be shown how coalgebraic traces, in suitable Kleisli categories, give rise to traced monoidal structure in those Kleisli categories, with finite coproducts as monoidal structure. By applying the standard ``Int'' construction one obtains compact closed categories for ``bidirectional monadic computation''. This generic construction uses partially additive structure in suitably ordered Kleisli homsets. It combines several lines of work in the semantics of computation.
Bart Jacobs (Radboud Univ. Nijmegen)Quantum Logic in Dagger Kernel Categories11.00 - 12.00, Fri 3 Apr 2009CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; see direction ) 概要

This paper investigates quantum logic from the perspective of categorical logic, and starts from minimal assumptions, namely the existence of involutions/daggers and kernels. The resulting structures turn out to (1) encompass many examples of interest, such as categories of relations, partial injections, Hilbert spaces (also modulo phase), and Boolean algebras, and (2) have interesting categorical/logical properties, in terms of kernel fibrations, such as existence of pullbacks, factorisation, and orthomodularity. For instance, the Sasaki hook and and-then connectives are obtained, as adjoints, via the existential-pullback adjunction between fibres.

Reference: Quantum Logic in Dagger Kernel Categories, by Chris Heunen and Bart Jacobs. [arXiv]
Jun Pang (Univ. Luxembourg)Measuring Voter-controlled Privacy16.00 - 17.00, Fri 13 Mar 2009Room 202, RIMS, Kyoto University 概要

In voting, the notion of receipt-freeness has been proposed to express that a voter cannot gain any information to prove that she has voted in a certain way. Receipt-freeness aims to prevent vote buying, even when a voter chooses to renounce her privacy.

In this paper, we distinguish various ways that a voter can communicate with the intruder to reduce her privacy and classify them according to their ability to reduce the privacy of a voter. We develop a formal framework combining knowledge reasoning and trace equivalences to formally model voting protocols and define vote privacy for the voters. Our framework is quantitative, in the sense that it defines a measure for the privacy of a voter. Therefore, the framework can precisely measure the level of privacy for a voter for each of the identified privacy classes. The quantification allows our framework to capture receipts that reduce, but not nullify, the privacy of the voter. This has not been identified and dealt with by other formal approaches.
Paul-André Melliès (Univ. Paris VII)Game Semantics in String Diagrams11.00 - 12.00, Thu 15 Jan 2009CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; see direction ) 概要

2012 2011 2010 2009 2008 2007 2006 2005 2004 2003 2002 2001

Ana Sokolova (Univ. Salzburg)Expressivity of modal logics for probabilistic systems11.00 - 12.00, Thu 4 Dec 2008CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; see direction ) 概要

In this talk I will report on a joint work with Bart Jacobs on examples of expressivity of modal logics. We investigate expressivity of modal logics for transition systems, multitransition systems, Markov chains, and Markov processes, as coalgebras of the powerset, finitely supported multiset, finitely supported distribution, and measure functor, respectively. Expressivity means that logically indistinguishable states, satisfying the same formulas, are behaviourally indistinguishable too. The investigation is based on the framework of dual adjunctions between spaces and logics and focuses on a crucial injectivity property. The approach is generic both in the choice of systems and modalities, and in the choice of a ``base logic''. Most of these expressivity results are already known, but the applicability of the uniform setting of dual adjunctions to these particular examples is what constitutes the contribution of this work.
Daisuke Kimura (National Inst. Informatics)Computational duality and Logical duality11.00 - 12.00, Thu 27 Nov 2008CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; see direction ) 概要

Computational duality between call-by-value and call-by-name is closely related to logical duality of classical logic that is known as de Morgan duality. Selinger gave a categorical semantics of the lambda-mu-calculus, and explained this relationship by using the category-theoretic duality. Wadler introduced the dual calculus that corresponds to classical sequent calcul us, and explained it in a purely syntactical way. However, their result was based on equational theories. Wadler left an open question whether one can obtain similar results by replacing the equations of his work with reductions. This talk presents the best possible answer to his question.

We first refine the lambda-mu-calculus as reduction systems by reformulating sum types and omitting problematic reduction rules that are not simulated by Cut-elimination procedures. Secondly, we give reduction preserving translatio ns between the call-by-name lambda-mu-calculus and dual-calculus. We show that the compositions of these translations become identity maps up to the call-by-name reductions. We also give translations for the call-by-val ue systems, and show that they satisfy properties similar to the call-by-name case. Thirdly, we introduce translations between the call-by-value and call-by-name lambda-mu-calculi by composing the above translations with duality on the dual c alculus. We finally obtain results corresponding to Wadler's, but our results are based o n reductions.
Ana Sokolova (Univ. Salzburg)Classification of Probabilistic Systems16.00 - 17.00, Wednesday 19 Nov 2008Room 202, RIMS, Kyoto University 概要

Probabilistic models for verification of systems with quantitative behaviour have been extensively studied in the area of formal methods in the last couple of decades. Still, there has not been a clear classification of the various models in a single framework for a long time. In this work I will report on an expressiveness hierarchy of probabilistic models which is carried out in the unifying theory of coalgebras.

Most of the existing (discrete) probabilistic (automata based) models can be modelled as coalgebras in the category Sets. A simple though elegant generic observation on the colagebraic level allows us to compare the expressiveness of the different probabilistic models.

Having presented the classification of discrete probabilistic models, we will shed some light on a non-discrete model, that has also been studied in the literature. We will see this model as colagebras in Meas (the category of measure spaces) and show that it is at least as expressive as the corresponding discrete model, using the same expressiveness criterion as before. As future work, using this observation we would like to build a new-dimension level in the hierarchy of probabilistic models.
末永幸平（東北大学大学院情報科学研究科）割り込み入り並行計算のための型を用いたデッドロック解析13.00 - 14.00, Monday 27 Oct 2008Room 202, RIMS, Kyoto University 概要

信頼性の高い並行プログラムの記述は、デッドロックや競合状態の可能性のために、逐次プログラムの記述よりも難しい。また、スレッドが非決定的に並行実行されることにより起こる状態爆発により、プログラムの状態を追跡することが難しいことも、高信頼な並行プログラムの記述の難しさの原因となっている。

このような問題に対処するための有望な手法の一つに、静的検証が挙げられる。これは、プログラムを実行する前に、そのプログラムを正しさが数学的に証明された方法で検証するという手法である。しかしながら、これまでに逐次プログラムの静的検証手法は多く研究されているものの、並行プログラムに対する静的検証手法の研究は、割り込みなどの、現実のソフトウェアによく現れる特徴が扱われていないという点で、未だ発展途上の段階である。テスト実行によるデバッグ手法は、並行プログラムに対しては逐次プログラムの場合よりも有効性が低いため、これらの特徴を扱うことのできる静的検証手法の研究は非常に重要である。

そのような現実的な並行プログラムを扱うことのできる静的検証手法の構築への第一歩として、本講演ではデッドロックの型システムに基づく検証手法を提案する。提案するデッドロック検証手法では、(1) 入れ子構造をとらないロックプリミティブ (2) 破壊的代入が可能なロックへの参照 (3) 割り込みという三つの特徴を備えたプログラムを扱うことができる。これらの特徴は、現実のプログラムではよく用いられるにもかかわらず、既存のデッドロック解析では扱われてこなかった。

我々は、これらの特徴を備えた計算体系を構築し、その計算体系で記述されたプログラムのための型システムを提案する。我々の型システムは、プログラムがデッドロックに陥らないことを保証するために (1) ロック/アンロック操作の間に循環した依存性がないことと (2) 獲得されたロックがちょうど一度解放されること、の二つの性質を検証する。一つ目の性質を検証するために、型システムは各ロック型にはロックレベルと呼ばれる自然数を割り振り、プログラムがロックをロックレベルの昇順に獲得することを保証する。二つ目の性質の検証においては、エイリアシングやロックへの参照への競合状態といった問題に対応するために、{\em 権利と義務}という線形型に基づく概念と、{\em 所有権}という参照へのアクセスをコントロールするための概念を導入する。また、この型システムに基づいた手法により、ネットワークプロトコルの実装の一部に対して検証を行った予備実験の結果を報告する。
Michele Basaldella (RIMS, Kyoto Univ.)Ludics with repetitions: exponentials, interactive types and completeness (Joint work with Claudia Faggian, PPS, CNRS-Paris 7)11.00 - 12.00, Thursday 23 Oct 2008CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; see direction ) 概要

Ludics is a research program introduced by Girard with the aim of providing a foundation for logic based on interaction. It can be seen as a form of Game Semantics whose approach is completely interactive: strategies are untyped (given on a universal arena) and they can only interact with each other (by composing them). An interactive type is a set of strategies which reacts in the same way to a set of tests (which are strategies themselves).

The semantical types which are interpretation of logical formulas enjoy a closure property, called internal completeness, which is essential to prove full completeness.

In this talk, we first give a basic introduction to Ludics: we introduce multiplicative strategies, we define the concepts of interactive types and internal completeness and we sketch how to prove full completeness (with respect to Multiplicative Linear Logic with Synthetic connectives MLLS).

Second, we extend the concept of strategies: we introduce Linear Logic exponentials in Ludics by allowing repetition of actions. We show that in order to interpret exponentials, we need to extend the universe of strategies by introducing non-uniform strategies: non-uniformity is essential to build exponential (semantical) types interactively. We also discuss internal completeness for exponential types and we show that our extension of Ludics is a fully complete model for Multiplicative Exponential Linear Logic with Synthetic connectives MELLS.
Patrick Baillot (ENS Lyon)Light Logics, Optimal Lambda Calculus Reduction and Implicit Computational Complexity11.00 - 12.00h, Thursday 16 Oct 2008Room 102, RIMS, Kyoto University 概要

Light logics are variants of linear logic that can be used as type systems for lambda calculus ensuring certain complexity bounds: e.g. programs typed in the system LAL can be executed in polynomial time (PTIME). Optimal reduction is a graph-rewriting method to evaluate "economically" lambda terms, that is to say without any duplication of redex. We join these two lines of work by showing that optimal reduction provides an efficient -- and simple ! -- way to evaluate LAL-typable lambda terms. For that we show that an algorithm for optimal reduction, Lamping's abstract algorithm, can be run on these terms in PTIME. (Joint work with Paolo Coppola (Udine) and Ugo Dal Lago (Bologna)).
南出靖彦（筑波大学）証明支援系の基礎京都大学数理解析研究所 102号室概要
高階論理に基づく証明支援系について、基礎となる理論といくつかのシステムについて解説する。近年、Isabelle/HOL ,Coqなどの高階論理に基づく証明支援系（対話的定理証明系）が、ハードウェア/ソフトウェアの検証、プログラミング言語理論の定式化、数学の定理の証明などの様々な分野で応用されるようになってきている。
講義の前半では、証明支援系の理解に必要となるラムダ計算、高階単一化、高階論理などについて概説する。講義の後半では、具体的な証明支援系としてIsabelle/HOLを取り上げ、理論との関係及び具体的な使用法について解説する。さらに、時間が許せばCoqについても解説する予定である。
ワークショップ「計算機にまつわる喫緊の問題を解決するための数学的手法」 (RIMS共同研究) 京都大学数理解析研究所 2階 202会議室概要
ウェブページ

2012 2011 2010 2009 2008 2007 2006 2005 2004 2003 2002 2001

香川考司（香川大学工学部）関数型プログラミング言語Haskellの理論と応用 (数理解析特別講義) ２００７年６月１１日（月）・１２日（火）、７月９日（月）・１０日（火）１３：３０-１７：００京都大学数理解析研究所１０２号室概要
本講義では、関数型プログラミング言語Haskellについて、その理論的基礎から実際的な応用までを解説する。 Haskellは、副作用を持たない、 CやJavaなどいわゆる“主流の言語”とは一風変わったプログラミング言語である。また、強力な型システムを持つことも大きな特徴である。本講義では、おもに次のようなトピックについて説明する。
- 遅延評価
- 型クラス
- リスト内包表記とモナド
- パーサコンビネータ
さらに時間が許せば、総合演習として命令型ミニ言語のインタプリタの作成を行なう。受講に際しては、ラムダ計算に関する基本的な知識があること、また、 SchemeやMLなどの関数型プログラミング言語を使用した経験があることが望ましい。
蓮尾一郎 The Microcosm Principle and Concurrency in Coalgebras ２００７年４月２６日（木）１４：００-１５：００旧工学部７号館・コンピュータサイエンス室概要
Coalgebras are categorical presentations of state-based systems. In considering parallel composition of coalgebras (realizing "concurrency"), we observe that the same algebraic structure (e.g. the binary operation || for parallel composition and its associativity) occurring in two different domains, in a nested manner, namely: on the category CoAlg(F) and on its final object (Z -> FZ). This is an instance of what is called the microcosm principle, a prototypical example of which is the nested structure "a monoid is defined in a monoidal category". We formalize the microcosm principle using Lawvere theories in a 2-categorical setting. From this general account, we get the compositionality result (saying "behavior of a composed system is determined by that of each component") for free. (Joint work with Bart Jacobs and Ana Sokolova)
長谷川真人相互作用の幾何、線型分解とトレース付きモノイダル圏２００７年４月１１日（水）１６：３０-京都大学数理解析研究所２０２号室（数理解析研究所談話会）概要
１９８０年代後半に、Girardは、証明論における三段論法の除去の過程のモデルとして相互作用の幾何（Geometry of Interaction、GoI）を提案しました。その後、GoIは、Abramskyらにより、双方向のコミュニケーションを伴う計算のモデルを構成する技法として位置づけられ、９０年代半ばには、Joyal、 Street、Verityの、トレース付きモノイダル圏（traced monoidal category）からトーティルモノイダル圏（tortile monoidal category、ribbon category またはbraided compact closed category）を構成する一般的な方法の、特殊な場合になっていることが明らかになりました。トレース付きモノイダル圏は、そのモノイダル積が直積である場合には、再帰プログラムの意味論で用いられている不動点演算子を持つ圏に他なりません（長谷川、Hyland）。したがって、GoIは、再帰プログラムのモデルから、双方向計算のモデルを作り出す仕組みとして用いることが出来ます。ところで、GoIとは別に、「線型な」計算ないし論理のモデルから、非線型な（というより通常の）計算／論理のモデルを作り出す一般的な方法（線型分解、linear decomposition）が、やはりGirardが考案した線型論理（linear logic）の枠組みに基づいて広く用いられています。先述のトーティルモノイダル圏も線型な計算のモデルになっていますので、トーティルモノイダル圏から適当な線型分解により非線型な計算モデルを得ることが出来ます。得られるモデルは、一体どのようなものでしょうか？この講演では、GoIとトレース付きモノイダル圏、線型論理のモデルの理論と線型分解について紹介したあと、適当な条件のもとで、GoIが線型分解の「逆」になっていること、そしてその簡単な応用として、再帰を持つ型付きラムダ計算の任意のモデル（トレース付きカルテジアン閉圏）は、あるトーティルモノイダル圏から線型分解によって得られるモデルと同値になることを示します。時間が許せば、ゲーム意味論という比較的新しい計算モデルの理論との関係についても考察したいと思います。

2012 2011 2010 2009 2008 2007 2006 2005 2004 2003 2002 2001

Ewen Denney (NASA Ames Research Center，US)Certifiable Program Synthesis２００６年９月２５日（月）１６：００- 京都大学数理解析研究所２０２号室概要
Software is playing an increasingly important role in space missions, and as NASA transitions from the space shuttle to the new Orion Space Vehicle, this trend will certainly continue. However, new techniques are needed to give the high levels of assurance that are required for safety and mission critical software. Program synthesis (also known as automated code generation) is a technology which could be applied in many NASA missions, but concerns over the safety and comprehensibility of generated code have hampered its widespread adoption. One solution to the safety problem is to extend the generator in such a way that it automatically certifies that the code it generates is safe, a technique we call certifiable program synthesis. I will describe the domain-specific code generators, AutoBayes and AutoFilter, which work in the domains of data analysis and state estimation, respectively, and give an overview of some of the techniques used to achieve safety.
中田景子Recursive Modules for Programming (joint work with Jacques Garrigue)２００６年９月５日（火）１４：００- 京都大学数理解析研究所２０２号室概要
勝股審也Algebraic Fusion of Functions with an Accumulating Parameter and Its Improvement (joint work with Susumu Nishimura)２００６年９月５日（火）１４：００- 京都大学数理解析研究所２０２号室概要
Philip Wadler (University of Edinburgh)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 (University of Edinburgh)The Girard-Reynolds isomorphism (second edition)２００６年４月２８日（金）１６時- 京都大学数理解析研究所１階１１５号室概要
Martin Berger (Queen Mary, University of London)A Logical Analysis of Aliasing in Imperative Higher-Order Functions２００６年３月２４日１４：００- 京都大学数理解析研究所１１５号室概要
We present a compositional program logic for call-by-value imperative higher-order functions with general forms of aliasing, which can arise from the use of reference names as function parameters, return values, content of references and parts of data tructures. The program logic extends our earlier logic for alias-free imperative higher-order functions with new modal operators which serve as building blocks for clean structural reasoning about programs and data structures in the presence of aliasing. This has been an open issue since the pioneering work by Cartwright-Oppen and Morris twenty-five years ago. We illustrate usage of the logic for description and reasoning through concrete examples including a higher-order polymorphic Quicksort. The logical status of the new operators is clarified by translating them into (in)equalities of reference names. The logic is observationally complete in the sense that two programs are observationally indistinguishable iff they satisfy the same set of assertions. (Joint work with Kohei Honda and Nobuko Yoshida)

2012 2011 2010 2009 2008 2007 2006 2005 2004 2003 2002 2001

Vincent Schmitt (University of Leicester)Saturated Classes of Colimits２００５年１２月２７日（火）１１：００- 京都大学数理解析研究所２０２号室概要
This talk will be a survey on enriched category theory including recent results obtained with Max Kelly. I will recall the notion of saturated classes of weights due to Albert and Kelly. I will show that it brings considerable conceptual simplifications for the study of categories with colimits of some class: accessible categories and Cauchy-completeness. Depending on time I could say more regarding categories of continuous functors.
Irek Ulidowski (University of Leicester)Reversing Algebraic Process Calculi２００５年１１月２８日（月）１４：００- 理学部６号館６階６０９号室概要
Reversible computation has a growing number of promising application areas such as the modelling of biochemical systems, program debugging and testing, and even programming languages for quantum computing. We formulate a procedure for converting operators of standard algebraic process calculi such as CCS, ACP and CSP into reversible operators, while preserving their operational semantics. We define a forward-reverse bisimulation and prove that it is a congruence for all reversible operators. (Joint Work with Iain Phillips)
結縁祥治 (名古屋大学大学院情報科学研究科)通信プロセスモデルにおける並行計算の代数的意味２００５年７月１６日（火）-２２日（金）１４：００-１６：００理学部数学教室１０９号室（３号館１階）概要
本講義では、CCS、CSPなどをはじめとする通信プロセスモデルによる並行計算モデルとその上で展開される代数的意味論について述べる。通信プロセスモデルは並行に実行されるプロセスが互いに同期通信を行いながら計算が進行する形式的な計算モデルである。このモデルにおける特徴は、プロセスによる通信を観測して意味論を構築することである。このことによって、計算が開始される前の入力と終了後の出力を観測する伝統的な関数による計算の意味づけを一般に拡張した意味論が展開することが可能になり、並行計算のもつ非決定性、非停止性などの特徴を表現することができる。本講義では、通信プロセスモデルにおける基本的な双模倣意味論による代数的な意味論、様相論理による特性化、等式にもとづく公理的な特性化などの基本的な意味付けについて述べ、一般的な意味論構築のための構造動作意味定義(SOS)のための理論、時間および確率などの拡張、さらに、時間の許す範囲で近年盛んに研究されているπ計算の動作意味についても述べる。
Donald Sannella (University of Edinburgh)Mobile Resource Guarantees２００５年６月２日（木）１４：００- 京都大学数理解析研究所００９号室概要
The Mobile Resource Guarantees (MRG) project is building infrastructure for endowing mobile bytecode programs with independently verifiable certificates describing their resource consumption. These certificates will be condensed and formalised mathematical proofs of a resource-related property which are by their very nature self-evident and unforgeable. Arbitrarily complex methods may be used to construct such a certificate, but once constructed its verification will always be a simple computation. This makes it feasible for the recipient to check that the proof is valid, and so the claimed property holds, before running the code. This work falls within an area known as "proof carrying code". Our focus in MRG on quantitative resource guarantees is different from the traditional PCC focus which is security. Another novelty is the method to be used to generate proofs, which is to use a "linear" type system that classifies programs according to their resource usage as well as according to the kinds of values they consume and produce. The intention is to generate proofs of resource usage from typing derivations. The MRG project (IST-2001-33149), which is a collaboration between the University of Edinburgh and LMU Munich, is funded by the European Commission under the FET proactive initiative on Global Computing. See http://groups.inf.ed.ac.uk/mrg/ for more information.
Paul-Andre Mellies (Universite Paris VII)An introduction to asynchronous game semantics２００５年１月２６日（水）１４：００- 京都大学数理解析研究所２０６号室概要
In game semantics, the higher-order value passing mechanisms of the lambda-calculus are decomposed as sequences of atomic actions exchanged by a Player and its Opponent. Seen from this angle, game semantics is akin to trace semantics in concurrency theory, where a process is identified to the sequences of requests it generates in the course of time. Asynchronous game semantics is an attempt to bridge the gap between the two subjects, and to see mainstream game semantics as a refined and interactive form of trace semantics. Asynchronous games are positional games played on Mazurkiewicz traces, which reformulate (and generalize) the usual notion of arena game. The framework enables to analyze the interleaving semantics of lambda-terms, expressed as innocent strategies, in the perspective of true concurrency. The analysis reveals that innocent strategies are positional strategies regulated by forward and backward confluence properties. A further distinction between external and internal positions in asynchronous games leads to the very first sequential game model of full propositional linear logic --- in the style of Blass games.

2012 2011 2010 2009 2008 2007 2006 2005 2004 2003 2002 2001

中田景子Recursive Object-Oriented Modules２００４年１２月１６日（木）１４：００数理解析研究所１１５号室概要
ML-style modules and classes are complementary. The former are better at structuring and genericity, the latter at extension and mutual recursion. We investigate the convergence of both mechanisms by designing an object-oriented calculus based on a nominal module system with mutual recursion. Our modules assume simultaneously the roles of classes with subtyping, nested structures with type members, and simple functors. Flexible inter-module recursion is obtained by allowing free references not constrained by the order of definitions. Close examination of the well-foundedness of the recursion is performed, in the presence of nesting and functors. To keep the mutual recursion seen in object-oriented languages, we propose an innovative approach to the well-foundedness, by considering the topological sortability of modules. Its static inspection is possible at the cost of some forms of parametricity. The presented type system is provably decidable, and ensures well-foundedness of the recursion. The paper also presents a call-by-value semantics, for which type soundness is proved. [To be presented at the International Workshop on Foundations of Object-Oriented Languages (FOOL-12), joint work with Akira Ito and Jacques Garrigue]
Erik Poll (University Nijmegen)From algebras and coalgebras to dialgebras２００４年１２月１０日（金）１５：００- 数理解析研究所００９号室概要
Algebras and coalgebras are dual notions, and are in some intuitive sense `opposites'. However, algebras and coalgebras also have certain things in common. (For example, the standard example of an algebraic specification, stacks, also occurs in the literature as an example of a coalgebraic specification.) The notion of dialgebra, introduced by Hagino, generalises the notions of algebra and coalgebra. We investigate in how far properties of (co)algebras - in particular properties of invariants and bisimulations - can be generalised to arbitrary dialgebras, to get a better understanding of what the essential differences between algebras, coalgebras, and dialgebras are. We relate the notion of observational equivalence for dialgebras can be seen as a special case of observational equivalence of abstract datatypes (eg., as provided in the second-order lambda calculus) in type theory.
中田景子相互参照のあるオブジェクト指向モジュールシステム２００４年９月２日（木）１４：００- 数理解析研究所１１５号室概要
石原存下極限に基づく無限項書換え系２００４年９月２日（木）１４：００- 数理解析研究所１１５号室概要
西村進（理・数学）Fusion with Stacks and Accumulating Parameters２００４年８月１６日（月）１４：００- 理学部６号館６０９号室概要
We propose a new algorithm for fusion transformation that allows both stacks and accumulating parameters. The new algorithm can fuse programs that cannot be handled by existing fusion techniques. The algorithm is formulated in a modular, type-directed style where the transformation process is comprised of several transformation steps that change types but preserve the observational behavior of programs. We identify a class of functions to which our new fusion method successfully applies and show that a closure property holds for that class. (to be presented at PEPM'04)
大崎人士（産総研）書換系とツリー・オートマトン理論: システム検証の自動化を目指して (数理解析特別講義１計算理論特別講義) ２００４年７月２６（月）- ３０（金）１４：００ - １５：３０理学部数学教室１０９号室（３号館１階）概要
本講義では，書換系(かきかえけい)とツリー・オートマトンを数理的な枠組みとする．はじめに，書換系についての基本概念についての解説をする．次に，書換系のひとつのインスタンスとしてのツリー・オートマトンに話題を移し，閉包性および決定可能性の問題について述べる．さらに，最近の研究成果により明らかとなった等式付ツリー・オートマトンとペトリネット (等式付書換系の一種)との関連，等式付ツリー・オートマトンをもとに定義される言語階層の形式言語論的な解釈をおこなう．さらに，システム検証の自動化に向けた最近の研究の取り組みについて，デモンストレーションなどを交えて紹介する．
Per Martin-Lf (University of Stockholm) 佐藤雅彦 (解説/情報学研究科)Types and Categories (情報学研究科佐藤研究室と共催) ２００４年５月２６日（水）・６月３日（水）１４：３０- 数理解析研究所２０６号室概要

2012 2011 2010 2009 2008 2007 2006 2005 2004 2003 2002 2001

西村進（理・数学）Correctness of a Higher-Order Removal Transformation through a Relational Reasoning ２００３年１１月２１日（金）１６：００- 数理解析研究所００９号室概要
The syntactic logical relations developed by Pitts are applied to show the correctness of a higher-order removal program transformation algorithm. The convenient proof method that resorts to the induction on the structure of programs does not apply because of the circular references to be introduced by the transformation. In this talk, it is shown that a relational reasoning based on a variant of the syntactic logical relations, where every pair of the transformation source and target are related, can break the circularity and make an inductive proof go through.
勝股審也 (LFCS, University of Edinburgh) Behavioural Equivalence and Indistinguishability in Higher-Order Typed Languages ２００３年８月８日（金）１６：００- 数理解析研究所１１５号室概要
We extend the study of the relationship between behavioural equivalence and indistinguishability relation to the simply typed lambda calculus, where higher-order types are available. The main technical tool of this study is pre-logical relations, which give a precise characterisation of behavioural equivalence. We establish a relationship between behavioural equivalence and indistinguishability in terms of factorisability. We then consider a higher-order logic to reason about models of the simply typed lambda calculus, and relate the resulting standard satisfaction relation to behavioural satisfaction.
角谷良彦Parameterizations and Fixed-Point Operators on Control Categories２００３年５月２８日（水）１６：００- 数理解析研究所２０６号室概要
The $\lambda\mu$-calculus features both variables and names, together with their binding mechanisms. This means that constructions on open terms are necessarily parameterized in two different ways for both variables and names. Semantically, such a construction must be modeled by a bi-parameterized family of operators. In this paper, we study these bi-parameterized operators on Selinger's categorical models of the $\lambda\mu$-calculus called control categories. The overall development is analogous to that of Lambek's functional completeness of cartesian closed categories via polynomial categories. As a particular and important case, we study parameterizations of uniform fixed-point operators on control categories, and show bijective correspondences between parameterized fixed-point operators and non-parameterized ones under uniformity conditions. (Joint work with Masahito Hasegawa, to appear in TLCA'03)
XML処理手法と理論(XYZ) (京都大学数理解析研究所短期共同研究) ２００３年５月１５日-１６日数理解析研究所１１５号室概要
Irek Ulidowski (University of Leicester)Structured Operational Semantics with Orderings on Rules２００３年４月７日（月）１６：００- 数理解析研究所１０２号室概要
A process language framework for concurrent systems is presented. The framework is defined using the Ordered Structural Operational Semantics (OSOS) approach, where traditional Plotkin-style SOS rules have orderings associated with them. The orderings allow one to control the order of application of SOS rules when deriving transitions of process terms. The framework is very expressive: it allows one to express easily a wide range of functional and temporal behaviour of concurrent systems. Also, it allows the user to define new task specific operators and features such as, for example, the notion of time and random delays. Once the user has chosen her process language (i.e. the operators, time and other features, and a suitable semantics), the process language is given an operational definition by means of OSOS rules and orderings on rules. Depending on the chosen semantics, OSOS rules and semantics must satisfy several simple conditions. These conditions restrict the structure of OSOS rules and the type of rule orderings that can be used. As a result, the defined process language preserves the chosen semantics. As an example, a class of OSOS process languages preserves bisimulation semantics. Several other classes of process languages that preserve weak semantics, e.g. testing equivalence and eager bisimulation, will be briefly discussed. Software tools such as Concurrency Workbench and PAC (Process Algebra Compiler) can be adapted to accept general process languages and to perform simple verification with respect to the chosen semantics.
Nobuko Yoshida (Department of Computing, Imperial College)Strong Normalisation in the Pi-Calculus２００３年３月４日（火）１５：００- 数理解析研究所２０６号室概要
Fedor Fomenko (LFCS, University of Edinburgh)Categorical Understanding of Feasible Computations２００３年２月２６日（水）１６：００- 数理解析研究所２０６号室概要
I will briefly describe known implicit characterisation of feasible computations and then try to outline how one can try to understand these categorically.
中野圭介Composing Stack-Attributed Tree Transducers２００３年１月２２日（水）１６：００- 数理解析研究所２０６号室概要
We present a composition method for stack-attributed tree transducers. Stack-attributed tree transducers extend attributed tree transducers with a pushdown stack device for attribute values. Stack-attributed tree transducers are more powerful than attributed tree transducers due to the stack mechanism. We extend an existing composition method for attributed tree transducers to the composition method for stack- attributed tree transducers. The composition method is proved to be correct and to enjoy a closure property. In this talk, we also present a practical application of the composition method, that is an XML stream transformer generator.
Alex Simpson (LFCS, University of Edinburgh/京都大学数理解析研究所) Topology and Computation (数理解析研究所談話会) ２００３年１月８日（水）１６：００- 数理解析研究所２０２号室概要
Topology plays a fundamental role in the modelling of computation. This talk will provide a gentle introduction to topology from a computational viewpoint, emphasising, in particular, interesting differences between computational topology and familiar mathematical topology as usually developed for geometric and analytic purposes. In the talk, I will assume just a working mathematician's knowledge of topology. No knowledge of computation will be required.

2012 2011 2010 2009 2008 2007 2006 2005 2004 2003 2002 2001

Alex Simpson (LFCS, University of Edinburgh/京都大学数理解析研究所) Interpreting Set Theory in Toposes (5)２００２年１２月２０日（金）１１：００- 数理解析研究所１１５号室概要
第１３回代数、論理、幾何と情報科学研究集会 (ALGI-13) (京都大学数理解析研究所短期共同研究) ２００２年１２月１６日-１９日数理解析研究所１１５号室概要
Alex Simpson (LFCS, University of Edinburgh/京都大学数理解析研究所) Interpreting Set Theory in Toposes (4)２００２年１２月６日（金）１１：００- 数理解析研究所４０２号室概要
細谷晴夫Regular Expression Filters for XML２００２年１２月４日（水）１６：００- 数理解析研究所２０６号室概要
XML data are described by types involving regular expressions. This raises the question of what a convenient language feature is to manipulate such data. Previous proposals for XML processing languages such as XSLT and XQuery typically provide a ``for each'' loop construct. However, it only permits the independent processing of each children node and has no way to exploit the full structure of regular expressions. In this talk, I propose a novel programming feature {\em regular expression filters}. This construct stems from our previous proposal, regular expression pattern matching, which is inspired by the corresponding ML-style construct. We extend it by allowing pattern clauses to be closed under arbitrary regular expression operators, yielding a significat expressiveness. In particular, a clause closed by a Kleene star can iterate on sequences with no need to write an explicit recursion. In addition, we equip a typing inference mechanism that obtains (1) types for pattern variables that are {\em locally precise} with respect to the type of input values and (2) a type for the result of the whole filter expression that is also locally precise with respect to the types of the body expressions. I discuss how our construct is useful in the practice of XML processing and, in particular, how our type inference is crucial when type evolution is involved.
Alex Simpson (LFCS, University of Edinburgh/京都大学数理解析研究所) Interpreting Set Theory in Toposes (3)２００２年１１月２２日（金）１１：００- 数理解析研究所４０２号室概要
長谷川真人Classical Linear Logic of Implications２００２年１１月２０日（水）１６：００- 数理解析研究所２０６号室概要
We give a simple term calculus for the multiplicative exponential fragment of Classical Linear Logic, by extending Barber and Plotkin's system for the intuitionistic case. The calculus has the non-linear and linear implications as the basic constructs, and this design choice allows a technically managable axiomatization without commuting conversions. Despite this simplicity, the calculus is shown to be sound and complete for category-theoretic models given by *-autonomous categories with linear exponential comonads. This talk is largely based on the paper presented at CSL'02 (available from here).
Alex Simpson (LFCS, University of Edinburgh/京都大学数理解析研究所) Interpreting Set Theory in Toposes (2)２００２年１１月１５日（金）１１：００- 数理解析研究所４０２号室概要
西村進Deforesting in Accumulating Parameters via Type-Directed Transformations２００２年１１月１３日（水）１６：００- 数理解析研究所２０６号室概要
Classical deforestation methods fail to compose functions with accumulating parameters, which are function arguments to which intermediate result accumulates. This paper proposes a new deforestation method which solves this problem. The method is comprised of a few transformation steps, each of which is guided by type information. Though our solution draws its fundamental idea from a deforestation method that has been developed for attribute grammars, it is not merely a recast of an existing technique to another formalism. The new method provides a type-based account for the existing attribute grammar deforestation process. Further, it can deforest a class of functions that the attribute grammar deforestation cannot. These advantages are demonstrated by a few examples. It is also shown that the new method is as powerful as another method that has been developed for macro tree transducer composition. A draft version of the accompanied paper (being prepared for APLAS'02 workshop) is available from here.
Alex Simpson (LFCS, University of Edinburgh/京都大学数理解析研究所) Interpreting Set Theory in Toposes (1)２００２年１１月８日（金）１１：００- 数理解析研究所４０２号室概要
Jacques GarrigueRelaxing the Value Restriction２００２年１１月６日（水）１６：００- 数理解析研究所２０６号室概要
Restricting polymorphism to values is now the standard way to obtain soundness in ML-like programming languages with imperative features. While this solution has undeniable advantages over previous approaches, it forbids polymorphism in many cases were it would be sound. We use a subtyping based approach to recover a small part of this lost polymorphism, without changing the type algebra itself, and this has significant applications.
沢田潤（IBM Austin Research Lab）Mechanical Verification of a Square Root Algorithm using Taylor's Theorem２００２年８月１６日（金）１５：００- 数理解析研究所２０２号室概要
The IBM Power4(TM) processor uses Chebyshev polynomials in the calculation of square root. We formally verified the correctness requirement of this algorithm using the ACL2(r) theorem prover. Such a formal verification is critical to guarantee the quality of a microprocessor. The ACL2 theorem prover is a descendent of the Boyer-Moore prover, and it is both a programming system and a mechanical theorem proving system. The ACL2 prover does not axiomatize the real numbers, thus the user cannot prove any theorems involving irrationals. ACl2(r) is an extension of the ACL2 prover for real numbers, by way of the non-standard analysis introduced by Robinson. The ACL2(r) prover has been used to prove various theorems such as the correctness of the Fast Fourier Transformation (FFT) algorithm and the Fundamental Theorem of Analysis. Here, we discuss the use of ACL2(r) in the analysis of a square root algorithm used in an industrial processor. This is done, by first proving Taylor's theorem, and then used it to analyze the size of the rounding and approximation error of the algorithm. One challenge in formally verifying this particular algorithm is in the analysis of the Chebyshev polynomial. Since a Taylor polynomial has less accuracy than the Chebyshev polynomial of the same degree, the error measurement of a Chebyshev polynomial using a Taylor polynomial is not straightforward. We instead used hundreds of Taylor polynomials to evaluate the error size of a Chebyshev polynomial. This approach makes the error size analysis easier to automate.
五十嵐淳（京大・情報）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.
Jean-Philippe Vert（京都大学化学研究所バイオインフォマティクスセンター）２００２年７月１２日（金）１６：００-１７：００数理解析研究所２０２号室概要
A major goal of post-genomic era reasearch is to better understand the functions and interactions of genes discovered during the sequencing projects recently completed. To this end new technologies such as DNA chips or Yeast 2-hybrid systems are routinely used to produce large amounts of data aimed at characterizing each gene. In order to integrate these various types of information we propose a mathematical framework where a particular type of information is encoded into a kernel function on the set of genes, and where the comparison of two types of information can be performed using linear data mining methods in the corresponding reproducible kernel Hilbert spaces. As an application we show how to extract correlations between microarray data on the one hand, and gene networks on the other hand.
五十嵐淳（京大・大学院情報学研究科）Resource Usage Analysis (数理解析研究所談話会) ２００２年５月１５日（水）１６：００- 数理解析研究所２０２号室概要
It is an important criterion of program correctness that a program accesses resources in a valid manner. For example, a memory region that has been allocated should be eventually deallocated, and after the deallocation, the region should no longer be accessed. A file that has been opened should be eventually closed. So far, most of the methods to analyze this kind of property have been proposed in rather specific contexts (like studies of memory management and verification of usage of lock primitives), and it was not so clear what is the essence of those methods or how methods proposed for individual problems are related. To remedy this situation, we formalize a general problem of analyzing resource usage as a {\em resource usage analysis problem}, and propose a type-based method as a solution to the problem. [Joint work with Naoki Kobayashi]
XML処理における理論的アプローチ (XYZ) (京都大学数理解析研究所短期共同研究) ２００２年４月４日-５日数理解析研究所１１５号室概要
Martin Hofmann (University of Muenchen) Another Type System for In-Place Update (Joint work with David Aspinall)２００２年３月８日（金）１６：００- 数理解析研究所２０６号室概要
Linear typing schemes guarantee single-threadedness and so the soundness of in-place update with respect to a functional semantics. But linear schemes are restrictive in practice, and more restrictive than necessary to guarantee soundness of in-place update. This has prompted research into static analysis and more sophisticated typing disciplines, to determine when in-place update may be safely used, or to combine linear and non-linear schemes. Here we contribute to this line of research by defining a new typing scheme which better approximates the semantic property of soundness of in-place update for a functional semantics. We begin from the observation that some data is used only in a ``read-only'' context after which it may be safely re-used before being destroyed. Formalizing the in-place update interpretation and giving a machine model semantics allows us to refine this observation. We define three \emph{usage aspects} apparent from the semantics, which are used to annotate function argument types. The aspects are (1) used destructively, (2) used read-only but shared with result, and (3) used read-only and not shared.

2012 2011 2010 2009 2008 2007 2006 2005 2004 2003 2002 2001

Lennart Beringer (LFCS, University of Edinburgh)Typing Assembly Programs with Explicit Forwarding２００１年１１月５日（月）１６：００- 数理解析研究所１１５号室概要
We consider processor architectures where communication of values is achieved through operand queues instead of registers. Explicit forwarding tags in an instruction's code denote the source of its operands and the destination of its result. We give operational models for sequential and distributed execution, where no assumptions are made about the relative speed of functional units. We introduce type systems which ensure that programs use the forwarding mechanism in a coordinated way, ruling out various run time hazards. Deadlocks due to operand starvation, operand queue mismatches, non-determinism due to race conditions and deadlock due to the finite length of operand queues are eliminated. Types are based on the shape of operand queue configurations, abstracting from the value of an operand and from the order of items in operand queues. Extending ideas from the literature relating program fragments adjacent in the control flow graph, the type system is generalised to forwarding across basic blocks.
長谷川真人Linearly Used Effects (Or: A Fully Complete CPS Transform)２００１年１０月２４日（水）１６：００- 数理解析研究所２０６号室概要
今年のContinuation Workshop (CW'01)でBerdine達が発表した"linearly used continuations"の仕事を、MLやSchemeのような副作用（effects）を持つ値呼びプログラミング言語に対応するcalculusからlinear lambda calculusへのコンパイル（monadic変換）として定式化・一般化して、syntax・semantic 両面から攻める...という、現在進行中の研究です。特に、continuationの場合には、linear lambda calculusへのCPS (continuation-passing style) 変換が、fully completeという良い性質を持つことがわかっています。
細谷晴夫型付きXML処理言語XDuce (数理解析研究所談話会) ２００１年１０月１７日（水）１６：００- 数理解析研究所２０２号室概要
XMLとは、アプリケーション間で交換されるデータの形式を定義するための産業仕様であり、近年その汎用性から広く関心を集めている。XMLでは、(1) 一般的なツリーデータ構造と、(2) そのツリーの制約条件を記述するスキーマ、を定義している。アプリケーション開発者は、スキーマを書くことによって、アプリケーション独自のデータ形式を簡単に制定することができる。本研究では、XMLデータ処理に特化した型付きプログラミング言語XDuce（「トランスデュース」と読む）の設計・実装を行っている。「型付き」とは、コンパイラに「型検査」と呼ばれる機構が備わっていると言うことである。型検査は、与えられたプログラムを解析し、「このプログラムを実行して得られた出力データはある制約条件を常に満たす」と言うこと（型安全性という）を保証する。型検査は、古くからある機構であり、C言語やJava言語などの普通のプログラミング言語にも備わっている。しかし、本研究においては、XML のスキーマをデータ型と見なす。XML のスキーマには子ノード列の制約条件を記述するために正規表現が用いられるが、これを型システムに導入するという点が、従来の型検査と異なる。さらにこうしてできた型システムが型安全性を持つことを数学的に証明し、この型システムを組み込んだXDuce言語を設計した。この型システムの設計には、スキーマの正規性を多用している。正規性とは、スキーマがツリーオートマトン（ツリーを受理する有限状態機械）と等価ということである。これによって、２つのスキーマの和、積、もしくは差を表すスキーマを計算することが可能であるということや、包含関係を判定することも可能であることがわかる。特に、本型システムにおける部分型は包含関係であると定義され、ユーザに高い柔軟性を提供するために重要である。一方、包含関係の判定は指数時間完全という高い計算量を持つことがわかっている。そのため本研究では、実際の入力に対しては実用的速度で動作する「トップダウン」なアルゴリズムを開発した。
Jacques GarrigueHindley-Milner with Local Constraints: Extending Type Inference the Easy Way２００１年１０月１０日（水）１６：００- 数理解析研究所２０２号室概要

Research Institute for Mathematical Sciences, Kyoto University, 606-8502 Japan.