--- Wed. 14/10 ---

13:30--14:30
Weiermann, A. (Westfaelische Wilhelms-Univ. Muenster)
Sharp bounds for the lengths of reduction sequences in Goedel's T

Break

14:45--15:15
Tatsuya SHIMURA (College of Science and Technology, Nihon Univ.)
A semantics of Kashima's connection calculus for the logic of constant domain

By giving an interpretation for Kashima's method of sequents with connections and using Schuette's method, this talk proves that Kashima's system is cut-free and that it is complete for some subordination frame.

15:15--16:05
Misao Nagayama (Dept. of Mathematics, Tokyo Woman's Christian Univ.),
Mitsuhiro Okada (Dept. of Philosophy, Keio Univ.)
Graph-theoretic characterizations of proof nets in non-commutative linear logics and their computational complexity

This talk presents much simpler correctness criteria with no use of the Danos-Regnier switching condition and proves the corresponding sequentialization theorems for two multiplicative non-commutative Linear Logics, Cyclic Linear Logic and Abrusci's non-commutative Linear Logic. As corollaries to the theorems, we show that typability problems in the Multiplicative non-commutative Linear Logics are in linear time.

Break

16:20--16:50
Osamu Watari(Grad. School of Engineering, Hokkaido Univ.),
Koji Nakatogawa(Grad. School of Engineering, Hokkaido Univ.),
Masaaki Miyakoshi(Fac. of Letters, Hokkaido Univ.)
Multiplicative / Additive Connectives for Deontic Logic

This talk studies how we can introduce multiplicative / additive connectives into deontic logic. It also studies some concrete examples in which it is relevant to distinguish multiplicative from additive.

16:50--17:40
Mamoru Shimoda (Shimonoseki City Univ.)
About fuzzy equivalence relations

The basic concepts of fuzzy sets and fuzzy relations have been shown (by the author) to be most naturally interpreted in the cumulative model of intuitionistic set theory, where the truth value set is a complete Heyting algebra. In this talk similar natural interpretation will be presented about fuzzy equivalence relations and related concepts.

--- Thu. 15/10 ---

9:45--10:45
Takaki Osamu (Kyoto Sangyo Univ.)
On normalizability of natural deduction of arithmetic with inductive definition

This talk defines a reduction for constructive arithmetic TRDB with the axiom TRD, which is recursive definition on primitive recursive well-ordering. And this talk shows strong normalizability of the reduction.

10:15--10:45
Hirai Takaharu (Grad. School of Science and Technology, Kobe Univ.)
On Temporal Linear Logic and Timed Petri Net

In these days, Petri nets have been extended with time. For example, transitions are arranged by the delay in the firing. They are called timed Petri nets. The reachability to a marking from another marking corresponds to the provability of a sequent in linear logic. By introducing discrete time to linear logic, we represent temporal linear logic and state the correspondence to timed Petri net.

10:45--11:15
TANABE, Makoto (Prest21, JST/ASTEM-RI, Kyoto)
Observing Reactive Systems: A Logical Approach using Intuitionistic Modal Logic

A variety of classical modal/temporal logics have been used for specification and verification of reactive systems. In contrast, there are few applications of intuitionistic modal logics to computer science.
In this talk, the possibility and the feasibility of using intuitionistic modal logic (IML) into specification of the observed computations ,as sequences of events, of reactive systems (such as error-loggers and meta control systems) are discussed.
We show that, using IML, subsequences of the ongoing computation which satisfy certain properties can be explicitly mentioned as instances of the properties using IML formulas. It is also shown that double negated formulas can be used to specify the whole computation.

Break

11:30-12:00
WATANABE HIROSHI (Semantics Group, Electrotechnical Laboratory)
An Axiomatics for Categories of Transition Systems as Coalgebras

We consider the categories of transition systems and functinal bisimulations, which is given as a category of coalgebras for finite-powerset functor on Set. This category is complete and cocomplete, and has symmetric monoidal closed structures and a subobject classifier. Most of these properties are implied axiomatically by the structures of both base category and endofunctor. We give examples of symmetric monoidal closed structures on the category of labelled transition systems and an overview of subobject classifier in the category of transition systems.

12:00-12:30
Shinya Sato (Grad. of Science and Technology, Science Univ. of Tokyo),
Toru Sugimoto (Fac. of Science and Technology, Science Univ. of Tokyo)
A concurrent call-by-value lambda evaluator based on computational interpretation of Linear Logic

Corresponding to cut-elimination in Classical Linear Logic, Abramsky proposed a computational system which consists of proof expressions and Linear CHemical Abstract Machine (CHAM). By Girard's embedding of Intuitionistic Logic into Linear Logic, typed lambda calculus is embedded into this system. We show that Linear CHAM can perform reductions of proof expressions which correspond to the call-by-value lambda evaluation. Since reductions of Linear CHAM can be performed in parallel, we can design a concurrent call-by-value lambda evaluator.

Break

13:30--14:30
Wainer, S. S. (Univ. of Leeds)
Proof Theory and Complexity

Break

14:45--15:15
Fujita Ken-etsu (Kyushu Inst. of Technology)
2nd Order Lambda-Mu-Calculus of Call-by-Value

We introduce an explicitly typed lambda-mu-calculus of call-by-value as a short-hand for the complete 2nd order Church-style. Our motivation comes from the observation that in Curry-style polymorphic calculi, control operators such as callcc or mu-operators cannot, in general, treat the left contexts correctly. It is shown that the CPS-translation is sound with respect to lambda 2 (the System F of Girard). As one of by-products, it can be obtained that the 2nd order lambda-mu-calculus of call-by-value has the strong normalization property.

15:15--16:15
Ichiro Ogata (Electrotechnical Lab.)
lambda-mu calculus as cut elimination of LK

Break

16:30--17:00
Yukiyoshi Kameyama (Grad. School of Informatics, Kyoto Univ.)
A simple proof of the strong normalizability of classical catch/throw calculi

We interpret a classical logic version of Nakano's catch/throw calculus and also Sato's classical catch/throw calculus into a variant of Parigot's lambda-mu- calculus. By using this interpretation, we give a simple proof of the strong normalizability of these calculi.

17:00--17:30
Baba Kensuke (Kyushu Univ.), Hirokawa Sachio (Kyushu Univ.),
Fujita Ken-etsu ( Kyushu Inst. of Thechnology)
Parallel calculation on lambda-mu calculus

This talk proves confluence of lambda-mu calculus by regarding a renaming and some steps of structural reductions as one step parallel reduction.

--- Fri. 16/10 ---

9:25--10:05
Kohtaro Tadaki (Grad. School of Science, Hokkaido Univ.)
Kolmogorov complexity and fractal sets

kolmogorov complexity denotes the auxiliary information content which is required for generating a given object by an algorithm.
We represent any point in Euclidean space in base-two notation and consider the rate of information compression by means of Kolmogorov complexity. We show that the maximum value of all such rates of information compression is equal to the Hausdorff dimension for each set in a certain class of self-similar sets which includes familiar fractal sets, Cantor set, Koch curve, Sierpinski gasket, and so on. And also we introduce Omega^D which is a generalization of Chaitin's halting probability Omega. Studying its properties, we show that the Hausdorff dimension of the self-similar set related to the halting problem is equal to 1.

10:05--10:35
KAMO, Hiroyasu (Fac. of Science, Nara Women's Univ.)
Computability of the Hausdorff Metrics on Computable Metric Spaces

It is known that all nonempty compact subsets of a metric space form a metric space with the Hausdorff metric. Weihrauch has defined a "computable metric space" as a metric space with an enumarated dense subset. We will show that all nonempty compact subsets of a computable metric space can form a computable metric space. We will also show some applications.

10:35--11:05
Tsuiki Hideki (Fac. of Integrated Human Studies, Kyoto Univ.)
Real PCF by Gray code

This talk introduces Real PCF by Gray code, and shows that it is equivalent to the original Real PCF.

break

11:20--12:00
Kenji Taguchi (Grad. School of Information Science and Electrical Engineering, Kyushu Univ.),
Hiroyuki Sato (Computer Centre, The Univ. of Tokyo)
A Calculus for Manipulating Cells - The Cell Calculus -

This talk shows the powers of computation of mobile ambients with various capabilities.

12:00--12:30
Makoto Tatsuta (Dept. of Mathematics, Kyoto Univ.)
Uniform Continuity of Graph Model and Partial Function Model

The uniform continuity property MCONT for a partial combinatory algebra with pairing and natural numbers is that there exists a functional which uniformly produces from a type 2 functional its associate in the finite type structure on the algebras. This talk shows that either the the partial function model or the graph model does not have MCONT.

Break

13:30--14:00
Masaru Shirahata
Pier -- a proof interactive editor --

We introduce Pier (Proof Interactive Editor), which is a Java Applet for writing proof trees through graphical user interface. Pier is intended as a handy tool for the research and education in logic. We would also like to compare our motivation for developing Pier with that of automated theorem proving community.

14:00--14:15
Tsuiki Hideki (Fac. of Integrated Human Studies, Kyoto Univ.),
Takeuti Izumi (Grad. School of Informatics, Kyoto Univ.)
Implementation of drawing self-similar sets with network

As an extension of the fundamental theorem in Kawamura's doctral thesis into Gray code, this talk shows demo of a Java applet to draw self-similar sets.

13:30--15:05
Sumitomo Ryosuke (Grad. School of Science and Technology, Kobe Univ.)
An environment assisting proof animation

This talk introduces an system which gives an environment to assist proof animation, and shows some demo of it.

Break

15:20--16:00
Hiroshi Nakano (Dept. Applied Math. and Informatics, Ryukoku Univ.)
A realizability interpretation of self-referential types

It is well known that type definitions with negative self-references introduce a contradiction so called Russell's paradox. We propose a cost conscious typing system and its realizability interpretation which gives a natural semantics to such paradoxical types. We also show that this typing system gives a good axiomatic semantics to fixed point combinators, such as Y, so that we can construct recursive programs using fixed point combinators taking account only of their types.

16:00--16:50
Susumu Hayashi (Fac. of Engineering, Kobe Univ.)
Beeson's q-realizability is useful for program extraction

Beeson introduced a q-realizability interpretation to prove existence property for some constructive formal theory with set notions(IZF, T_0, etc). It used a technique of "doubling variables". Tatsuta introduced "set completion" q-realizability interpretation and showed it could be a substitue of Beeson's for particular formalizations of Feferman's T_0. Then, he claimed that "doubling variable" interpretation is not adequate for program extraction" but his one is. We will show "doubling variables" technique is adequate for program extraction contrary to the claim.