ALGI-13 Programme

*** Dec. 16 (Joint session with CC-Seminar organized by Prof. Dr. M. Yasugi)***

10:00-10:30 Yohji Akama (Tohoku Univ.) Systems of Typed Limiting Computations The typed limiting computation will be analyzed with the help of category theories to obtain a typed semi-formal system. Then we will discuss the concerning problems. We will be led to Howard's typed lambda-calculus of limiting recursor, and will discuss the upper bound of ordinal numbers Coquand inductively defined. This talk is based on on-going work with Susumu Hayashi and Ken-etsu Fujita. 10:35-11:05 Hajime Ishihara (JAIST) Pointwise and Sequential Continuity in Constructive Analysis We will discuss the relationship between pointwise and sequential continuity in Bishop's constructive mathematics. 11:10-11:40 Izumi Takeuti (Toho Univ.) Computable Structure and Effective Categoricity Hertling defined the notion of effective categoricity and showed that the structure of real number with effective convergence is effectively categorical (MLQ 45-2, '99). He defined the notion with the words of representation. This talk will show another equivalent definition of effective categoricity with the words of computable structure. The aim of this work is to compare the two methods of computable analysis; one is that by representation and the other is by computable structure. 13:30-14:00 Hideki Tsuiki (Kyoto Univ.) Dimension of limits of algebraic domains We show that when D is a Coherent algebraic domain, the dimension of L(D), the set of limits of D, and the height of L(D) are equal. As a consequence, a condition on D for the domain representability of a space X in L(D) is given. 14:10-14:40 Hiroyuki Miyoshi (Kyoto Sangyo Univ.) Mereotopology and Computation 14:50-15:35 Rene Vestergaard (JAIST) Structural Induction and the lambda-Calculus We consider formal provability with structural induction and related proof principles in the lambda-calculus presented with first-order abstract syntax over one-sorted variable names. Surprisingly, informal practice is shown to be a subset of the formal requirements by way of a general proof methodology that we introduce. The results we establish range from the relative renaming-freeness of residual theory over decidability of alpha-equivalence to beta-standardisation. 15:45-16:30 Jamie Gabbay (Univ. of Cambridge) Fraenkel-Mostowski Semantics for Names and Binding We often want to reason about systems with names and binding, for example about syntax such as that of the lambda- or pi-calculus. Yet we encounter apparently technical difficulties doing so because of problems with names and binding such as accidental variable capture, or clash of bound variable names. The usual solution is to prove lemmas allowing us to rename up to alpha-equivalence. However, this is no help when we come to the next piece of work, nor if we need meta-theories such as logics and programming languages for syntax with names and binding. Fraenkel-Mostowski techniques observe that these lemmas are all consequences of a general (first-order) semantic theory of names and binding. Once we understand this theory, we can appeal to it in order to obtain the required lemmas "for free", and we can use the semantics to design general programming and logical tools. *** Dec. 17 *** 9:45-10:45 Hitoshi Ohsaki (AIST) Equational Tree Automata: Towards Automated Verification of Network Protocols Equational tree automata provide a powerful tree language framework that manipulates the congruence closures of tree languages. In the first part of this talk I will summarize the closure properties and decidability results on the extended tree automata. In particular, I will show the (intersection-)emptiness problem for AC-tree automata, which was open in my previous work, is decidable, by the straightforward reduction to the reachability problem for ground AC-term rewriting. The newly obtained results generalize decidability of so-called reachable property problem [Mayr & Rusinowitch, 1999]. In the second part, we discuss the usefulness of this tree automata theory. To be precise, I will explain how equational tree automata can be applied to equational unification problems. We then demonstrate how the network security problem, such as for Diffie-Hellman key exchange algorithm, can be dealt with the equational tree automata theory. This tutorial talk is basically the same talk of ones at RTA 2002 and UNIF2002 in Copenhagen. 11:00-12:00 Hitoshi Ohsaki (AIST) Sequel to the previous talk 13:30-14:30 Alex Simpson (Univ. of Edinburgh) What is a category of domains? Domain theory is usually taken to be the study of complete partial orders, possibly satisfying additional properties (continuity, algebraicity, etc.). However, there are other types of mathematical structure equally suited to modelling computation. Such structures form categories sharing many properties in common with the more familiar categories of domains. In this talk, I shall describe several examples of such structures, and I shall give a survey of work done in the 1990s on "axiomatic domain theory", which studied the characteristic properties of categories of domains in general. 14:45-16:15 Atsushi Shimojima (JAIST), Channel theory as a philosophical experiment, In this short tutorial, I will introduce basic concepts of channel theory (Barwise and Seligman 1997), with an emphasis on philosophical motivations behind them. Specifically, we will see how the theory has been designed to give a general, naturalistic theory of information and thereby that of "representations", where the term broadly refers to symbols, pictures, and physical models in everyday life, as well as such abstract objects as mathematical models. ************************************************* * Workshop Banquet * * 17 December (Tuesday) 18:00- * * at MISORA (approx. 3 min. walk from RIMS) * ************************************************* *** Dec. 18 *** 9:45-10:45 Misao Nagayama (TWCU) Ludics and proof-nets (Part I) 11:00-12:00 Misao Nagayama (TWCU) Ludics and proof-nets (Part II) 13:30-14:00 Kazumasa Honda (Kyushu Univ.) An implementation of a proof system for dependencies for information relations: validation and finding counter-examples. (In Japanese) 14:00-14:30 Hitomi Okuma (Kyushu Univ.) Demonic orders and quasi-totality in Dedekind categories （joint work with Yasuo Kawahara) Relation algebras are suitable for describing semantics of relational programming. In particular demonic composition and demonic orderings will be useful for designing nondeterministic programs. We give definitions of two refinement orderings using quasi-total relations, and provide existence conditions of the supremum and values of supremum and infimum of a set of relations with respect to both refinement orderings. Finally we prove that the demonic composition is monotonic on these orderings, respectively. (This talk will be given in Japanese.) 14:45-15:15 Yasuhide Sawada (Kyoto Univ.) An Explicit Environment Calculus with Subtyping (In Japanese) 15:30-16:30 Satoko Itaya (ATR) A study on an immune network dynamical system model In this study we propose and analysis models of immune networks. Our main aims in this study are to clarify mechanisms for emergence　 of functions and connectivity in immune networks and to reproduce　 phenomena in real immune systems. First, we summarize the immune system of humans, the theory of immune　 networks and various existing models. Moreover, we introduce examples of　application of immune networks theorys to other fields, and describe the　aims　of our study. Next, we investigate the possible steady states in an idiotype network model introduced by Varela et. al. and in two modified models. In all these three models, both chaotic and periodic states exist. Next, we investigate the response of the model immune systems to invasion by antigens. It is found that compared to periodic states, the response time in a chaotic state shows less dependence on antigen type. Moreover, we show that the introduction of thresholds in the immune system model enhances the stability of the network and results in localization of the immune response. Finally, we study connectivity of networks. We found that in the case that a network has fixed strength of connectivity, local coupling results in oscillatory behavior which could be advantageous for dynamic coupling in the network. Further, we find that a system with mutation results in formation of sub-networks, which could be advantageous for stability. *** Dec. 19 *** 9:45-10:15 Masahito Hasegawa (Kyoto Univ.) Coherence of the Double Involution on *-Autonomous Categories (joint work with R. Cockett and R.A.G. Seely) 10:30-12:00 Makoto Kikuchi (Kobe Univ.) An Introduction to Abstract Design Theory Design is one of the most important activities of human reasoning, which is not easy to deal with mathematically. Abstract Design Theory is a mathematical framework for the analysis of design proposed by Kakuda in 1999. The basic idea of the theory is that design in an activity of producing information flow between the realm of our consciousness and the real world. In part, the theory is an application of Channel Theory, a mathematical theory of information flow invented by Barwise and Seligman. The philosophy of Yoshikawa's General Design Theory, in which design is discussed in terms of two topologies defined by functions and attributes of artifacts, plays an important role for the developments of the theory, and some of the arguments in General Design Theory have been justified mathematically by Abstract Design Theory. This talk is an introduction to Abstract Design Theory in which the motivations and the basic part of the mathematical machinery will be presented. It includes also a brief review of Channel Theory and General Design Theory and no background is assumed. 13:30-14:30 Alex Simpson (Univ. of Edinburgh) A convenient category of topological domains In this talk, I'll begin by setting out a list of desirable properties that an ideal category of domains, convenient for applications in the semantics of computation, should possess. No existing category of domains satisfies all the conditions identified. To remedy this, I shall propose a new category of domains, consisting of certain simple topological spaces, that does promise to fulfill all of the requirements. This is work in progress. 14:45-15:15 Satoshi Matsuoka (AIST), Exponential-Free Typed Boehm Theorem (part II), In this talk I discuss typed Boehm theorem on the intuitionistic implicational multiplicative additive fragment of Linear Logic. In the previous ALGI workshop, I only discussed the fragment without additives although type instantiations and contexts include additives. 15:15-15:45 Ryu Hasegawa (Tokyo Univ.) T.B.A. 16:00-16:30 Masaru Shirahata (Keio Univ.), Review of "Geometry of Interaction and linear combinatory algebras", I would like to review S. Abramsky, E. Haghverd and P. Scott, "Geometry of Interaction and linear combinatory algebras", (MSCS, October 2002) which utilizes traced monoidal categories to give an axiomatic framework for Geometry of Interaction. I hope to have a vigorous discussion on this issue with the audience. *** Dec. 20 *** 11:00-12:00 Seminar "Interpreting Set Theory in Toposes (5)" by Alex Simpson (Room 402) [NOTE:Not Part of ALGI]