🚀 go-pugleaf

In article <1993Feb3.201423.18351@CSD-NewsHost.Stanford.EDU> minami@Xenon.Stanford.EDU (Etsuro Minami) writes:
>In article <1993Feb3.175858.21619@etl.go.jp> yoshiki@etl.go.jp (KINOSHITA Yoshiki) writes:
>
>>$B$"$H!"BeF~$HJQ?t$NCV$-49$($O0c$$$^$9$h!#(B
>
>$B$3$l$OJQ?t$NCV$-49$($K4X$9$kK!B'$,BeF~$NDj5A0J30$K$"$k!"$H$$$&$3$H$G$7$g$&$+!#(B

$B$?$V$s$=$&$$$&$3$H$@$H;W$$$^$9!#;vBV$r$O$C$-$j$5$;$k$K$OMQ8l$NDj5A$r$O(B
$B$8$a$+$i$d$C$F!"$*$?$,$$$K6&DL$NM}2r$r$7$F$$$k$N$+$I$&$+0l!93N$+$a$J$1(B
$B$l$P$J$j$^$;$s$,!"$=$l$O$7$s$I$$!#(B

$BIaDL!"JQ?t$NCV$-49$($H$$$&$H&K(B-calculus $B$G$$$&(B $B&A(B-conversion $B$N$3$H$r(B
$B$$$$$^$9!#B+G{JQ?t$NCV$-49$(!#$@$+$iJQ?t$NCV$-49$($r$7$F$b!">ZL@2DG=@-!"(B
validity $B$H$b$KITJQ$G$9$,!"BeF~$r$9$k$H>ZL@2DG=@-$b(B validity $B$bJQ$o$k(B
$B>l9g$,$"$j$^$9!#(B

>$B;d$OJQ?t$NCV$-49$($K4X$9$kK!B'$J$s$>$J$$$H;W$C$F$$$?$N$G!"$3$A$i$K$"$k(B
>proof$B!!(Bchecker $B$G$NMQ8l$G@bL@$7$F$7$^$C$?$N$G$9$,!"$A$g$C$HJ6$i$o$7$+$C$?$+(B
>$B$bCN$l$^$;$s!#$?$@A0<T$G$"$l$P!"0c$$$r65$($F$$$?$@$-$?$$$N$G$9$,!#(B

$B1Q8l$G2?$H$$$C$F$^$7$?$+!)(B $B2?$H$$$&(B proof checker $B$G$9$+!)(B

$BB+G{JQ?t$NCV$-49$($NK!B'$O$A$c$s$H$$$m$$$m$"$j$^$9!#B+G{JQ?t$NCV$-49$((B
$B$+$i@bL@$9$k$N$OBgJQLLE]$J$N$G!"$$$$$+$2$s$J652J=q$@$H!"$=$NJU$O$4$^$+(B
$B$7$F$$$^$9!#$G!":$$C$?$3$H$K<j$KF~$j$d$9$$BgDq$N652J=q$O$$$$$+$2$s$G$9!#(B
$B<B:]!"$-$C$A$j$d$C$F$7$+$b=i?4<T$K$b$o$+$j$d$9$/=q$/$H$$$&$N$OFq$7$$Cm(B
$BJ8$@$H;W$$$^$9!#(B

$B$J$s$+%W%m%0%i%`AjCL<<$_$?$$$K$J$C$F$-$?$J!#(B

$B$-$N$7$?(B

-- 
KINOSHITA Yoshiki [KINOSHITA is my family name]
Department of Computer Science, University of Edinburgh
James Clark Maxwell Building, The King's Buildings, Edinburgh EH9 3JZ, Scotland
[On leave from Electrotechnical Laboratory, 1-1-4 Umezono, Tsukuba, 305 Japan]