Computer Science Team, Research Institute for Mathematical SciencesKyoto University

Also running is a more informal series of seminars, Logic and Semantics Seminar.

• 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 11.00 -, Thursday January 12th General Research Building 2 (next to the CS room) (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.

• Kenshi Miyabe (RIMS, Kyoto University) Characterization of Kurtz randomness by a differentiation theorem 11.00 - 12.00, Thursday 17 November 2011 General Research Building 2 (next to the CS room) (map) Abstract

  Brattka, Miller and Nies showed that some major algorithmic randomness notions are characterized via differentiability. The main goal of this talk is to characterize Kurtz randomness by a differentiation theorem on a computable metric space. The proof shows that characterization by integral tests plays an essential part and shows that how randomness and differentiation are connected.

• 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 General Research Building 2 (next to the CS room) (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.

• Kohei Suenaga (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 General Research Building 2 (next to the CS room) (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.

• Naohiko Hoshino (RIMS, Kyoto University) Semantics for higher-order quantum computation via Geometry of Interaction 11.50? - 12.40?, Thursday 16 June 2011 Room 478, Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan)(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.

• Kenshi Miyabe (RIMS, Kyoto University) Characterizing randomness by integral tests 11.00 - 11.50?, Thursday 16 June 2011 Room 478, Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan)(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 (RIMS, Kyoto University) A gentle introduction to ludics11.00 - 12.00, Thursday 21 April 2011Room 478, Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan) (map) Abstract

  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 2011Room 478, Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan) (map) Abstract

  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.

• Yoshihiro Maruyama (Department of Humanistic Informatics, Kyoto Univ.) Natural Duality, Modality and Coalgebra 11.00 - 12.00, Tuesday 8 March 2011Room 478, Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan) (map) Abstract

  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/

• Ryu Hasegawa (Tyoto Univ.) A proof of the Church-Rosser property based on the combinatorial enumeration model 111.00 - 12.00, Februrary 24th (Thu)Room 478, Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan) (map)
• Susumu Nishimura (Dept. Math., Kyoto Univ.) Calculating Tree Navigation with Symmetric Relational Zipper11.00 - 12.00, Thursday 20 January 2011Room 478, Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan) (map) Abstract

  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.

• Kohei Suenaga (Universidade de Lisboa, Portugal)Fractional Ownerships for Safe Memory Deallocation11.00 - 12.00, Thu 2 Dec 2010Room 478, Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan) (map) Abstract

  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.

• Kazushige Terui (RIMS, Kyoto U.)Church => Scott = Ptime: an application of resource sensitive realizability11.00 - 12.00, Thu 25 Nov 2010Room 478, Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan) (map) Abstract

  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.

• Yawara Ishida (RIMS, Kyoto Univ.) 11.00 - 12.00, Thursday 28 Oct 2010Room 478, Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan) (map) Abstract
• Ichiro Hasuo (RIMS, Kyoto Univ.) Generic Forward and Backward Simulations II: Probabilistic Simulation11.00 - 12.00, Thursday 26 Aug 2010Room 478, Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan) (map) Abstract

  Jonsson and Larsenﾂ｡ﾃ㎏ 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.

• Shin-ya Katsumata (RIMS, Kyoto Univ.) Categorical Descriptional Composition11.00 - 12.00, Thursday 29 July 2010Room 478, Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan) (map) Abstract

  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.

• Masahito Hasegawa (RIMS, Kyoto Univ.) Small-step and big-step semantics for call-by-need (joint work with Keiko Nakata)11.00 - 12.00, Thursday 15 July 2010Room 478, Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan) (map) Abstract

  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.

• Naohiko Hoshino (RIMS, Kyoto Univ.) A modification of GoI interpretation for DILL11.00 - 12.00, Thursday 24 June 2010Room 478, Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan) (map) Abstract

  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.

• Takeo Uramoto (Dept. Math., Kyoto Univ.) ++-construction and filtration11.00 - 12.00, Thursday 17 June 2010Room 478, Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan) (map) Abstract

  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.

• Kenshi Miyabe (RIMS, Kyoto Univ.) Algorithmic randomness over general spaces11.00 - 12.00, Thursday 10 June 2010Room 478, Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan) (map) Abstract

  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.

• Masahito Hasegawa (RIMS, Kyoto Univ.) Traced monoidal categories and semantics of programming languages10.00 - 10.45, Thursday 3 June 2010Room 478, Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan) (map) Abstract

  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).

• Masahito Hasegawa (RIMS, Kyoto Univ.) A quantum double construction in Rel11.00 - 12.00, Thursday 3 June 2010Room 478, Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan) (map) Abstract

  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 2010Room 478, Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan) (map) Abstract

  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.

• Ichiro Hasuo (RIMS, Kyoto Univ.) Crash Introduction to Coalgebra (A primer to the subsequent talk)10.00 - 11.00, Thursday 20 May 2010Room 478, Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan) (map) Abstract

  The very basics of coalgebraic modeling in computer science are covered as a primer to my subsequent talk.

• Ichiro Hasuo (RIMS, Kyoto Univ.) Coalgebraic Representation Theory of Fractals (Act 2)11.00 - 12.00, Thursday 20 May 2010Room 478, Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan) (map) Abstract

  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 2010Room 478, Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan) (map) Abstract

  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 2010Room 305, Faculty of Science Bldg. No. 3 (map) Abstract

  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 2010Room 305, Faculty of Science Bldg. No. 3 (map) Abstract

  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.

• Keiko Nakata (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 2010Room 305, Faculty of Science Bldg. No. 3 (map) Abstract

  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 2010Room 305, Faculty of Science Bldg. No. 3 (map) Abstract

  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 2010Room 305, Faculty of Science Bldg. No. 3 (map) Abstract

  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.

• Irek Ulidowski (University of Leicester) Reverse Bisimulations on Stable Event Structures 11.00 - 12.00, Thursday 10 December 2009Room 203P, Faculty of Science Bldg. No. 6 (map) Abstract

  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 2009Room 203P, Faculty of Science Bldg. No. 6 (map) Abstract

  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 2009Room 203P, Faculty of Science Bldg. No. 6 (map) Abstract

  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].

• Ichiro Hasuo (RIMS, Kyoto Univ.) Coalgebraic Representation Theory of Fractals11.00 - 12.00, Thursday 1 October 2009Room 203P, Faculty of Science Bldg. No. 6 (map) Abstract

  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).

• Susumu Nishimura (Dept. Math., Kyoto Univ.) Refining Exceptions in Four-Valued Logic11.00 - 12.00, Thursday 9 July 2009CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; see direction ) Abstract

  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 ) Abstract

  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 ) Abstract

  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 ) Abstract

  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 ) Abstract

  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 ) Abstract

  Goedelﾂ｡ﾃ㎏ completeness theorem is concerned with provability, while Girardﾂ｡ﾃ㎏ 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ﾂ｡ﾃ㎏ completeness, in that it explicitly constructs a countermodel essentially using Koenigﾂ｡ﾃ㎏ lemma, proceeds by induction on formulas, and implies an analogue of Loewenheim-Skolem theorem.

• Taichi Haruna (Kobe Univ. & JST PRESTO)Category Theory in System Biology11.00 - 12.00, Thursday 21 May 2009CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; see direction ) Abstract
• 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 ) Abstract

  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 ) Abstract

  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 ) Abstract

  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 ) Abstract

  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 Abstract

  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 ) Abstract

• 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 ) Abstract

  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 ) Abstract

  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 Abstract

  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.

• Kohei Suenaga (Tohoku Univ.)Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts13.00 - 14.00, Monday 27 Oct 2008Room 202, RIMS, Kyoto University Abstract
• 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 ) Abstract

  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 Abstract

  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)).

• Yasuhiko Minamide (Univ. of Tsukuba)Introduction to Theorem Provers Abstract
• Workshop: Mathematics for Pressing Problems in Computer Science (RIMSﾂｶﾂｦﾃ・ｱﾂｸﾂｦﾂｵﾃｦ) Abstract

• 香川考司（香川大学工学部）関数型プログラミング言語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が線型分解の 「逆」になっていること、そしてその簡単な応用として、再帰を持つ型付きラ ムダ計算の任意のモデル（トレース付きカルテジアン閉圏）は、あるトーティ ルモノイダル圏から線型分解によって得られるモデルと同値になることを示し ます。時間が許せば、ゲーム意味論という比較的新しい計算モデルの理論との 関係についても考察したいと思います。

• 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)

• 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.

• 中田景子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 (情報学研究科 佐藤研究室と共催) ２００４年５月２６日（水）・６月３日（水） １４：３０- 数理解析研究所２０６号室 概要

• 西村 進 （理・数学）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.

• 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.

• 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２００１年１０月１０日（水）１６：００- 数理解析研究所２０２号室 概要