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

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

• Toru Takisaka (RIMS, Kyoto University) On large scale geometries of infinite strings 11:00-12:00, 15 June, 2017 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract

  Motivated by notions in geometric group theory, we introduce the concept of large scale geometry on infinite strings.

  Informally, two infinite strings have the same large scale geometry if there is a bi-Lipschitz map between both strings with a finite uniform distortion. We call these maps quasi-isometric maps.

  Introduction of large scale geometries poses several questions. The first question is related to understanding the partial order induced by quasi-isometric maps on large scale geometries of strings. We prove that there is the greatest large scale geometry and infinitely many minimal large scale geometries. The second is related to understanding the quasi-isometric maps on various classes of strings. The third question address the issue of building quasi-isometric maps between computable infinite strings. We show that the problem is Sigma_3-complete. The fourth question is about understanding sets of large scale geometries given some tools (e.g. Buchi automata) that describe sets of strings. We provide an efficient algorithm that gives a full description of large scale geometries of strings accepted by such automata. Finally, the fifth question asks if it is possible to associate with every large scale geometry an algebraic structure that describes the geometry uniquely. Here we use tools of geometric group theory by invoking the notion of asymptotic cone.

• Taichi Uemura (RIMS, Kyoto University) Fibred Fibration Categories 11:00-12:00, 15 June, 2017 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract

  We introduce fibred type-theoretic fibration categories which are fibred categories between categorical models of Martin-L\ouml{}f type theory. Fibred type-theoretic fibration categories give a categorical description of logical predicates for identity types. As an application, we show a relational parametricity result for homotopy type theory. As a corollary, it follows that every closed term of type of polymorphic endofunctions on a loop space is homotopic to some iterated concatenation of a loop.

• Takuma Imamura (RIMS, Kyoto University) Analogies between small scale topology and large scale topology from the nonstandard perspective 11:00-12:00, 14 June, 2017 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract

  Large scale topology is the study of the large scale (asymptotic) behaviour of various spaces. It is well-known that there are many analogies between small scale topology and large scale topology. We see some of these analogies in the light of nonstandard analysis, and give "definitions" of small scale topology and of large scale topology in terms of logic.

• Hisashi Aratake (RIMS, Kyoto University) Bicategory of Theories as an Approach to Model Theory 11:00-12:00, 14 June, 2017 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract

  We give a purely syntactic definition of bicategory Th of classical first-order theories, and show that it is biequivalent to the groupoid-enriched category BPretop_* of Boolean pretoposes. We also make a close observation on (internal) equivalences in Th. Morphisms and equivalences in Th are called interpretations and bi-interpretations respectively, which are familiar to model theorists. At the end of this talk, we briefly discuss expected applications of this framework to model theory.

• Ugo Dal Lago (University of Bologna) Context Equivalences and Metrics in Probabilistic Lambda-Calculi 11:00-12:00, 25 May, 2017 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract

  Probabilistic models are more and more pervasive in computer science, and randomized algorithms are the ones offering the best performances in many domains. Higher-order probabilistic computation -- in which probabilistic functions may be passed as a parameters and returned as results -- is on the other hand a relatively underdeveloped field, which is however receiving more and more attention. We give a survey of what is known about the probabilistic lambda-calculi, later focusing on some of our recent results on coinductive techniques for proving program equivalent and for evaluating their distance. Finally, we hint at how all this could be useful when structuring proofs of security for cyptographic primitives.

• Kenta Cho (Radboud University Nijmegen) An Effectus-Theoretic Perspective on Probabilistic Programming 11:00-12:00, 16 Feb, 2017 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract

  Modern probabilistic programming languages have the ability to "condition", which is an essential operation in Bayesian statistics to compute conditional (posterior, updated) probabilities given certain data. Probabilistic programming has attracted increasing attention especially for machine learning applications.

  Effectuses have recently been introduced as categorical models for quantum logic and computation, with probabilistic and Boolean as special cases. Based on the concepts of states and predicates in an effectus, we formulate "conditioning" as an operation on states and predicates. It then offers a language and semantics for Bayesian probabilistic reasoning. For example, backward and forward inference can be neatly captured by the combination of conditioning and state/predicate transformers. This works uniformly, not only in the discrete and continuous probabilistic setting, but also in the quantum setting.

  We are also developing a Python library implementing the effectus language based on states and predicates. It is currently not meant for large scale computation (e.g. machine learning), but is useful for modelling and calculating small probabilistic problems. The talk will include the use / demo of the library.

• Marc Bagnol (JSPS Postdoctoral Fellow, University of Tokyo) Multiplicative-Additive Proof Equivalence is Logspace-complete 11:00-12:00, 9 Feb, 2017 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract

  Given a logic presented in a sequent calculus, a natural question is that of equivalence of proofs: to determine whether two given proofs are equated by any denotational semantics, i.e. any categorical interpretation of the logic compatible with its cut-elimination procedure. This notion can usually be captured syntactically by a set of rule permutations.

  Very generally, proofnets can be defined as combinatorial objects which provide canonical representatives of equivalence classes of proofs. In particular, the existence of proof nets for a logic provides a solution to the equivalence problem of this logic. In certain fragments of linear logic, it is possible to give a notion of proofnet with good computational properties, making it a suitable representation of proofs for studying the cut-elimination procedure, among other things.

  It has recently been proved that there cannot be such a notion of proofnets for the multiplicative (with units) fragment of linear logic, due to the equivalence problem for this logic being Pspace-complete.

  We will investigate the multiplicative-additive (without unit) fragment of linear logic and see it is closely related to binary decision trees: we can build a representation of proofs based on binary decision trees, reducing proof equivalence to decision tree equivalence. We will see as a consequence that the proof equivalence problem multiplicative-additive linear logic is Logspace-complete.

• Leo Stefanesco (Ecole Normale Supérieure de Lyon) Asynchronous Games and Concurrent Separation Logic 11:00-12:00, 2 Feb, 2017 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract

  We develop a game-theoretic and asynchronous approach to concurrent separation logic. To every execution trace of the code confronted to the environment, we associate a separation game whose purpose is to decompose each intermediate state of the execution in three pieces: one piece for the Code, one piece for the Environment, and one piece for the locks. We establish the soundness of concurrent separation logic by associating to every derivation tree of the logic a winning strategy of this separation game. Then, shifting to an asynchronous notion of separation game, we show that two execution traces which take and release every lock in the same order are equivalent up to permutation of asynchronous tiles. This result implies in particular that the program is data-race free.

• Nao Hirokawa (Japan Advanced Institute of Science and Technology) Basic Normalization 11:00-12:00, 22 Dec, 2016 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract

  The Normalization Theorem (O'Donnell 1977) states that for every left-normal orthogonal rewrite system, the leftmost outermost strategy reduces any term to the normal form if it exists. Although the theorem ensures the normalization property of important systems such as Combinatory Logic, the left-normality condition rules out most of functional programs. We revisit the problem to seek a solution for normalization of the leftmost outermost strategy. This work is based on joint work with Aart Middeldorp and Georg Moser.

• Kei Matsumoto (RIMS, Kyoto University) Coherence Spaces and Uniform Continuity 11:00-12:00, 8 Dec, 2016 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract

  In this talk, we consider a model of classical linear logic based on coherence spaces endowed with a notion of totality. If we restrict ourselves to total objects, each coherence space can be regarded as a uniform space and each linear map as a uniformly continuous function. The linear exponential comonad then assigns to each uniform space X the finest uniform space !X compatible with X. By a standard realizability construction, it is possible to consider a theory of representations in our model. Each (separable, metrizable) uniform space, such as the real line R, can then be represented by (a partial surjecive map from) a coherence space with totality. The following holds under certain mild conditions: a function between uniform spaces X and Y is uniformly continuous if and only if it is realized by a total linear map between the coherence spaces representing X and Y.

• Bakh Khoussainov (University of Auckland) and Toru Takisaka (RIMS, Kyoto university) On large scale geometries of infinite strings 11:00-12:00, 1 Dec, 2016 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract

  Motivated by notions in geometric group theory, we introduce the concept of large scale geometry on infinite strings.

  Informally, two infinite strings have the same large scale geometry if there is a bi-Lipschitz map between both strings with a finite uniform distortion. We call these maps quasi-isometric maps.

  Introduction of large scale geometries poses several questions. The first question is related to understanding the partial order induced by quasi-isometric maps on large scale geometries of strings. We prove that there is the greatest large scale geometry and infinitely many minimal large scale geometries. The second is related to understanding the quasi-isometric maps on various classes of strings. The third question address the issue of building quasi-isometric maps between computable infinite strings. We show that the problem is Sigma_3-complete. The fourth question is about understanding sets of large scale geometries given some tools (e.g. Buchi automata) that describe sets of strings. We provide an efficient algorithm that gives a full description of large scale geometries of strings accepted by such automata. Finally, the fifth question asks if it is possible to associate with every large scale geometry an algebraic structure that describes the geometry uniquely. Here we use tools of geometric group theory by invoking the notion of asymptotic cone.

• Nayuta Yanagisawa (Dept. of Math., Kyoto University) Generalized Homogeneous Polynomials for Efficient Wait-Free Solvability of Colorless Tasks in Anonymous Shared-Memory Model 11:00-12:00, 27 Oct, 2016 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract

  We investigate the capability of distributed systems in the anonymous asynchronous shared-memory model, in which processes have no identifiers and communicate through multi-writer/multi-reader atomic registers. The present paper assumes that an arbitrary number of processes may fail by crashing. We propose a full-information protocol for colorless tasks and give a topological characterization of colorless tasks that are wait-free solvable in the anonymous model. The characterization implies, as long as colorless tasks are concerned, that the anonymity does not reduce the computational power of the asynchronous shared-memory model.

• 末永幸平(京都大学情報学研究科/ JST PRESTO) Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis
  (Joint work with Kensuke Kojima and Minoru Kinoshita) 11:00-12:00, 20 Oct, 2016 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract

  The template-based method is one of the most successful approaches to algebraic invariant synthesis. In this method, analgorithm designates a template polynomial (p) over program variables, generates constraints for (p=0) to be an invariant, and solves the generated constraints. However, this approach often suffers from an increasing template size if the degree of a template polynomial is too high.

  We propose a technique to make template-based methods more efficient. Our technique is based on the following finding: If an algebraic invariant exists, then there is a specific algebraic invariant that we call a generalized homogeneous algebraic invariant that is often smaller. This finding justifies using only a smaller template that corresponds to a generalized homogeneous algebraic invariant.

  Concretely, we state our finding above formally based on the abstract semantics of an imperative program proposed by Cachera et al. Then, we modify their template-based invariant synthesis so that it generates only generalized homogeneous algebraic invariants. This modification is proved to be sound. Furthermore, we also empirically demonstrate the merit of the restriction to generalized homogeneous algebraic invariants. Our implementation outperforms that of Cachera et al. for programs that require a higher-degree template.

• Adam Prenosil (Czech Academy of Sciences) Classical proof theory, non-classically 11:00-12:00, 13 Oct, 2016 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract

  We present an approach to cut elimination in classical logic which appeals to elimination rules.rather than to induction on cut rank and which works equally well for proofs from a non-empty set of sequential premises. As an illustration of the benefits of accepting elimination rules as an integral part of the sequent calculus for classical logic, we use the calculus with elimination rules to provide a particularly simple syntactic proof of a recent non-classical refinement of Craig's interpolation theorem due to Milne. This approach, while non-standard, is in fact natural when we view classical logic as part of the family of super-Belnap logics, that is, extensions of the four-valued Belnap-Dunn logic. We shall therefore start by introducing this family proof-theoretically as the logics which retain the structural and logical rules of classical logic, but relax Identity and Cut (as opposed to substructural logics, which retain Identity and Cut but relax the structural rules of classical logic).

• 山形賴之 (産業技術総合研究所) 11:00-12:00, 6 Oct, 2016 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract

  Bounded arithmetics are systems of arithmetic in which induction is restricted to bounded formulas. Bounded formulas are formulas in which all quantifiers are bounded by some terms. Among many such systems, Buss's hierarchy of bounded arithmetics have particular interest, because their provably total functions exactly correspond polynomial-time hierarchy.

  A major open problem on bounded arithmetics is whether Buss's hierarchy collapses or not. If it collapses, for example, it implies P=NP. One strategy to differentiate the hierarchy is to use Gödel sentence of some theories. In this talk, we consider a theory PV by Cook and Urquhart and its restrictions. PV is an equational system, which has roughly the same strength to Buss's S12. Beckmann proved that when induction and substitution are removed from PV, the consistency of the system can be proved by S12. On the other hand, Buss and Ignjatović proved that S12 cannot prove the consistency of the system which obtained by removing just induction, but adding propositional logic and BASIC axioms, from PV.

  In this talk, we improve the Beckmann by proving that S22 can prove the consistency of the system which obtained by removing just induction from PV. By delineating bounded arithmetics which can prove consistency of various restrictions of PV, we hope to prove non-collapse of Buss's hierarchy, and relatedly, polynomial-time hierarchy.

• Jun Maillard (ENS) Lifting monads (and more) along fibrations 11:00-12:00, 2 Aug, 2016 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract

  Fibrations have been sucessfully applied in several domains, in particular to discuss properties of (categorical) models. However these models generally carry more structure than the barebone category axioms. Focusing on monads, I would like to give an insight of what it means for such a structure to interact nicely with the fibration and why it is important. I will present a technical way to solve the problem called top-top-lifting (developped by S. Katsumata) and how it can be generalized to adjunctions.

• Takuma Imamura (RIMS, Kyoto University) Nonstandard Algebraic Topology of Uniform Spaces. 11:00-12:00, 14 Jul, 2016 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract

  McCord developed a homology theory of topological spaces by using nonstandard analysis, the advent of nonstandard algebraic topology. McCord homology is based on the hyperfinite sums of microsimplices. Microsimplices are abstract ordered simplices whose vertices are infinitely close in the sense of nonstandard topology. McCord homology can be seen as a nonstandard analogue of Vietoris homology theory. Garavaglia proved that McCord homology agrees with Vietoris homology for all compact spaces.

  In the recent paper, we introduced a McCord-type homology theory of uniform spaces, provisionally called μ-homology. μ-homology is the nonstandard analogue of uniform Vietoris homology. It is easy to see that μ-homology is equivalent to McCord homology for all compact uniform spaces. This equivalence can be extended to all precompact uniform spaces. To see this, we will introduce the notion of S-homotopy, a nonstandard homotopy equivalence, and will show that every uniform space is an S-deformation retract of its completion.

• Kazushige Terui (RIMS, Kyoto University) Inductive vs. impredicative: a lambda-calculus perspective. 11:00-12:00, 7 Jul, 2016 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract

  I will informally discuss the following topics based on my recent paper (see below):

  • From proof theory (ordinal analysis) to lambda calculus
  • Inductive vs. impredicative fixed points
  • Inductive data types and parameter-free polymorphic types
  • Inductive proofs of strong normalization
  • The Omega rule

  Ryota Akiyoshi and Kazushige Terui. Strong normalization for the parameter-free polymorphic lambda calculus based on the Omega-rule. Proceedings of FSCD'16, 2016.

  Following (Aehlig 08), we consider a hierarchy F^p = {F^p_n}_{n: Nat} of parameter-free subsystems of System F, where each F^p_n corresponds to ID_n, the theory of n-times iterated inductive definitions. We here present two proofs of strong normalization for F^p_n, which are directly formalizable with inductive definitions. The first one, based on the Joachimski-Matthes method, can be fully formalized in ID_{n+1}. This provides a tight upper bound on the complexity of the normalization theorem for System F^p_n. The second one, based on the Goedel-Tait method, can be locally formalized in ID_n. This provides a direct proof to the known result that the representable functions in F^p_n are provably total in ID_n. In both cases, Buchholz' Omega-rule plays a central role.

• 西村進（京都大学理学部数学教室） Carrier Complex: A Poset Topology for Finding Distributed Protocols. 11:00-12:30, 30 June 2016 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract

  We study the problem of finding a wait-free protocol for read-write shared memory distributed systems that meets a given topological specification of colored distributed task. Due to the asynchronous computability theorem by Herlihy and Shavit, this amounts to finding a pair of a subdivision on the input complex and a chromatic simplicial map onto the output complex, but it is an undecidable problem.

  Though there can be no perfect solution to the problem, we claim that there is a partial solution. Given a carrier map as a task specification, we first set up a variant of a well-known poset topology, called the carrier complex, which is a simplicial complex obtained by a combinatorial construction on the carrier map. The solution is then reached by finding an appropriate sequence of simplicial collapses that deforms the input complex embedded as a subcomplex within the carrier complex. Notice that this method only serves as a partial solution to the problem, as it may not be able to find a suitable deformation for some task specifications that indeed have corresponding protocols.

  To put the above method to work for concrete instances of tasks in practice, we have to find a reasonably efficient algorithm. We show that this algorithmic difficulty is partly remedied by a combination of a few combinatorial algorithms for hypergraphs and hyperforests. The complexity bound of the algorithm is polynomial when the number of processes is fixed, but the constant factor rapidly increases for a larger number of processes. Based on a preliminary experiment on a prototype implementation, we report that the algorithm is expected to work in practice for a sufficiently small number of processes (up to 4, namely).

• Nicolas Wu (University of Bristol) Monad Transformers and Modular Algebraic Effects: What Binds Them Together . 11:00-12:30, 29 June 2016 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract

  Monads and algebraic effects are two alternative approaches for expressing purely functional side-effects. While the two approaches have been well-studied, there is still much confusion about their relative merits and expressiveness, especially when it comes to their comparative modularity. This talk clarifies the connection between the two approaches.

  In this talk we introduce the notion of modular algebraic effects, and show how these correspond to a specific class of monad transformers. In particular, we show that every modular algebraic effect gives rise to a monad transformer.

• 浦本武雄（京都大学数理解析研究所） On a reformulation of Eilenberg's variety theory. 11:00-12:30, 23 June 2016 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract

  Eilenberg's variety theory concerns a systematic classification of regular languages, finite monoids, and deterministic finite automata (DFAs). In this theory Eilenberg's variety theorem is a fundamental result, which claims a bijective correspondence between

  1. varieties of regular languages and
  2. pseudo-varieties of finite monoids.

  By the recent work of Gehrke et al. and Rhodes et al., this theorem was reformulated in the light of Stone's duality theorem. On one level this insight promoted a unification of several variants of Eilenberg's variety theorem and a generalization of them, as recently pursued by Adamek et al., Chen et al., and Bojanczyk. On another level, however, this reformulation of Eilenberg's variety theorem is also related to the research line on profinite monoids that has been developed in this field since the late 1980s as a research topic of independent interest. Our work concerns the latter in particular. In this relation, we introduce and study the class of semi-galois categories--- an extension of galois categories; and develop a particularly fundamental theory concerning semi-galois categories and Eilenberg's variety theory: that is,

  1. a duality theorem between profinite monoids and semi-galois categories;
  2. a duality-based yet another proof of two classical Eilenberg-type variety theorems due to Straubing and Chaubard et al.; and
  3. a Galois-type classification of closed subgroups of profinite monoids in terms of finite discrete cofibrations over semi-galois categories.

• 上村太一（京都大学数理解析研究所） Fibred Fibration Categories. 11:00-12:30, 16 June 2016 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract

  We show that, for a fibred category whose base category is a type-theoretic fibration category, fiberwise and total structures of type-theoretic fibration categories coincide. This gives the notion of fibred type-theoretic fibration categories which includes Shulman's inverse diagrams. Fibred type-theoretic fibration categories give categorical foundation of logical relations for identity types.

• Bakhadyr Khoussainov (University of Auckland) Open questions in the theory of automatic structures. 11:00-12:30, 7 June 2016 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract (in Japanese)

  In this talk, we introduce the notion of automatic structure (defined by the speaker and Nerode). Informally, these are infinite algebraic structures (such as graphs, trees, groups, linear orders) that can be presented by automata. We present many examples, several basic results, formulate and discuss some open questions in the area.

• 滝坂透（京都大学数理解析研究所） On coalgebraic characterization of algorithmic randomness. 11:00-12:30, 2 June 2016 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract (in Japanese)

  Martin-Lof randomness is the most frequently used notion of algorithmic randomness, and has several equivalent characterizations: via Martin-Lof tests, martingales, and Kolmogorov complexity.

  In this paper we define these notions coalgebraically. We also show that under our formulation the essential part of the existing proof of equivalence can be seen as the construction of certain Kleisli backward simulations.

• 長谷川真人（京都大学数理解析研究所） プログラム意味論・テンソル圏・量子トポロジー 11:00-12:30, 26 May 2016 Rm 478, Research Building 2, Main Campus, Kyoto University (next to the CS room)(map) Abstract

  プログラミング言語の意味論（プログラム意味論）と位相幾何学における 量子トポロジーの関係について、圏論、特にテンソル圏（モノイダル圏） 及びそのグラフィカルな表現（ストリング図式、ペンローズ図式）を用い ながら紹介します。なかでも、意味論と不変量の比較・融合を中心に話し たいと考えています。

  時間が許せば、「プログラミング言語の研究における圏論の役割・意義 とは何か？」「表示的意味論に未来はあるのか？」というような、切実？ な問題についても論じたいと思います。 （予備知識を仮定しない、入門的・俯瞰的な話です。）

• 片岡俊基(東京大学) Categorical Nonstandard Analysis 11:00-12:30, 28 April 2016 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  超準解析は無限小を元としてもつ実数のモデルを利用する解析であり，その基礎付け にはモデルのultraproductが用いられる。直観主義論理の場合にもMoerdijkにより自 然数（Peano算術）の超準モデルが構成された。ここではultrafilterを1つ選ぶので はなく，filterの圏を用いた構成を行う。その構成においてPalmgrenにより従来の超 準解析と同様に追加の公理を満たすことが示され，直観主義超準解析の基礎が完成し たが，圏論的な理解はButzにより与えられた。すなわち，coherent categoryのfree meet-compl etion（と，coherent categoryのtoposへの埋め込み）がfilter constructionだった。

  圏の対象とその上のfilterの対を対象にもつ圏は2通り知られており一方がnaiveに 射を定義し，他方の定義では上記のようにcompletionとなる。実は，subobject fibrationのfiberwise completionのtotal categoryが前者そのfibrationを subobject fibrationに埋め込む先のbase categoryが後者である。

• 由水輝(東京大学) Multitoken Geometry of Interaction in Concurrent Computation
  (Joint work with Ugo Dal Lago and Ryo Tanaka) 11:00-12:30, 28 April 2016 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  The Geometry of Interaction (GoI) is originally semantics for linear logic proofs and has been found as a useful framework to give a denotational semantics of programming languages. One of its representation is so-called token machine semantics [Danos & Regnier, LICS 1993], in which a single token circulates over a given proof (and thus over a program via Curry-Howard isomorphism) to compute the essential paths on it. The token machine semantics has successfully been exploited as a basis of concrete implementations of compilers, such as [Mackie, POPL 1990] and [Ghica, Smith, & Singh, ICFP 2011]. However, the singleness of the token makes it hard to capture a computational concept, namely synchronization. Thus the (single)token machines cannot naively capture computational paradigms such as quantum computation and concurrent computation in which synchronization is essential.

  Recently, we extended the token machine to a setting allowing more than one token circulating at the same time (multitoken machines), and accommodated synchronization in this setting. The obtained semantics is found to be useful to interpret quantum computation [Dal Lago, Faggian, Hasuo, & Y., CSL-LICS 2014] as well as distinction of call-by-name and call-by-value strategies in classical computation [Dal Lago, Faggian, Valiron, & Y., LICS 2015]. We give a brief introduction to this multitoken machine semantics, and then give a work-in-progress attempt to expand the results so far to concurrent computation.

  We set the first goal on giving such a semantics to multiport interaction nets that was proposed originally in [Alexiev, Ph.D. thesis, 1999] and later in [Mazza, Ph.D. thesis 2005].

  This is joint work with Ugo Dal Lago (Universita di Bologna) and Ryo Tanaka (The University of Tokyo).

• 佐藤哲也（京都大学数理解析研究所） Approximate Relational Hoare Logic for Continuous Random Samplings 11:00-12:00, 21 April 2016 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  Approximate relational Hoare logic (apRHL) is a logic for formal veri cation of the differential privacy ofdatabases written in the programming language pWHILE. Strictly speaking, however, this logic deals only with discrete random samplings. In this paper, we de ne the graded relational lifting of the subprobabilistic variant of Giry monad, which described differential privacy. We extend the logic apRHL with this graded lifting to deal with continuous random samplings. We give a generic method to give proof rules of apRHL for continuous random samplings.

• 上村太一（京都大学数理解析研究所） Fibred Fibration Categories 11:00-12:00, 21 January 2016 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  近年, ホモトピー論と依存型理論の類似点が指摘されている. Homotopy Type Theory は, Martin-Löf の依存型システムの拡張の一つで, 抽象ホモトピー論の言語として使えると期待される. 型理論をベースにしているので, コンピュータを使った形式的証明との相性が良いという点からも注目されている.

  Homotopy Type Theory がホモトピー論の言語であるためには, 適切な意味論を与える必要がある. Shulman は, 依存型システムの圏論的意味論として type-theoretic fibration category (TTFC) を導入し, ある種のモデル圏が TTFC であることを示した.

  一方, 型理論の解析においては fibred category がしばしば使われる. TTFC 上の fibred category を考えれば, それは Homotopy Type Theory の解析ツールを与えることになる.

  本論文では base category が TTFC であるような fibred category について, 各 fiber ごとの TTFC の構造を束ねて total category の TTFC の構造を作ることを考える.

• Tarmo Uustalu (Institute of Cybernetics, Tallinn) From stateful to stackful computation (Joint work with Danel Ahman) 11:00-12:00, 14 January 2016 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  We analyze a number of notions of effectful computation, accounting for computation with a stack at different degrees of intensionality. We demonstrate how all of these notions of computation can be modelled with both monads and Lawvere theories, obtained in a systematic way from modularity tools like distributive laws. We also show how stateful runners for each type of computations are given by coalgebras of the corresponding comonads.

  This is joint work with Danel Ahman, University of Edinburgh.

• Masahiko Sato (Professor Emeritus, Kyoto University) Proof Theory of the $\lambda$-calculus. 11:00-12:00, 17 December 2015 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  By tradition, $\lambda$-terms are defined by means of $\lambda$-abstraction and application from variables. In such an approach, one cannot define the set of closed $\lambda$-terms (or, combinators) directly without using variables.

  In this talk, we give a simple inductive definition of the datatype of closed $\lambda$-terms without using variables, and develop proof theory of $\lambda$-calculus on this datatype. We will prove the pushout property for the category of strongly equivalent reductions (see Excercise 12.4.4 of "The Lambda Calculus" by Barendregt) in this framework.

• Marco Gaboardi (University of Dundee) Verifying Differentially Private Bayesian Inference. 11:45-12:30, 15 October, 2015 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  Differential privacy is a promising approach to the privacy-preserving release of data: it offers a strong guaranteed bound on the increase in harm that a user incurs as a result of participating in a differentially private data analysis, even under worst-case assumptions. A standard way to ensure differential privacy is by adding some statistical noise to the result of a data analysis and several mechanisms have been designed to ensure differential privacy and achieve at the same time a good accuracy.

  Most of the tools designed so far for verifying differential privacy are successful in proving programs differentially private when they use standard mechanisms. However, they offer limited support for reasoning about differential privacy in presence of explicit conditional distributions as in the case of Bayesian Inference.

  To overcome this situation we propose a system where we can reason about differential privacy and bayesian inference. In this system, bayesian inference is expressed in terms of observations and using an inference engine while differential privacy can be proved by using a type system based on the notion of relational higher-order refinement types. Verified programs can be then executed using the Infer.net framework.

• Stephen Chong (Harvard University) Cryptographic Enforcement of Language-Based Erasure.
  (Joint work with Aslan Askarov, Scott Moore, and Christos Dimoulas) 11:00-11:45, 30 October, 2015 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  Information erasure is a formal security requirement that stipulates when sensitive data must be removed from computer systems. In a system that correctly enforces erasure requirements, an attacker who observes the system after sensitive data is required to have been erased cannot deduce anything about the data. Practical obstacles to enforcing information erasure include:

  1. correctly determining which data requires erasure; and
  2. reliably deleting potentially large volumes of data, despite untrustworthy storage services.

  I present a novel formalization of language-based information erasure that supports cryptographic enforcement of erasure requirements: sensitive data is encrypted before storage, and upon erasure, only a relatively small set of decryption keys needs to be deleted. This cryptographic technique has been used by a number of systems that implement data deletion to allow the use of untrustworthy storage services. However, these systems provide no support to correctly determine which data requires erasure, nor have the formal semantic properties of these systems been explained or proven to hold. We address these shortcomings. Specifically, we study a programming language extended with primitives for public-key cryptography, and demonstrate how information-flow control mechanisms can automatically track data that requires erasure and provably enforce erasure requirements even when programs employ cryptographic techniques for erasure.

  This is joint work with Aslan Askarov, Scott Moore, and Christos Dimoulas, and was presented at the 28th IEEE Computer Security Foundations Symposium in July 2015.

• Petr Cintula (The Czech Academy of Sciences) Logic and mathematics with lattice-valued predicates. 11:00-12:00, 29 October, 2015 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  Classical predicate logic interprets n-ary predicates as mappings from the n-th power of a given domain into the two-valued boolean algebra 2. The idea of replacing 2 by a more general structure is very natural and was shown to lead to a very interesting mathematics: prime examples are the boolean-valued or Heyting-valued models of set theory (or even more general models proposed by Takeuti & Titani (1992), Titani (1999), and Hajek & Hanikova (2001)).

  In the first part of the talk we present a framework for the study of logics where predicates can take values in a lattice (with additional operators) from a given class satisfying certain minimal conditions (our framework covers previous approaches of Rasiowa & Sikorski (1963), Horn (1969), Rasiowa (1974), Hajek (1998), and others). For each such logic we first describe its `propositional' part and then use it to give an axiomatization of the full first-order logic.

  The second part of the talk shows that the proposed logical formalism is rich enough to support non-trivial mathematical theories. We illustrate it by proving `graded' variant of the well-know relation between equivalences and partitions. The goal of the example is to illustrate the contrast between very general semantical interpretation of the proven fact and its almost classical proof.

• 本浦 庄太(京都大学数理解析研究所) A General Framework for Modal Correspondence in Dynamic Epistemic Logic. 11:00-12:00, 15 October, 2015 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  A dynamic epistemic logic (DEL) is a logic for reasoning about knowledge change or belief revision. In this talk, we first introduce a well-known and well-studied DEL, public announcement logic (PAL). Taking PAL as a leading example, we then talk about our results. We propose a generic framework to study a wide variety of DELs. This framework can be used to specify the interaction between properties of knowledge change and several axioms.

  (This talk is an rehearsal for an international conference, LORI, held at the end of the month.)

• Matthew de Brecht (情報通信研究機構・脳情報通信融合研究センター) Towards a descriptive set theory for QCB spaces. 11:00-12:00, 25 June, 2015 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  QCB spaces (quotients of countably based spaces) are a convenient cartesian closed category of topological spaces with important applications in computable analysis and for modeling the semantics of programming languages.

  However, they generally fail to be countably based and have very complicated topologies, which so far has been a major obstacle for obtaining a deep understanding of these spaces.

  In this talk, I will present recent joint work with M. Schroeder and V. Selivanov concerning a classification of QCB0 spaces according to the descriptive complexity of defining a basis for their topologies.

  Our approach provides useful tools for analyzing when one QCB space can be embedded into another, and has deep connections with the projective hierarchy from descriptive set theory. We will present some applications concerning the existence of universal QCB-spaces, as well as some results on the Kleene-Kreisel continuous functionals.

• 松本 慧(京都大学数理解析研究所) Coherence Spaces for Computable Analysis (Joint work with Kazushige Terui) 11:00-12:00, 4 June, 2015 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  There have been two mainstream approaches in computable analysis: the type-two theory of effectivity (TTE) and the domain theory. In this talk, we propose a variant of the second approach based on coherence spaces, which are a drastic simplification of Berry's stable domains.

  We import various concepts from TTE such as admissibility, and provide admissible representations for various spaces (eg. for the real line). This allows us to represent, for instance, a real continuous function by a stable map.

  A natural question is then what linear maps correspond to in terms of analysis. Our answer, although partial, seems a bit surprising: they correspond to uniformly continuous functions, when a specific representation for the real line is chosen. This leads to an internal expression of Heine's theorem (every continuous function on a closed interval of the real line is uniformly continuous) as the existence of a certain stable map from a stable function space to a linear function space.

• 浦本 武雄(京都大学数理解析研究所) 副有限monoidの有限表現の圏の公理的特徴付けと，その応用について 11:00-12:00, 28 May, 2015 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  正規言語のvarietyへの所属問題との関連で，副有限monoidの構造論が近年発展している．本発表では，その副有限monoidの構造論に，ガロア圏的アプローチを導入することについて話す．

  まず正規言語のvarietyとは，正規言語の族Vであって，ブール演算，Brzozowski微分，および言語の準同型による逆像をとる操作で閉じているものを言う．与えられた正規言語LがVに属すか否かの決定問題は「正規言語の所属問題(membership problem)」といい，Buchiの単項二階算術などとの関連で古くから研究されてきた．

  興味深いのはEilenbergの定理により，正規言語のvariety Vへの所属問題がその「ストーン双対」である有限monoidのvariety V'の所属問題に帰着されることである．そして，もしV'が「計算可能で有限な生成等式」で定義されていると分かれば，結果的に元の正規言語族Vの所属問題を決定できる．古典的には，この生成等式の発見は，V'を構成する有限monoidのイデアルの分類等により達成されてきた．

  Almeidaらの研究が示しているように，有限monoidのvariety V'への所属問題は，V'の元の逆極限である副有限monoidの構造論に帰着される場合がある．近年副有限monoidの構造論に関心が集まっているのは，このような経緯による．

  この関連で本発表では，副有限monoidの有限表現の圏が，ガロア圏の場合と同じく公理的に特徴付けられることの証明（概要）を紹介し，副有限monoidの構造論との関連で，なぜそんな特徴付けを与えたかの動機を話す．

• Kazuto Yoshimura (Japan Advanced Institute of Science and Technology) A brief introduction to the theory of the Weihrauch lattice 11:00-12:00, 23 Apr, 2015 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  The Weihrauch lattice and its underlying reducibility notion, Weihrauch reducibility, was introduced in 1980s as fundamental concepts for investigating the discontinuities of functions. However it is only recently when the deep analysis of the Weihrauch lattice started, being influenced by the project of constructive reverse mathematics. In this talk, we aim to present a brief review on the theory of the Weihrauch lattice from both historical and technical perspectives, and try to point out the importance of the structure for computable analysis, constructive mathematics and computer science respectively.

• 勝股 審也(京都大学数理解析研究所) Codensity Liftings of Monads (Joint work with Tetsuya Sato) 11:00-12:00, 16 Apr, 2015 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  We introduce a method to lift monads on the base category of a fibration to its total category using codensity monads. This method, called codensity lifting, is applicable to various fibrations which were not supported by the categorical TT-lifting. After introducing the codensity lifting, we illustrate some examples of codensity liftings of monads along the fibrations from the category of preorders, topological spaces and extended psuedometric spaces to the category of sets, and also the fibration from the category of binary relations between measurable spaces. We next study the liftings of algebraic operations to the codensity-lifted monads. We also give a characterisation of the class of liftings (along posetal fibrations with fibred small limits) as a limit of a certain large diagram.

• Gergei Bana(INRIA Paris-Rocquencourt) Formal Verification of Complexity-Theoretic Properties of Security Protocols 11:00-12:00, 26 Mar, 2015 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  Rigorous modeling of attackers to security protocols, and hence the prospect of proving the security of protocols has been developed from the 1980’s in two directions. One focused on automated proving and accordingly modeled protocol execution and attackers with a set of symbolic operations on symbolic terms, treating cryptographic primitives such as encryption as black-box operations (Dolev-Yao approach). The other took a complexity-theoretic approach, modeled protocol execution and attackers as probabilistic polynomial-time algorithms with the aim of deriving protocol security from hardness assumptions such as the DDH assumption (computational approach). While the first technique is convenient for automation and is effective in finding attacks, there is little guarantee that if there is no Dolev-Yao attack, then there is no real-life attack either. Computational approach approximates real life far closer, but is not convenient for automation, proving by hand is too laborious and error prone. From the beginning of the 2000’s there have been numerous research directions trying to unify the two approaches and provide automated verification of computational properties, with variable success. In this talk we briefly review the history of the unification process, the failed attempts, the currently available tools, and we give a more detailed account of our approach with Hubert Comon-Lundh of ENS Cachan and Mitsuhiro Okada of Keio University, which we call “computationally complete symbolic attacker”.

• Maria Emilia Maietti(University of Padova) Why developing mathematics in a two-level foundation 15:30-17:30, 13 Mar, 2015 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  We provide motivations for developing mathematics in a two-level formal system following the ideas put forward in joint work with G. Sambin in [MS05].

  There we introduced the notion of two-level system to found constructive mathematics but it turned out that the same notion can be accomodated to develop mathematics in general with computer-aided formalization of its proofs.

  A main motivating example of such foundations is the Minimalist Foundation for constructive mathematics which was ideated in [MS05] and completed into two levels in [M09]. Its peculiarity is that it is compatible with most relevant constructive and classical foundations at the "right level". Another perculiarity is that its design makes use of different languages: mostly that of type theory, but also that of category theory and axiomatic set theory.

  [MS05] M.E. Maietti and G. Sambin "Toward a minimalist foundation for constructive mathematics" in L. Crosilla and P. Schuster eds., ''From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics", Oxford University Press, 2005
  [M09] M.E. Maietti "A minimalist two-level foundation for constructive mathematics" Annals of Pure and Applied Logic 160(2009):319-354
  

• Giovanni Sambin(University of Padova) A new foundation of constructive mathematics 50 years after Bishop's FCA 15:30-17:30, 13 Mar, 2015 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  Bishop's book Foundations of constructive analysis, 1967, briefly CFA, showed that constructive mathematics can be emancipated from the subjective views of its founder Brouwer. That single book started the process turning constructive mathematics into a rich and lively research field and community, as it is today.

  While standing on the shoulders of such giants, after almost fifty years it is our task to see further. Some epochal changes which took place after 1967 provide motivations and support.

  Outside mathematics:

  1. Evolutionary thought has expanded its range of application and is now commonly accepted in science, except in mathematics. The main challenge awaiting us is to pass from a static, transcendent view of mathematics to a dynamic, human one.
  2. The power of computers and other tools has enormously increased. Their active role in mathematical research will certainly also increase. This requires fully detailed formal systems for the foundation of mathematics.
  3. Diffusion of information technology makes our world intensely connected. One feels the need of a framework which allows for a plurality of different world views.

  Moreover, inside mathematics:
  

  1. new branches have been created,
  2. other branches besides analysis have been constructivized, such as algebra and topology.

  The talk will give a preliminary view on a new foundational system inspired by these facts, first introduced in 2005 and later developed by M. E. Maietti and myself and called the Minimalist Foundation, shortly MF.

  Aims of MF include:

  1. to permit the development of constructive mathematics, including topology, in agreement with a dynamic view (different levels of abstractions, real and ideal entities,...),
  2. to provide a framework in which virtually all foundations of mathematics can be expressed by adding some assumptions (hence the adjective minimalist) and hence in particular a good setting for reverse mathematics,
  3. to allow formalization of mathematics in a computer language,
  4. to express the computational content of mathematics.

  More specifically MF keeps: 1. an effective notion of set different from an ideal notion of collection 2. the notions of operation (with instructions) distinct from that of function (without instructions), 3. a positive notion of existence

  We wish to know that MF is consistent by a proof, not by faith or feelings. One can prove much more than consistency for MF, namely a normalization theorem, a realizability interpretation, implementation in a proof-assistant. We conclude the talk by showing that one needs a theory with two levels of abstraction, thus providing a good introduction to Maietti's talk.

• Adam Chlipala(Massachusetts Institute of Technology) Ur/Web: A Simple Model for Programming the Web 16:30-17:30, 1 Dec, 2014 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  Web applications are built on top of a ramshackle technology platform designed without consideration for classic software-engineering ideas like modularity. Ur/Web is a programming language that hides the cruft behind the sorts of nice abstractions that functional programmers like. The language design is inspired by not just Haskell and ML but also dependently typed languages like Coq and Agda. The open-source implementation is decently practical, powering several production web sites (including at least one profitable business) and scoring well in third-party performance benchmarks.

  I will start off with a few slides introducing the basic Ur/Web programming model, but I want to spend most of the time on a live-coding demo. We will build up several versions of a simple chat application starting (almost) from scratch. I encourage the audience to suggest coding variations, intentional errors that we hope the compiler catches, etc.!

  The main features I want to introduce are strongly typed embedded HTML and SQL code; the functional-reactive GUI system; remote procedure calls; and typed message-passing channels from server to client. Cross-cutting themes include novel encapsulation features and a simple concurrency model. This talk will draw on material from my upcoming POPL 2015 paper with the same name.

• 勝股　審也(京都大学数理解析研究所) Parametric Effect Monads and Semantics of Effect Systems 11:00-12:00, 4 Sep, 2014 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  We study fundamental properties of a generalisation of monad called parametric effect monad, and apply it to the interpretation of general effect systems whose effects have sequential composition operators. We show that parametric effect monads admit analogues of the structures and concepts that exist for monads, such as Kleisli triples, the state monad and the continuation monad, Plotkin and Power's algebraic operations, and the categorical ┬┬-lifting. We also show a systematic method to generate both effects and a parametric effect monad from a monad morphism. Finally, we introduce two effect systems with explicit and implicit subeffecting, and discuss their denotational semantics and the soundness of effect systems.

• 西村　進(京都大学数学教室) 公平な並列実行のためのゲーム意味論 11:00-12:00, 4 Sep, 2014 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) 概要

  Algol風の並列プログラミング言語に対して，その公平な並列実行のゲー ム意味論を提案する．従来のゲーム意味論では，可能なゲームの進行を規 定する安全性(safety)のみ表現することが可能であり，公平性のような活 性(liveness)を規定する術を持ち合わせていなかった．本稿では，先行研 究で提案したwait-notifyゲームを発展させ，非決定性を誘導する可能性 のある計算資源一般へのアクセスをゲーム列の中に明示する．これによっ て，プログラムは非決定性の度合いが特定のゲーム手の出現数によって有 界に制限されるWN有界戦略となることが示される．WN有界戦略と公平なス ケジュールに相当する戦略の合成により，外延的ゲーム意味論を導出し， これが公平な並列実行の操作的意味論に関して完全抽象であることを示す．

• 浦本　武雄(京都大学数学教室) On an algebraic method of deciding logical properties of programs 11:00-12:00, 1 Sep, 2014 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) 概要

  Abstract: 正規言語によるKAT termのinterpretation Wを通して、regular program (を少し弱めたKAT term) p に対して、有限の大きさのKleene algebra with tests K(p) を対応させることができる。KAT termの制限で ある正規表現 r に対しては、syntactic monoid M(r) 或は syntactic semiring S(r)を対応させ、M(r) および S(r) の代数的性 質(pseudo-identityを満たすか否か)で r の組合せ的性質を特徴付けるこ とで、r の組合せ的性質の決定可能性を証明できた。まったく同様に、 KAT term p に対し、有限のKleene algebra with tests K(p)を対応させ、 その代数的性質で、p の組合せ的性質を論じることが勿論できる。ここで さらに重要なのは、K(p)が単にsemiring ではなく、Kleene algebra with tests であることから、単にpseudo-identity(代数的性質)を満たす かどうかだけでなく、K(p) がmodal formulaを満たすかを自然に定義する ことができると言う点である。本発表では、「与えられたregular program p が``observationally deterministic''であるかどうか」とい う性質が、「K(p)がある種のmodal formulaを満たすかどうか」で特徴付 けられることを示す。結果的に、元の「pがobservationally deterministicかどうか」という問題が決定可能であることが従う。

  この決定可能性は、しかしながら、PDL (propositional dynamic logic) の決定可能性を使っても証明できるので、この決定可能性自体は特に新し いものではない。そこで本発表では、K(p)を使った上記の方法と、PDLの 決定可能性を使った方法と、どちらが適応範囲が広いかについての予想に ついても言及する。簡単に言えば、PDLでは基本的に、プログラム p の 「実行前後の性質」（pを実行する前 ... なら、実行後は ...など）だけ を表せるのに対して、K(p)はプログラム p の「実行途中の性質」（pの実 行中に、決して命令qを呼び出すことはないなど）も表せるということで ある。本発表では、「K(p)を経由した方法の方が、PDLを使った方法より 決定出来る問題のクラスが広い」ということを定式化した予想（願望）に ついても話す。

• 山本 健太郎(京都大学数理解析研究所) On the computational power of algorithmically random machine constants in Blum-Shub-Smale machines (Joint work with Akitoshi Kawamura) 11:00-12:00, 29 May, 2014 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  A Blum-Shub-Smale (BSS) machine over R, which can operate on elements of R in a unit time, is one of the models for the theory of computation over real numbers. An interesting problem regarding BSS machines is to determine the computational power of BSS machines relative to other computational models.

  Allender, Burgisser, Kjeldgaard-Pedersen and Miltersen [1] related BSS ma- chines with ordinary Turing machines and straight-line programs (SLPs), an algebraic model of computation perused in algebraic complexity theory. To see their work in detail, let us introduce a few notations. Let L0 denote the discrete decision problem of deciding whether a given 0-variate SLP (that uses 0 and 1 as constants) represents a positive number. Also, for a finite set S ⊂ R, let BP(PS ) denote the class of discrete decision problems solved by polynomial- R time BSS machines that may use only elements of S as machine constants, i. e., the real numbers that the machine may access when performing operations on R. The union of BP(PS ) over all finite sets S ⊂ R is denoted BP(PR ). It is R easily seen that PL0 /poly ⊂ BP(PR ); Allender et al. conjectured that, in fact, PL0 /poly = BP(PR ).

  As a step towards proving the conjecture, they introduced the notion of a real number α being approximable, which means that either

  1. α is algebraic, or
  2. α is transcendental and there exists a family of 0-variate SLPs (Γn )n∈ω such that |Γn | = nO(1) and for every n there is no univariate SLP of length at most n such that the polynomial represented by it has a real root between α and the real number represented by Γn . {α}

  They showed that PL0 /poly ⊃ BP(PR ) if α ∈ R is approximable, and that almost every real number is approximable. In addition, they proved that the values of elementary functions at rationals are approximable.

  A natural question to ask next is whether or not there exists a non- approximable transcendental number of higher complexity, e. g., among non- computable reals. In this light, we investigated the approximability of algorith- mically random reals, and showed the following. Theorem. Every Schnorr random real is approximable.

  We prove this by effectivizing Allender et al.’s proof that almost every real number is approximable. Specifically, we construct a c. e. null cover of com- putable measure that contains all non-approximable reals in [0, 1], by exploiting the fact that approximating the complex roots of a given polynomial can be done effectively [3].

  In fact, Schonhage’s algorithm [3] approximates the roots efficiently, but our proof does not exploit this fact. It remains open whether we can strengthen our claim using notions of resource-bounded randomness. The notion of resource- bounded randomness based on tests has been introduced by Ko [2], and is dependent on two parameters: a complexity class that the null cover belongs to, and an upper bound of the rate at which the amount of information extracted by a null cover from an initial segment of an infinite sequence grows depending on its length. We have been unable to generalize our proof to this setting, because the null cover we constructed does not seem to be even computable, and the rate of information growth is also unclear.

  Acknowledgements. This work is based on part of the bachelor thesis of the second author at the University of Tokyo. The authors thank the advisor Hiroshi Imai and his group members for their support and discussions. The work was supported in part by KAKENHI.

  References
  [1] E. Allender, P. Burgisser, J. Kjeldgaard-Pedersen, and P. B. Miltersen, On the complexity of numerical analysis, SIAM Journal on Computing, 38 (2009), pp. 1987-2006.
  [2] K.-I. Ko, On the notion of infinite pseudorandom sequences, Theoretical Computer Science, 48 (1986), pp. 9-33.
  [3] A. Schonhage, The fundamental theorem of algebra in terms of computa- tional complexity, preliminary report, Mathematisches Institut der Univer- sitat Tubingen, August 1982.

• 佐藤　哲也(京都大学数理解析研究所) Identifying All Preorders on the Subdistribution Monad 11:00-12:00, 29 May, 2014 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  The countable valuation monad, the countable distribution monad, and the countable subdistribution monad are often used in the coalgebraic treatment of discrete probabilistic transition systems. We identify preorders on them using a technique based on the preorder TT-lifting and elementary facts about preorders on real intervals preserved by convex combinations. We show that there are exactly 15, 5, and 41 preorders on the countable valuation monad, the countable distribution monad, and the countable subdistribution monad respectively. We also give concrete definitions of these preorders. By applying Hughes and Jacobs’s construction to some preorder on the countable subdistribution monad, we obtain probabilistic bisimulation between Markov chains ignoring states with deadlocks.

• 柳澤 名由太(京都大学数学教室) Topological Methods in Distributed Computing 11:00-12:00, 8 May, 2014 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) 概要

  位相幾何の分散コンピューティングへの応用について解説する．分散コン ピューティングの基礎的な事項，位相幾何的な道具立ての説明から始め， immediate snapshot modelにおける wait-free computability theorem を与えることを目標とする．

• 浦本　武雄(Department of Mathematics, Graduate School of Science, Kyoto University) A Modified Completeness Theorem of KAT 11:00-12:00, 17 Apr, 2014 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  This talk is about a completeness theorem of KAT, the equational logic of Kleene algebra with tests, and will be given in English. A completeness theorem of KAT reduces the problem of deciding the equivalence between KAT terms into the problem of deciding the equivalence between regular expressions. This reduction yields the decidability of equivalence between simple while programs. The first theorem of this type was proved by Kozen and Smith in 1997, and has been recognized as the standard completeness theorem of KAT. In this talk, this standard one will be modified, using an idea from the variety theory of regular languages.

• 長谷川　真人(京都大学数理解析研究所) プログラム意味論と量子トポロジー（進捗報告） 11:00-12:00, 10 Apr, 2014 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) 概要

  集合と二項関係の圏Relにおける量子二重化を用いたリボンHopf代数・リ ボン圏の構成をきっかけとして、これまでに、プログラム意味論の文脈で 量子トポロジー（量子群に由来する結び目などの不変量）の知見を応用す る研究を進めてきた。研究の概要とこれまでに得られた成果を紹介すると ともに、今度の発展の可能性について触れたい。

• Shohei Izawa(Tohoku University) べき等縮約を通じて見る代数系の圏 11:00-12:00, 13 Feb, 2014 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) 概要

  代数系のべき等演算による像には、もとの代数系のtermから得られる演算 を導入することで自然に構造（べき等縮約）を入れることができる。より 小さな代数系を得るその操作は自然に関手に拡張されること、および有限 代数系の場合にはもとの代数系が復元できるようなべき等縮約の族の中に は最小のものが存在することから、そのような族を通じて代数系の圏を調 べることができると期待される。本発表では上記の枠組みの概要と関連す る結果を紹介する。

• Professor Emeritus Masahiko Sato Viewing lambda terms through maps (Joint work with Randy Pollack, Helmut Schwichtenberg and Takafumi Sakurai) 11:00-12:00, 14 Nov, 2013 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  In this talk we introduce the notion of map, which is a notation for the set of occurrences of a symbol in a syntactic expression such as a formula or a lambda-term. We use binary trees over 0 and 1 as maps, but some well-formedness conditions are required. We develop a representation of lambda terms using maps. The representation is concrete (inductively definable) and canonical (one representative per lambda-term). We define substitution for our map representation, and prove the representation is in substitution preserving isomorphism with both nominal logic lambda-terms and de~Bruijn nameless terms. These proofs are mechanically checked in Isabelle/HOL and Minlog respectively.

  The map representation has good properties. Substitution does not require adjustment of binding information: neither alpha-conversion of the body being substituted into, nor de Bruijn lifting of the term being implanted. We have a natural proof of the substitution lemma of lambda calculus that requires no fresh names, or index manipulation.

  Using the notion of map we study conventional raw lambda$syntax. E.g. we give, and prove correct, a decision procedure for alpha-equivalence of raw lambda terms that does not require fresh names.

• Paul Blain Levy(University of Birmingham) A call-by-push-value tutorial 13:00-14:40, 11 Oct, 2013 (incl. 10min break) Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  Call-by-push-value is a calculus for computational effects that provides the particles of meaning from which both call-by-value and call-by-name calculi are built. This decomposition appears in a wide variety of semantics: operational, domains, state, continuations, games, possible worlds, etc.

  We first look at semantics of call-by-value and call-by-name, using algebras for a monad, and see how that leads us to call-by-push-value.

  We then look at two examples of call-by-push-value semantics that do not use algebras: state (global ground) and continuations.

  The slides for this tutorial are available at http://www.cs.bham.ac.uk/~pbl/papers/cbpvefftt.pdf

• 佐藤　哲也(京都大学数理解析研究所) Simulations for Discrete Probabilistic Systems via Preorder TT-Liftings 11:00-11:45, 29 Aug, 2013 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  It is known that the subdistribution monad D captures discrete probabilistic branchings in the theory of transition systems. The pointwise ordering of distributions is well-known in many coalgebraic discussions but there might be such other orderings. Preorder TT-lifting is a tool to obtain relational liftings, and it gives preoders on monads and coalgebraic simulations. Thus, we are interested in characterising preorders on D and the corresponding coalgebraic simulations between probabilistic systems.

  In this work, we obtain at least 25 preorders on D which include all partial orders on D. We also investigate TT-liftings of D, and we obtain convenient forms of preorder TT-liftings. In addition, we obtain variants of the probabilistic modal logic given by Larsen and Skou. In other words, we characterize variants of the probabilistic modal logic using simulations via preorder TT-liftings of the monad D

• 西村　進(Department of Mathematics, Graduate School of Science, Kyoto University) A Fully Abstract Game Semantics for Parallelism with Non-Blocking Synchronization (A talk to be presented at CSL'13) 11:00-11:45, 22 Aug, 2013 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  We present a fully abstract game semantics for an Algol-like parallel language with non-blocking synchronization primitive. Elaborating on Harmer's game model for nondeterminism, we develop a game framework appropriate for modeling parallelism. The game is a sophistication of the wait-notify game proposed in a previous work, which makes the signals for thread scheduling explicit with a certain set of extra moves. The extra moves induce a Kleisli category of games, on which we develop a game semantics of the Algol-like parallel language and establish the full abstraction result with a significant use of the non-blocking synchronization operation.

• Kenji Maillard(Ecole Normale Superieure) Looking for the lost Hopf algebras 11:00-12:00, 18 Jul, 2013 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  We investigate the existence of braided variants of classical denotational semantics. For this purpose, we look for quasi-triangular Hopf algebras in two models of linear logic since braided monoidal categories arises as their category of modules. The study of the categories of Conway games and the category of Coherence spaces reveals that this approach may have been too optimistic. We also try to extend results of existence of Hopf algebra in Rel to set-valued relations.

• 長谷川　真人(京都大学数理解析研究所) Traced *-autonomous categories are compact closed (Joint work with Tamas Hajgato) 11:00-12:00, 9 May, 2013 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  For years we have been bothered by a small mistery on categorical models of Linear Logic (*-autonomous categories) and Geometry of Interaction (compact closed categories, typically arising from traced monoidal categories via Int-construction): Is there a proper intermediate structure between *-autonomous categories and compact closed categories, that is, a traced *-autonomous category which is not compact closed? We settle this issue by showing that any traced *-autonomous category is actually compact closed.

• 滝坂　透(京都大学数理解析研究所) On quantum Kolmogorov complexities and their relationships 11:00-12:00, 9 May, 2013 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  In the early 2000s, several definitions of quantum Kolmogorov complexity (QKC) were proposed. QKC is expected to be a useful tool for analyzing quantum states (e.g. quantum entanglement) or to be the foundation of the theory of “quantum randomness”. There are three major definitions of QKC by Vitanyi, Berthiaume et al, and Gacs. Vitanyi and Berthiaume et al. defines QKC based on the notion of a quantum Turing machine, that is, a probabilistic Turing machine which allows amplitudes of a computable complex number, of which transition function can be expressed by a unitary operator. Vitanyi’s QKC (cbit complexity) restricts us to use only classical string as an input, while QKC defined by Berthiaume et al. (qubit complexity) allows an arbitrary qubit string. Gacs approaches QKC by defining a universal semi-density matrix, a quantum analogue of a universal semimeasure. Though a decade has passed since these suggestions have been made, it seems that there is very little progress in this area and a number of elementary facts are still not investigated. I will recall some facts about them which are already known: relationships between them by Gacs, and fundamental facts about qubit complexity shown by Muller. I will then propose some conjectures now I am working on, which might be named “quantum Levin’s coding theorem”.

• 浦本　武雄(京都大学数学教室) A non-Cartesian extension of Galois categories? 11:00-12:00, 11 Apr, 2013 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  We talk about two Tannaka-style reconstruction theorems, which are non-Cartesian modifications of the reconstruction theorem in the theory of Galois categories. In the search of an appropriate duality for non-deterministic actions of profinite monoids onto finite sets, we found a duality theorem for join semilattices (due to Hofman et al, not me). It seems that the Stone duality is to Galois categories what this duality theorem is to non-Cartesian extension of Galois categories.

• 佐藤　哲也(京都大学数理解析研究所) Preorders on Monads and Coalgebraic Simulations(Joint work with Shin-ya Katsumata) 11:00-12:00, 14 Mar, 2013 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) Abstract

  We study the construction of preorders on $\Set$-monads by the semantic $\top\top$-lifting. We show the universal property of this construction, and characterise the class of preorders on a monad as a limit of a $\Card^{op}$-chain. We apply these theoretical results to identifying preorders on some concrete monads, including the powerset monad, maybe monad, and their composite monad. We also relate the construction of preorders and coalgebraic formulation of simulations.

• Kazushige Terui(京都大学数理解析研究所) Herbrand's theorem via hypercanonical extensions 11:00-12:00, 29 Nov, 2012 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) 概要

  よく知られているエルブランの定理を代数的に捉えたい。そのために古典 論理のみならず、部分構造論理一般について考える。（様相などの単調／ 反単調な演算子を追加してもよい。たとえば直観主義論理、単調様相論理、 線形論理、ファジー論理など）。 Lをそのような命題論理とし、その最小述語拡大をQLとすると、QLについ てエルブランの定理が成り立つための代数的十分条件として、Lに対応す る代数のクラスがコンパクトな完備化について閉じていることが挙げられ る。そのような完備化の代表例はストーン双対性に基づくものであり、そ の一般化は正準拡大（canonical extensions）と呼ばれ広く研究されてい る。しかし部分構造論理の観点から興味深い代数のクラスの多くは、正準 拡大について閉じているかどうか定かではない。そこで本講演では、新た なコンパクト完備化として超正準拡大（hypercanonical extensions）を 導入する。これは非古典論理証明論における「シークエント計算⇒超シー クエント計算」という発想に基づいて正準拡大を一般化したものである。 それによりゲーデル＝ダメット論理、monoidal t-norm logicをはじめと する多くの論理についてエルブランの定理が系統的に成り立つことを示す。 （今年度MLGにおける講演と同内容）

• 浦本　武雄(京都大学数学教室) 淡中双対としての副有限完備化 11:00-12:00, 22 Nov, 2012 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) 概要

  今回の話は主に三部に分けられる。 <1>モノイドのfinite quotientによる通常の副有限完備化は、前回構成し た逆系の極限(短時間で復習する)と一致することを示す。結果的に、前回 話したPippenger, Rhodes-Steinbergの結果が、properに一般化される。 <2>モノイドMの有限Boole表現の圏から有限Boole代数の圏へのforgetful functorの上のtensor preservingな自己自然変換のなす位相モノイド T(M)は、Mの副有限完備化と一致する。この証明に<1>の結果を使う。この T(M)をMの淡中双対(あるいは淡中モノイド)と呼ぶ。 <3>最後に自由モノイドの副有限完備化(=profinite wordのモノイド)が、 自由モノイドの淡中双対と一致することを利用すると、profinite wordを Hoare論理プログラムとして見られるかもしれないという考察に多少時間 をさく。残念ながら現時点までの(上手いプログラム言語を定義する)全て の試みは、どこかでコケることがわかった。従って、この考察は今のとこ ろ非形式的だが、なにかしら厳密に意味付けを与えられると思うので紹介 する。

• Shota Motoura(京都大学数理解析研究所) On the semantic meaning of reduction axioms in Public Announcement Logic 11:00-12:00, 15 Nov, 2012 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) 概要

  前半ではPublic Announcement Logicとreduction axiomsについて話す。 Public Announcement Logicは人間の知識の変化を取り扱うための論理学 である。人間の知識をクリプキモデルによって表現し、知識の変化をクリ プキモデルの変形によって表現する。Public Announcement Logicをはじ めとする類似の論理の公理化では、完全性の証明を容易にする公理化をす ることが一般的に用いられる。そのような公理化で用いられるのが reduction axiomsである。

  後半では修士論文に向けた私自身の研究を発表する。reduction axiomは、 クリプキモデルの変形に関する性質をあらわしてる。本発表ではこのモデ ルの変形の性質をより捕捉するために、一方でPublic Announcement Logicをそれと同値かつ分析しやすい公理系に変形し、他方でモデルの変 形を１つのクリプキモデル内の遷移と捕らえたクリプキモデルを導入する。 その後この両者を用いて、導入したクリプキモデルの性質と各reduction axiomが完全かつ健全な形で対応するを示す。これらの対応の結果を用い て、最後に先のPublic Announcement Logicの完全性について、オリジナ ルな証明とは異なる別証明が可能であることを紹介する。

• 浦本　武雄(京都大学数学教室) 半表現関数環によるモノイドの副有限完備化 11:00-12:00, 1 Nov, 2012 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) 概要

  Hochschild-Mostowは表現関数環を使った表現論の研究を発展させた。そ の中で一つの主題となっているのは、「表現関数環のZariski spectrumに よって、各種の完備化を実現する」という問題である。 Hochschild-Mostowとその後のMostowの研究で、代数群、コンパクト群、 Lie代数やLie環に対して、この種の問題が解決されている。そのどれも複 素数体や実数体、代数閉体などの無限体値の表現関数を使ったものである。 今回の話では、前回話したブール値の表現関数双代数に対して、Zariski spectrumをとると、それがちょうど副有限完備化と一致することを紹介す る。標準的には副有限完備化は、有限群（有限モノイド）のvarietyをとっ て、その中で逆極限をとるという構成で定義されるが、これを表現関数の 言葉で書き換えることができ、その帰結として上記の結果が証明できる。 また証明をよくよく見ると、モノイドでも正しいことがわかった（正確に は一般化できるように副有限完備化の構成を書き換えたということ）。こ の結果は、最近のSteinberg-Rhodes, Almeida (2009?)の、自由モノイド に対する結果の、任意のモノイドへの一般化になっていることもわかる。

• 浦本　武雄(京都大学数学教室) 半群の表現関数 11:00-12:00, 18 Oct, 2012 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) 概要

  kを体とし、Sを半群とする。S上の表現関数とは写像f: S --> kであって、 ある種の有限性条件を満たす物として定義され、群の表現論の基本的な 概念である。今回の話で、kを2値のブール代数に置き換えた表現関数の 離散類似を定義し、Sがwordのなす半群?Sigma^*のとき、言語L ?subseteq ?Sigma^* がregularであることと、その特性関数 ?Sigma^* --> 2が表現関数であることが同値であることを示す。また、体値の表現 関数の成す集合R_k(S)は、双代数の構造を持ち、特にSが群の時はHopf代 数になる。これは余代数の基本定理を証明する際に、有効に使われる双 代数である。同様に2値の表現関数の成す集合R_2(S)はBool代数の圏の双 代数の構造をもち、Sが群の時はHopf代数となることをみる。この構成の 際、Bool代数のテンソル積の構造を決定しなくてはいけないが、多少面 倒な議論で決定出来る。さらに、有限オートマトンの圏は、R_2(S)の余 加群（であってそのunderlying semi-latticeが有限ブール代数である様 な物）の圏と同値となることも示す。最後に、regular languageの既存 のアプローチ(syntactic monoidを使うやつ)との比較と、 R_2(?Sigma^*)の構造を調べることで、Pumping Lemmaが示せるのではな いかとの予想と、その証明のラフな方針について話す。

• 星野 直彦(京都大学数理解析研究所) Step Indexed Realizability Semantics for a Call-by-Value Language Based on Basic Combinatorial Objects 11.00-12.00,21 Jun, 2012 Rm 478, Research Building 2, Main Campus, Kyoto University(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 Rm 478, Research Building 2, Main Campus, Kyoto University(next to the CS room)(map) 概要

  ランダムの概念として最も有名な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 Rm 478, Research Building 2, Main Campus, Kyoto University(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 Rm 478, Research Building 2, Main Campus, Kyoto University(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 Rm 478, Research Building 2, Main Campus, Kyoto University(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 Rm 478, Research Building 2, Main Campus, Kyoto University(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 Rm 478, Research Building 2, Main Campus, Kyoto University(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 Rm 478, Research Building 2, Main Campus, Kyoto University(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 Rm 478, Research Building 2, Main Campus, Kyoto University(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.

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

  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) 概要

  コンピュータソフトウェアは現代社会の縁の下の力持ちです。ソフトウェアの力を借りない日はほとんどないと言っても過言ではありません。私はコンピュータなんて触らないよ、という方でも、実は、携帯電話、自動車、家電、などなど、目に見えないところで知らず知らずソフトウェアの恩恵を受けているはずです。もちろん、企業や役所、公共交通機関などでは、より目につくかたちでソフトウェアが活躍しています。

  それらのソフトウェアには数百万行に及ぶ巨大なものも珍しくありません。そして、その中のほんの小さな不具合が、社会に致命的な影響を与えたという事例は山のようにあります。入り組んだ巨大なソフトウェアを上手に設計し、解析・検証し、さらに改良するためには、どのようにしたらよいのでしょうか？この講演では、数学を武器にしてソフトウェアに立ち向かう研究の、最近の動向についてご紹介します。特に、ソフトウェアを数学的に正確に捉えることと、現代数学が得意とする抽象化の考え方を用いてソフトウェアの本質に迫ることに重点をおいて、数学がコンピュータソフトウェアの研究開発において果たす役割についてお話ししたいと思います。

• 星野 直彦 (京都大学数理解析研究所) 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 ludics 11.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 Zipper 11.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.

• 末永 幸平 （リスボン大学） Fractional Ownerships for Safe Memory Deallocation 11.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 realizability 11.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 Simulation 11.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 atCONCUR 2010.

• 勝股 審也 (京都大学数理解析研究所) Categorical Descriptional Composition 11.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 DILL 11.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 filtration 11.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 languages 10.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 Rel 11.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 language 11.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 chapterhttp://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 inhttp://arxiv.org/abs/0906.4725.

• 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 Fractals 11.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 arepresentation 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 ofinjective 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 Logic 11.00 - 12.00, Thursday 9 July 2009 CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; seedirection) 概要

  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 categories 11.00 - 12.00, Tuesday 16 June 2009 CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; seedirection) 概要

  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 systems 11.00 - 12.00, Tuesday 9 June 2009 CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; seedirection) 概要

  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 spaces 10.00 - 11.00, Tuesday 9 June 2009 CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; seedirection) 概要

  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 state 11.00 - 12.00, Thursday 4 June 2009 CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; seedirection) 概要

  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 completeness 11.00 - 12.00, Thursday 28 May 2009 CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; seedirection) 概要

  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 2009 CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; seedirection) 概要

  カテゴリー論を用いた考察を通じて、

  1. ネットワークの新しい解析方法、
  2. ネットワークモチーフに関する新しい仮説、

  を議論する。有向グラフとして表現されるネットワークは構造のない頂点とその間の矢印からなるため、頂点の機能はそのままでは議論できない。しかし、現実のネットワークでは頂点には機能がある。例えば、遺伝子転写制御のネットワークやニューロンのネットワークなどでは、頂点においては情報処理が行われていると考えられる。情報処理のような頂点における機能を含めた形の表現を考えることができれば、現実のネットワークのより深い理解が得られる可能性がある。ここでは簡単に、頂点における機能も有向グラフで表現する。その際、元のネットワークの矢印に対応した有向グラフも用意する。これは頂点の機能間の関係の仕方を表現する。これらに対してカテゴリー論におけるdistributorを使うと様々な構成ができる。例えば、与えられたネットワークを機能のネットワークへと対応させる変換は、有向グラフの圏からそれ自身への函手となり、右随伴を持つ。この函手を用いた現実のネットワークのデータ解析、及びそれに基づくbi-fanと呼ばれるネットワークモチーフに関する新しい仮説について述べる。

• Aloïs Brunel (ENS Lyon) An introduction to Classical Realizability 11.00 - 12.00, Thu 14 May 2009 CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; seedirection) 概要

  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 theory 11.00 - 12.00, Thu 7 May 2009 CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; seedirection) 概要

  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 Traces 11.00 - 12.00, Thu 9 Apr 2009 CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; seedirection) 概要

  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 Categories 11.00 - 12.00, Fri 3 Apr 2009 CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; seedirection) 概要

  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, byChris Heunen and Bart Jacobs. [arXiv]

• Jun Pang (Univ. Luxembourg) Measuring Voter-controlled Privacy 16.00 - 17.00, Fri 13 Mar 2009 Room 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 Diagrams 11.00 - 12.00, Thu 15 Jan 2009 CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; seedirection) 概要

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

  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 duality 11.00 - 12.00, Thu 27 Nov 2008 CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; seedirection) 概要

  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 Systems 16.00 - 17.00, Wednesday 19 Nov 2008 Room 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 2008 Room 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 2008 CS Laboratory, RIMS, Kyoto University (in the "RIMS Annex" building; seedirection) 概要

  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 Complexity 11.00 - 12.00h, Thursday 16 Oct 2008 Room 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会議室 概要
  ウェブページ

• 香川考司（香川大学工学部） 関数型プログラミング言語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 Garrigue Relaxing 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 Garrigue Hindley-Milner with Local Constraints: Extending Type Inference the Easy Way ２００１年１０月１０日（水）１６：００- 数理解析研究所２０２号室 概要