<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
(This text includes Japanese characters.)

********************************************************************************

Subject: [sonoteno 89] Linear Logic Workshop
Date: Thu, 28 Jan 1999 20:33:10 +0900

Workshop on Linear Logic and Applications 
with the Special Intensive Lecture Series by J-Y. Girard.
(Feb 26-27, 1999, Mita-Campus, Keio University, Tokyo, JAPAN)

「線形論理とその応用」ワークショップ及び J-Y. Girard による特別連続講義
のお知らせ(1999年 2月 26日(金)-27日(土))


The following workshop on Linear Logic and its Applications is scheduled.
Free charge for participation.
The call for participations and call for papers follow below.
(A registration form is attached as well as some hotel information.)

線形論理の理論とその応用に関する次のようなワークショップを予定しております．
特に，線形論理及びその情報科学・計算機科学への応用に関する最先端の成果に関
する紹介の講演や、線形論理の予備知識をあまり持たない方，学生の方のための
チュートリアル形式の講演も含みます．
参加は無料・自由ですが，会場の準備のために下の登録をお願い致します．
このメールの最後に登録用様式とホテルの情報があります。


The tentative list of invited talks and tutorial talks.

現在，次のような特別講義やチュートリアルが予定されております．


 - Jean-Yves Girard (CNRS-IML, Marseille, France),
   "Recent Development of Linear Logic",
   Self-contained Four (4) one-hour lectures.

   (特別な予備知識なしに，最新の Girard の理論を紹介する Girard 自身による
   4回連続講義)


- Naoki Kobayashi (Univ of Tokyo, Dept of Computer Science)
  (線形論理のプログラミング理論への応用に関する講演ー詳細は追ってお知らせ
します。)


- Naoki Yonezaki (Tokyo Institute of Technology, Computer Engineering)
  (リアクティブシステムの形式的(論理的)検証に関する講演)


 - Mitsu Okada (Keio University, Dept of Philosophy)
  (線形論理の論理的計算モデルへの応用例の紹介)

 - (Not Confirmed Yet)
    Naoyuki Tamura (Kobe University, System Engineering)にお願い中ですが
    不確定です。 
   (線形論理に基づく種々の存在する論理型プログラム言語の概観、比較)

Research Presentations:

 - Misayo Nagayama (Tokyo Woman's Univ, Dept of Mathematics)
  (Proofnetsの新しいCharacterization Theoremの研究報告)

Several other presentations will be scheduled. (Around eight (8)- ten (10)
slots are available for research presentations.)

この他に更に研究発表の追加が予定されております．
講義形式の講演は各１時間(ただしGirardの講義は４回の連続講義形式)、
線形論理に関する研究発表は各々３０分ー４０分の予定です。


Call for papers.

  The PC of the workshop is seeking for talks of on-going research 
related to linear logic (around 30-40 minutes talks).
  Please write to <linear-workshop@abelard.flet.keio.ac.jp> with your proposed title and abstract or PS-file of paper/draft-paper.

現在進展中の研究も含めて，線形論理に関連する研究に関する発表を希望なさる方は，上のアドレスにタイトル及びアブストラクト (もし論文又は論文草稿のある方は
その PS 形式のファイル) をお送りください．
PC (J-Y. Girard, ，小林直樹, 岡田光弘) の間でプログラムの調整をさせて頂きます．


Linear Logic Workshop Program Committee:
  J-Y. Girard (CNRS,France),
  Naoki Kobayashi (U. Tokyo),
  Mitsu Okada (Keio U.).

Linear Logic Workshop Organizing Committee (tentative):
  Naoki Kobayashi (U. Tokyo, Computer Science),
  Masaki Murakami (Okayama U. Computer Engineering)
  Misao Nagayama (Tokyo Woman's U., Mathematics),  
  Mitsu Okada (Keio U., Philosophy),
  Suguru Shirahata (Keio U., Mathematics)
  Naoyuki Tamura (Kobe U., System Engineering)


Call for participation (Free of charge):
  Please fill the following registration form.
  Some hotel list is also attached below.

参加自由・無料ですが，準備の都合上なるべく下の登録ファイルを返送してください．
返送された方には，その後の連絡事項が直接メールで送られます．

Hotel Information(ホテル情報):
Please make a reservation by yourself directly if needed;
御自身で直接予約してください。

Walking distances
1. Hotel Mita-Kaikan (ホテル三田会館) Single 6940 円、Twin 11200円
03-3453-6601

2. Mita-Miyako Hotel 三田都ホテル(Single 10500の10%引き Twin 16000の10%引き 
から)
03-3454-3111 (10%引きのために、予約時に慶応線形論理会議出席と言ってください。)


3.(this is not walking distance but need subway connections or bus for
30 minutes (at Akasaka), but fairly cheap.)
Asia-Kaikan (アジア会館) Single from 5100, Twin from 6800
03-3402-6111.

4. If you are (or your friend is) a member of International House
(roppongi) 国際文化会館(六本木)
we strongly recommend there. (Maybe, 15 minutes by bus, but the bus
schedule is not very frequent)。 Reservation needs a fererence to a
member of the International House.

5. There are other walking distance hotels, Olympic-In, Azabu City Hotel,
Tokyo Ground Hotel, Shiba Prince Hotel, etc.


================================================================================
Registration Form (Please send this to 
<linear-workshop@abelard.flet.keio.ac.jp>)

I would like to attend the Linear Logic Workshop (Feb 26-27, 1999, at the Mita Campus, Keio University, Tokyo).


Name (氏名):

email address (メールアドレス):

Affiliation (所属)[もし学生の場合は学年もお願いします]:


================================================================================

********************************************************************************

Subject: Linear Logic Workshop
Date: Wed, 24 Feb 1999 23:50:25 +0900

Linear Logic Workshop への参加申し込み、
ありがとうございました。

早速プログラムをお送りさせていただきます。
なお text の後ろに LaTeX file を添付させて
いただきましたので、よろしければご利用ください。

Linear Logic Workshop Program

日程： Feb. 26th, Friday - 27th, Saturday, 1999
       (1999年2月26日(金)～27日(土))
場所： Mita-Campus of Keio University, Tokyo, Room 311 (The first floor
       of the building #3 (Daigakuin-Tou))
       (慶應義塾大学 三田キャンパス 大学院棟 311番教室 (第3校舎))
       
       (5 minutes walk from JR-Tamachi station or Subway Mita station:
       JR田町駅又は地下鉄三田駅から徒歩5分)


Feb. 26th, Friday (2月26日(金))

9:30 a.m.- 10:30 a.m.
 Title: Special Lecture: Meaning of Logical Rules: Elements of Ludics I
 Speaker: J-Y.Girard (CNRS-IML, Marseille, France)
 Abstract:


10:30 a.m.- 10:45 a.m. (break)


10:45 a.m.- 11:45 a.m.
 Title: Tutorial: Phase Semantics and its Applications
 Speaker: Mitsu Okada with Kazushige Terui 
         (Department of Philosophy, Keio University)
 Abstract:


11:45 a.m.- 1:00 p.m. (lunch break)


1:00 p.m.- 2:00 p.m.
 Title: invited talk: (tentative title) Some History of Lambda Calculus 
        and Combinator Logic
 Speaker: (Not confirmed yet) Roger Hindley 
         (Visiting Tokyo Institute of Technology)
 Abstract:


2:10 p.m.- 2:40 p.m.
 Title: A Study of Abramsky's Linear Chemical Abstract Machine
 Speaker: S. Mikami and Y. Akama (University of Tokyo)
 Abstract: Abramsky's Linear Chemical Abstract Machine ({\sc lcham}) 
           is a term calculus which corresponds to Linear Logic, 
           via the {\em Curry-Howard isomorphism}.  
           We introduce a translation from a linear $\lambda$-calculus 
           into \textsc{lcham}. The translation result can be well regarded 
           as a black box with the i/o ports being atomic. 
           We show that one step computation of {\sc lcham} is
           equivalent to that of the linear $\lambda$-calculus. Then, 
           we prove the {\em principal typing theorem} of {\sc lcham}, 
           which implies the decidablity of type checking.


2:40 p.m.- 3:10 p.m.
 Title: New Characterization of Non-commutative Proof Nets
 Speaker: Misao Nagayama (Dept of Mathematics, Tokyo Woman's University)
         and Mitsu Okada (Dept of Philosophy, Keio University)
 Abstract: 


3:10 p.m.- 3:20 p.m. (break)


3:20 p.m.- 3:50 p.m.
 Title: A General Framework for the Denotational Completeness
 Speaker: Kazusige Terui (Depertment of Philosophy, Keio University)
 Abstract: 


3:50 p.m.- 4:00 p.m. (break)


4:00 p.m.- 4:30 p.m.
 Title: Compiling Intuitionistic Linear Logic Programming Languages
 Speaker: Mutsunori Banbara (Nara National College of Technology),
         Kyoung-sun Kang (Depertment of Computer Science, Kobe University),
         and Naoyuki Tamura (Depertment of Computer Science, Kobe University)
 Abstract: There have been several proposals for logic programming languages
           based on linear logic: Lolli, Lygon, LO, LinLog, Forum, HACL. 
           In these languages, it is possible to create and consume 
           resources dynamically as logical formulas. The efficient handling 
           of resource formulas is therefore an important issue in the 
           implementation of these languages.

           When a system needs to execute the goal G1$\ast$G2 during the
           goal-directed(i.e. from the root to the leaves) proof search in
           original intuitionistic linear logic, there occurs a lot of
           non-determinism. In the paper on Lolli, Hodas and Miller solved 
           this problem by using IO-model in which each goal has its input 
           resources and output resources. Output resources of G1 are 
           forwarded to G2 as its input resources.

           We propose Leveled IO-model, a refinement of IO-model with level
           indices, to execute the goal G1\&G2 and !G efficiently. Leveled
           IO-model has a index which represents the current consumption level.
           At a given point in the proof, only resources labeled with that
           consumption level can be consumed. In addition, Leveled IO-model 
           has a new flag to solve the non-determinism which occurs in the 
           execution of top.

           Leveled IO-model enables us to develop more efficient implementation
           than IO-model. We have developed a compiler system called LLP 
           by using Leveled IO-model. LLP is a superset of Prolog and covers 
           a significant fragment of Lolli. The execution speed of LLP is 
           about 150 times faster than Lolli interpreter.

           Furthermore, we have extended the original LLP implementation by
           compiling resource formulas. To compile resource formulas with free
           variables, we introduce a new data structure which consists of a
           compiled code and a set of bindings for free variables. Such 
           structure corresponds to the idea of a closure that is widely used 
           in implementations of functional programming languages. 
           We gained about 28\% speedup by compiling resource formulas.


4:30 p.m.- 4:50 p.m.
 Title: Timed Petri nets and temporal linear logic (on-going work)
 Speaker: Makoto Tanabe 
         (Japan Science and Technology Corporation / ASTEM-RI Tokyo)
 Abstract: It is well known that Petri nets constitute the algebraic 
           structure of quantales, which can be models of linear logic.
           As a timed extension to quantales, {\em timed R-monoids} are 
           deifned, which are constructed from timed Petri nets.

           Next, {\em temporal linear logic} is introduced, which has timed 
           Petri nets as its models, i.e., whose formulas can be interpreted 
           as sets of timed markings of a timed Petri net.

           Soundness of the logic with respect to timed Petri net in 
           terpretation is shown.
           Finally, examples show how to express properties of timed 
           Petri nets by temporal linear logic.


5:00 p.m.- 6:00 p.m.
 Title: Special Lecture: Meaning of Logical Rules: Elements of Ludics II
 Speaker: J-Y.Girard (CNRS-IML, Marseille, France)
 Abstract:


Feb. 27th, Saturday (2月27日(土))

9:30 a.m.- 10:30 a.m.
 Title: Special Lecture: Meaning of Logical Rules: Elements of Ludics III
 Speaker: J-Y.Girard (CNRS-IML, Marseille, France)
 Abstract:


10:30 a.m.- 10:45 a.m. (break)


10:45 a.m.- 11:45 a.m.
 Title: Tutorial： Applications of Linear Logic to Programming Languages
 Speaker: Naoki Kobayashi with Toshihiro Shimizu and Eijiro Sumii
        (Depertment of Computer Science, University of Tokyo)
 Abstract: In this talk, we give a brief overview of some applications 
           of linear logic: linear type systems for functional and concurrent 
           programming languages, and the concurrent linear logic programming 
           framework. 
           We also introduce their extensions such as the quasi-linear 
           types and deadlock-free type systems and discuss their 
           relationships with linear logic.


11:45 a.m.- 1:00 p.m. (lunch break)

1:00 p.m.- 2:00 p.m.
 Title: invited talk: On the temporal proof of reactive systems
 Speaker: Naoki Yonezaki (Depertment of Computer Science, 
         Tokyo Institute of Technology)
 Abstract: 


2:10 p.m.- 2:40 p.m.
 Title: Multi-dimentional Representation of Concurrent Processes
        using Linear Logic
 Speaker: Masaki Murakami (University of Okayama)
 Abstract: A new representation of concurrent processes using linear logic 
           is introduced.  Each of messages, processes and definitions of 
           process behaviours is represented with a linear logic formula 
           as existing models. A multiset of active processes, messages 
           and definitions is represented as a $n$-dimensional hypercube 
           instead of sequent where $n$ is the number of bound names of 
           channels and processes that are active. The multi-dimensional 
           representation is introduced to represent the scopes of all 
           active bound names at the same time. A set of rules for the 
           operational semantics is introduced as an extension of sequent 
           calculus.


2:40 p.m.- 3:10 p.m.
 Title: Semantics for linear set theory
 Speaker: Masaru Shirahata (Keio University)
 Abstract: We discuss the semantics for the set theory based on linear logic
           and some of the related problems. First we review the standard
           technique to construct a model for the set theory on various logics,
           and show how to extend it to linear logic. Secondly, we modify the
           construction so that we can obtain the model for set theory with the
           unrestricted comprehension. Finally, we discuss some of the related
           issues, in particular the notion of "contradiction" and 
           extensionality.


3:10 p.m.- 3:20 p.m. (break)


3:20 p.m.- 3:50 p.m.
 Title: Temporal linear logic with natural meaning
 Speaker: Yoshiaki Minamisawa, Naoki Yonezaki
        (Department of Computer Science, Tokyo Institute of Technology)
 Abstract: M.Kanovich and T.Ito introduced temporal linear logic (TLL)
           which has the temporal operators named 'next' and 'later'.
           In TLL, the operators 'next' and 'later' have
           a small gap between semantics and intuitive meaning.

           We will propose two sequent calculus systems of
           temporal linear logic in which the gap is resolved.

           Both systems we introduced can prove the formulas
           which are not provable in TLL.

           The first system is got from TLL system
           by changing the rules related to 'later' operator.

           The second system has a special atomic
           proposition '$\tau$' as a time unit.
           Some special formulas with '$\tau$' can be seen as
           these operators. 
           This special atomic proposition is used to control
           inference in a proof of sequent calculus.


4:00 p.m.- 4:30 p.m.
 Title: Gentzen-style classical logic as CPS calculus
 Speaker: Ichiro Ogata (Electrotechnical lab.)
 Abstract: We show that one can encode proof of the Gentzen's
           {\em LKsystem} as the $\lambda$-terms; and the cut-elimination 
           procedure for {\em LKsystem} as $\beta$-contraction. 
           Precisely, we observe that Strongly Normalizable(SN) and 
           Church-Rosser(CR) cut-elimination procedure for
           (intuitionistic decoration of) {\em LKQsystem}, as presented 
           in Danos et al.(1993), can be considered as the call-by-value(CBV) 
           Continuation Passing Style(CPS) computation.


4:30 p.m.- 5:00 p.m.
 Title: to be announced
 Speaker: to be announced
 Abstract:


5:00 p.m.- 5:20 p.m. (break)


5:20 p.m.- 6:20 p.m.
 Title: Special Lecture: Meaning of Logical Rules: Elements of Ludics IV
 Speaker: J-Y.Girard (CNRS-IML, Marseille, France)
 Abstract:


----------------------- LaTeX file -------------------------------
\documentstyle[a4j]{jarticle}

%%%%%% new environment ``sweetdesc'' %%%%%%
  \def\sweetlabel#1{\bf #1\hfill}%
  \def\sweetdesc{\list{}%
      {\labelwidth 40pt \leftmargin\labelwidth
       \topsep 5pt \itemsep 0pt
       \parsep 0pt
       \listparindent 0pt
       \advance\leftmargin\labelsep
       \let\makelabel\sweetlabel}}%
  \let\endsweetdesc\endlist%

%%%%%% new command ``program'' %%%%%%
\newcommand{\program}[4]%
  {\noindent $\bullet${\tt #1} \vspace*{-.5em}\begin{quote}\begin{sweetdesc}%
  \item[{\rm Title:}] {\it #2}%
  \item[{\rm Speaker:}] #3%
  \vspace{0.5em}\item[{\rm Abstract:}] #4%
  \end{sweetdesc}\end{quote}%
  \vspace{.5em}%
}%

%%%%%% new command ``breaktime'' %%%%%%
\newcommand{\breaktime}[1]%
  {\noindent $\bullet$\hspace{1.2ex}{\tt #1} (break)%
  \vspace{1em}}%

%%%%%% new command ``lunch'' %%%%%%
\newcommand{\lunch}[1]%
  {\noindent $\bullet$\hspace{1.2ex}{\tt #1} (lunch break)%
  \vspace{1em}}%


\begin{document}

\begin{center}
{\LARGE Linear Logic Workshop プログラム}
\end{center}

\begin{quote}
\begin{sweetdesc}
\item[日程：] Feb. 26th, Friday - 27th, Saturday, 1999
 (1999年2月26日(金)～27日(土))
\item[場所：] Mita-Campus of Keio University, 
  Tokyo, Room 311 (The first floor of the building #3
  (Daigakuin-Tou))\\
  (慶應義塾大学 三田キャンパス 大学院棟 311番教室 (第3校舎))\\
  (5 minutes walk from JR-Tamachi station or Subway Mita station:
  JR田町駅又は地下鉄三田駅から徒歩5分)
\end{sweetdesc}
\end{quote}


\vspace{2em}
\noindent
{\large\bf Feb. 26th, Friday (2月26日(金))}

\program{
9:30 a.m.- 10:30 a.m.}{
Special Lecture: Meaning of Logical Rules: Elements of Ludics I}{
J-Y.Girard (CNRS-IML, Marseille, France)}{
}

\breaktime{10:30 a.m.- 10:45 a.m.}

\program{
10:45 a.m.- 11:45 a.m.}{
Tutorial: Phase Semantics and its Applications}{
Mitsu Okada with Kazushige Terui 
  (Department of Philosophy, Keio University)}{
}


\lunch{11:45 a.m.- 1:00 p.m.}

\program{
1:00 p.m.- 2:00 p.m.}{
invited talk: (tentative title) Some History of Lambda Calculus 
  and Combinator Logic}{
(Not confirmed yet) Roger Hindley (Visiting Tokyo Institute of Technology)}{
}

\program{
2:10 p.m.- 2:40 p.m.}{
A Study of Abramsky's Linear Chemical Abstract Machine}{
S. Mikami and Y. Akama (University of Tokyo)}{
Abramsky's Linear Chemical Abstract Machine ({\sc lcham}) is a term
calculus which corresponds to Linear Logic, via the {\em
Curry-Howard isomorphism}.  We introduce a translation from a
linear $\lambda$-calculus into \textsc{lcham}. The translation
result can be well regarded as a black box with the i/o ports being
atomic. We show that one step computation of {\sc lcham} is
equivalent to that of the linear $\lambda$-calculus. Then, we prove
the {\em principal typing theorem} of {\sc lcham}, which implies the 
decidablity of type checking.
}

\program{
2:40 p.m.- 3:10 p.m.}{
New Characterization of Non-commutative Proof Nets}{
Misao Nagayama (Dept of Mathematics, Tokyo Woman's University)
and Mitsu Okada (Dept of Philosophy, Keio University)}{
}

\breaktime{3:10 p.m.- 3:20 p.m.}

\program{
3:20 p.m.- 3:50 p.m.}{
A General Framework for the Denotational Completeness}{
Kazusige Terui (Depertment of Philosophy, Keio University)}{
}

\breaktime{3:50 p.m.- 4:00 p.m.}

\program{
4:00 p.m.- 4:30 p.m.}{
Compiling Intuitionistic Linear Logic Programming Languages}{
Mutsunori Banbara (Nara National College of Technology),
Kyoung-sun Kang (Depertment of Computer Science, Kobe University),
and  Naoyuki Tamura  (Depertment of Computer Science, Kobe University)}{
There have been several proposals for logic programming languages
based on linear logic: Lolli, Lygon, LO, LinLog, Forum, HACL. In these
languages, it is possible to create and consume resources dynamically
as logical formulas. The efficient handling of resource formulas is
therefore an important issue in the implementation of these languages.

When a system needs to execute the goal G1$\ast$G2 during the
goal-directed(i.e. from the root to the leaves) proof search in
original intuitionistic linear logic, there occurs a lot of
non-determinism. In the paper on Lolli, Hodas and Miller solved this
problem by using IO-model in which each goal has its input resources
and output resources. Output resources of G1 are forwarded to G2 as
its input resources.

  We propose Leveled IO-model, a refinement of IO-model with level
indices, to execute the goal G1\&G2 and !G efficiently. Leveled
IO-model has a index which represents the current consumption level.
At a given point in the proof, only resources labeled with that
consumption level can be consumed. In addition, Leveled IO-model has a
new flag to solve the non-determinism which occurs in the execution of
top.

  Leveled IO-model enables us to develop more efficient implementation
than IO-model. We have developed a compiler system called LLP by using
Leveled IO-model. LLP is a superset of Prolog and covers a significant
fragment of Lolli. The execution speed of LLP is about 150 times
faster than Lolli interpreter.

Furthermore, we have extended the original LLP implementation by
compiling resource formulas. To compile resource formulas with free
variables, we introduce a new data structure which consists of a
compiled code and a set of bindings for free variables. Such structure
corresponds to the idea of a closure that is widely used in
implementations of functional programming languages. We gained about
28\% speedup by compiling resource formulas.
}


\program{
4:30 p.m.- 4:50 p.m.}{
Timed Petri nets and temporal linear logic (on-going work)}{
Makoto Tanabe (Japan Science and Technology Corporation / ASTEM-RI Tokyo)}{
It is well known that Petri nets constitute the algebraic structure of
quantales, which can be models of linear logic.
As a timed extension to quantales, {\em timed R-monoids} are deifned, which
are constructed from timed Petri nets.

Next, {\em temporal linear logic} is introduced, which has timed 
Petri nets as
its models, i.e., whose formulas can be interpreted as sets of timed
markings of a timed Petri net.

Soundness of the logic with respect to timed Petri net in terpretation
is shown.
Finally, examples show how to express properties of timed Petri nets by
temporal linear logic.
}


\program{
5:00 p.m.- 6:00 p.m.}{
Special Lecture: Meaning of Logical Rules: Elements of Ludics II}{
J-Y.Girard (CNRS-IML, Marseille, France)}{
}


\vspace{2em}
\noindent
{\large\bf Feb. 27th, Saturday (2月27日(土))}

\program{
9:30 a.m.- 10:30 a.m.}{
Special Lecture: Meaning of Logical Rules: Elements of Ludics III}{
J-Y.Girard (CNRS-IML, Marseille, France)}{
}

\breaktime{10:30 a.m.- 10:45 a.m.}

\program{
10:45 a.m.- 11:45 a.m.}{
Tutorial： Applications of Linear Logic to Programming Languages}{
Naoki Kobayashi with Toshihiro Shimizu and Eijiro Sumii
  (Depertment of Computer Science, University of Tokyo)}{
In this talk, we give a brief overview of some applications 
of linear logic: linear type systems for functional and concurrent 
programming languages, and the concurrent linear logic programming 
framework. We also introduce their extensions such as the quasi-linear 
types and deadlock-free type systems and discuss their relationships 
with linear logic.
}


\lunch{11:45 a.m.- 1:00 p.m.}

\program{
1:00 p.m.- 2:00 p.m.}{
invited talk: On the temporal proof of reactive systems}{
Naoki Yonezaki (Depertment of Computer Science, 
  Tokyo Institute of Technology)}{
}


\program{
2:10 p.m.- 2:40 p.m.}{
Multi-dimentional Representation of Concurrent Processes
 using Linear Logic}{
Masaki Murakami (University of Okayama)}{
A new representation of concurrent processes using linear logic 
is introduced.  Each of messages, processes and definitions of process
behaviours is represented with a linear logic formula as existing
models. A multiset of active processes, messages and definitions is
represented as a $n$-dimensional hypercube instead of sequent where
$n$ is the number of bound names of channels and processes that are
active. The multi-dimensional representation is introduced to
represent the scopes of all active bound names at the same time. A set
of rules for the operational semantics is introduced as an extension
of sequent calculus.
}


\program{
2:40 p.m.- 3:10 p.m.}{
On the semantics of linear set theory and related issues}{
Masaru Shirahata (Keio University)}{
We discuss the semantics for the set theory based on linear logic
and some of the related problems. First we review the standard
technique to construct a model for the set theory on various logics,
and show how to extend it to linear logic. Secondly, we modify the
construction so that we can obtain the model for set theory with the
unrestricted comprehension. Finally, we discuss some of the related
issues, in particular the notion of "contradiction" and extensionality.
}


\breaktime{3:10 p.m.- 3:20 p.m.}

\program{
3:20 p.m.- 3:50 p.m.}{
Temporal linear logic with natural meaning}{
Yoshiaki Minamisawa, Naoki Yonezaki
  (Department of Computer Science, Tokyo Institute of Technology)}{
M.Kanovich and T.Ito introduced temporal linear logic (TLL)
which has the temporal operators named 'next' and 'later'.
In TLL, the operators 'next' and 'later' have
a small gap between semantics and intuitive meaning.

We will propose two sequent calculus systems of
temporal linear logic in which the gap is resolved.

Both systems we introduced can prove the formulas
which are not provable in TLL.

The first system is got from TLL system
by changing the rules related to 'later' operator.

The second system has a special atomic
proposition '$\tau$' as a time unit.
Some special formulas with '$\tau$' can be seen as
these operators. 
This special atomic proposition is used to control
inference in a proof of sequent calculus.
}


\program{
4:00 p.m.- 4:30 p.m.}{
Gentzen-style classical logic as CPS calculus}{
Ichiro Ogata (Electrotechnical lab.)}{
We show that one can encode proof of the Gentzen's
{\em LKsystem} as the $\lambda$-terms; and the cut-elimination procedure
for {\em LKsystem} as $\beta$-contraction. 
Precisely, we observe that Strongly
Normalizable(SN) and Church-Rosser(CR) cut-elimination procedure for
(intuitionistic decoration of) {\em LKQsystem}, as presented in Danos et
al.(1993), can be considered as the call-by-value(CBV) Continuation
Passing Style(CPS) computation.
}


\program{
4:30 p.m.- 5:00 p.m.}{
to be announced}{
to be announced}{
}

\breaktime{5:00 p.m.- 5:20 p.m.}

\program{
5:20 p.m.- 6:20 p.m.}{
Special Lecture: Meaning of Logical Rules: Elements of Ludics IV}{
J-Y.Girard (CNRS-IML, Marseille, France)}{
}


\end{document}

********************************************************************************