(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 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 ) 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} ********************************************************************************