# SLACS2000 $B%"%V%9%H%i%/%H=8(B $BCfLn(B $B9@(B ($BN6C+Bg3X(B $BM}9)3XIt(B) $B6a;wMMAj$K$h$k9=@.E*%W%m%0%i%_%s%0(B Constructive programming with approximation modality $B;EMM$N6a;w2aDx$rI=8=$9$kMMAjIU$-7?IU$1%7%9%F%$r1~MQ$9$k$H!"Hs>o$K9-(B $B$$HO0ON;EMMd B2#Fb(B B42J8(B (B72GOBg3X(B B9)3XIt(B B>pJs9)3X2J(B) Refinement typeBN7?%A%'%C%/!&%"%k%4%j%:%H=N Type checking algorithms for refinement types and their implementation Refinement (nonstandard) typeBHO!DL>oN7?>eN#1JQ?t=R8lr0UL#7!$$=(B $B$N7?%A%'%C%/$J$$7O7??dO@NOHAHNCfG!MM!9J%W%m%0%i%N2r@O,2DG=G(B B"k3H,CNilF$$$k!%$3$NH/I=$G$O!$C1=c7?BN7O$N>e$K!$(Bintersection $B$H(Bunion$B$N=89g1i;;$HHw$($?(Brefinement type$B$N7A<0BN7O$rDj5A$7!$$=N7?%A%'%C(B B%/!&%"%k%4%j%:%rDs0F9k!%^?!eG B:dK\?-9,(B (BElKLBg3XBg3X1!M}3X8&5f2J?t3X@l96(B) B?7?J(Bcountable functionalBN9=@.K!(B A new construction of countable functionals B=>MhN(B Kleene BN4X?tE,MQ(B f|g BhjD>46E*KM}2r7d9$$4X?tE,MQ(B fg $B$rDj5A(B $B$7(B,$B$3$N4X?tE,MQ$rMQ$$Fb(B countable functional BrDj5AG-k3Hr<(9(B.B^(B B?(B,B3N4X?tE,MQrMQ$$$F(B type-free theory APP $B$N%b%G%k$r9=@.$G$-$k$3$H$b(B $B<($5$l$k(B. $BLSMx85I'(B ($BKLN&@hC<2J3X5;=QBg3X1!Bg3X(B $B>pJs2J3X8&5f2J(B)
XPE with Theorem Provers

XPE(X Proof Editor)$B$O!"(BTeX$B$G$N>ZL@?^$N:n@.$r;Y1g$9$k%=%U%H$G$"$k!#$3(B $B$N(BXPE$B>e$G(Btheorem prover$B$r8F$S=P$9$3$H$K$h$j!"MF0W$KMxMQ$G$-$k2DFI@-$H(B $B:FMxMQ@-$N6K$a$F9b$$(Btheorem proverBHJC?!#(B 2000/8/15B8=:_NMxMQ2DG=JBN7O(B(BL?BjO@M}(B):classical logic, intuitionistic logic, FLe, FLew, FLec, K, KT, S4, S5(B9bLnN7hDj BC]Fb@t(B(B5~ETBg3X>pJs3X8&5f2J(B) B&X@5B'8@8lNB,EY,M-M}?tG"k3H(B B&X@5B'8@8lNB,EYOM-M}?tG"k!#(B BF#ED7{1Y!JEg:,Bg3X!K!(BA. Middeldorp B!JC^GHBg3X!K(B BF14|9=q-49(7O(B Synchronized Term Rewriting Systems We present an extension of term rewriting systems with the mechanism of synchronization, called synchronized TRS's. The notion of synchronization is newly introduced for synchronizing applications of rewriting rules. We prove the fundamental properties of the synchronized ground TRS's: (1) The reachability problem of synchronized ground TRS's is equivalent to the Post's Correspondence Decision Problem. (2) The halting problem of synchronized ground TRS's is equivalent to that of a two-counter automaton. B;3ED(B B=S9T(B (BC^GHBg3X(B BEE;R!&>pJs9)3X7O(B) BC1=c7?IU-9=q-49(7ONDd;_@-(B Termination of Symply Typed Term Rewriting Systems In this talk, I propose simply typed term rewriting systems, which extend first order term rewriting systems to the higher order case by allowing higher order symbols but without using bound variables. We discuss a semantic method for ensuring termination of simply typed term rewriting systems. B6aF#DLO/(B (BEg:,Bg3XAm9gM}9)3XIt(B) weak interlaced bilattice BN9=B$$K$D$$F(B On structures of weak interlaced bilattices weak interlaced bilattice BOO@M}%W%m%0%i%_%s%0N0UL#O@K*$$$F(B $B=EMW$JLr3d$r2L$?$7$F$$k,!$$3$NBe?t7O$N?t3XE*9=B$$KD$$$F$O(B $BITL@$JE@$,B?$$!%33GO!$$3$NBe?t7O$N;}$D4pK\E*$J@- $B2 $B%U%!%8%#4X78$N0lHL2=$K$D$$F(B On a generalization of fuzzy relation B%U%!%8%#4X78KD$$$F$O!$:#$^$G$O$[$H$s$I$N>l9g$K%/%j%9%W=89g$N>e$N(B $B%U%!%8%#4X78!$$9JoA%/%j%9%W=89gND>@QN%U%!%8%#ItJ,=89g,07olF(B B-?!%:#2sO0lHLN%U%!%8%#=89g!J%/%j%9%W=89gN%U%!%8%#ItJ,=89g!KN>e(B BN%U%!%8%#4X78N$$$m$$mJ@- In most cases fuzzy relations have been treated as fuzzy relations on crisp sets, that is, as fuzzy subsets of cartesian products of crisp sets. In my talk various properties on fuzzy relations on fuzzy sets (fuzzy subsets of crisp sets) will be discussed. BGr4z!!M%(B (B7DXf5A=NBg3X>&3XIt(B) B%2!<%G%kN%@%%"%l%/%F%#%+2r Goedel's Dialectica interpretation and game semantics We study Goedel's Dialectica interpretation of HA by T from the perspective of the game semantics of PCF. The higher-order functions are then seen as the first-order functions plus strategies. To make this point concrete, we define a version of Hintikka game for the first-order formulas and show how to read out the winning strategy from a proof. B9b66@5;R(B B!J9q:]4pFD65Bg3X!K(B B%A%e!<%H%j%"%k!'>ZL@H7?(B theoretical computer science BOFq79.kH$$$&@<$r;~!9<*$K$7$^$9!%(B $B;d$N9M$($G$O!$(Btcs $B$ODl$N@u$$J,LnGOJ$$$+$iEvA3$@$H$$&5;}AH!(B Bb&0lDO!Nr;KN@u5d=NB>N;v>p+iL@.=OJItJ,r$$$m$$mJz((B B?^^650i,9TolF$$$k$?$a$G$O$J$$+H$$$&5$$,7^9!%3N8eZL@H7?!WH!V7W;;O@!WK4X9k;dN55d+J;n_KD$$(B $B$F$*OC$7$F$_$?$$H;W$$$^$9!%(B $BpJsM}9)3X8&5f2J(B $B?tM}!&7W;;2J3X@l96(B) $B%i%%@7W;;$NI8=2=DjM}$N4JC1$J>ZL@(B Simple proof of the standardization theorem in lambda-calculus We present a new proof of the standardization theorem in lambda-calculus, which is performed by inductions based on an inductive definition of beta-reducibility with a standard sequence. $BGO>l(B $B8,2p(B ($B6e=#Bg3XBg3X1!(B $B%7%9%F%>pJs2J3X8&5f2J(B $B>pJsM}3X@l96(B)
$B>l9gJ,$1$K$h$k>ZL@(B Case Calculus for Classical Logic We introduce a new natural deduction formulation with one conclusion for implicational classical logic. The idea of the formulation is based on proof by case analysis''. We define reduction rules and prove weak normalization. As a corollary, we have the subformula property for normal proofs. This is a joint work with Sachio Hirokawa, Ryo Kashima, Yuichi Komori and Izumi Takeuti. $BW"@n:4@iCK(B ($B6e=#Bg3X(B) $BD9#D@55,7A$H>ZL@?^$NM#0l@-(B
Long D-normal form and uniqueness of proofs

There have been much interest in the conditions for uniqueness of normal form proofs in intuitionistic logic. [Tatsuta99] introduced a notion of D-normal form proof and showed that D-normal form proof is unique for any implicational formula. But this result means the uniqueness of D-normal form proof. There may be some other normal form proof which is not D-normal. We show that D-normality yields the uniqueness of proofs as long as the long-normal form proofs are concerned.

$B3QC+NII'(B ($B5~ETBg3X?tM}2r@O8&5f=j(B)
Duality between Call-by-name Recursion and Call-by-value Iteration

The duality between values and continuations enables us to exchange the call-by-name programming paradigm for the call-by-value one and vice versa. Since recursion is an essential factor for programming languages and the $\lambda\mu$-calculi fit in this duality, we extend the $\lambda\mu$-calculi with recursion operators and demonstrate the duality between recursion and iteration in the $\lambda\mu$-calculi.

$B>e=P!!E/9-(B ($BOB2N;39)6H9bEy@lLg3X9;EE;R9)3X2J(B)
Mingle$B$r;}$DItJ,9=B$O@M}(B
Substructural Logics with Mingle

We introduce structural$B!!(B rules mingle, and investigate theorem-equivalence, cut- eliminability, decidability, interpolability and variable sharing property for sequent calculi having the mingle. These results include new cut-elimination results for the extended logics: FL$B#m(B(full Lambek logic with$B!!(Bthe mingle), GLm(Girard's linear logic with the mingle) and Lm(Lambek calculus with restricted mingle). Moreover we show that Lm is useful for an application to the categorial grammar. $B:4!9LZ9nL&(B ($BFn;3Bg3X?tM}>pJs3XIt(B) Propositional lax logic $B$K$*$1$kA*8@$N$J$$O@M}<0KD$$$F(B Exact models for disjunction free fragments of propositional lax logic Propositional lax logic(PLL)$B$O(BMoggi$B$,F3F~$7$?(BComputational typed lambda calculus $B$H%+%j!4Q $BEDCf5A?M(B (\$B6e=#;:6HBg3X7P:Q3XIt(B)
Some proof systems for common knowledge predicate logic

We present some proof systems for common knowledge predicate logic which is complete with respect to the class of Kripke frames with constant domains.

John Longley (Edinburgh University)
Programming languages and notions of computability

According to Church's Thesis, all reasonable (sufficiently expressive) programming languages have the same computational power in the sense that they can compute the same class of functions on the natural numbers. However, if we measure the computational power of programming languages in more subtle ways (e.g. we consider which operations are computable at higher types), then interesting differences emerge between different languages, and we discover several natural notions of "computability". In this talk I will give a brief survey of various notions of computability, and of current research in this area.

Last Updated at Wed Aug 30 11:33:16 JST 2000 by Yukiyoshi Kameyama