🚀 go-pugleaf

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

$@62$i$/$O!IK!B'!I$,2?$r;X$9$N$+$,M}2r$G$-$F$$$J$$$?$a$@$H;W$$$^$9!#$I$&$b(J
$@652J=q!J$?$V$s=i?4<T$K$O$H$C$+$+$j$K$K$/$+$C$?$N$G!"$^$H$b$J$N$G$7$g$&!K(J
$@$K$O3:Ev$9$k8@MU$,$J$$$h$&$K;W$($^$9!#$G!"(J

 >$@IaDL!"JQ?t$NCV$-49$($H$$$&$H&K(J-calculus $@$G$$$&(J $@&A(J-conversion $@$N$3$H$r(J
 >$@$$$$$^$9!#B+G{JQ?t$NCV$-49$(!#$@$+$iJQ?t$NCV$-49$($r$7$F$b!">ZL@2DG=@-!"(J

$@B+G{JQ?t$NCV$-49$($OBeF~$K4X$9$kDj5A$+$iMh$kDjM}$N$h$&$G$9$,!"$"$C$F(J
$@$^$9$G$7$g$&$+!#$=$&$J$k$H!"K!B'$H$O!V?dO@5,B'!W!"!V8xM}!W!"!VDjM}!W(J
$@!J$"$k<o$N!)!K$r;X$7!"$+$D>.NS$5$s$N;XE&$+$i$9$k$H!VDj5A!W$O4^$^$J$$(J
$@$b$N$HM}2r$9$l$P$h$m$7$$$N$G$7$g$&$+!#(J

 >>$@;d$OJQ?t$NCV$-49$($K4X$9$kK!B'$J$s$>$J$$$H;W$C$F$$$?$N$G!"$3$A$i$K$"$k(J
 >>proof$@!!(Jchecker $@$G$NMQ8l$G@bL@$7$F$7$^$C$?$N$G$9$,!"$A$g$C$HJ6$i$o$7$+$C$?$+(J

$@$3$l$O;d$N;W$$0c$$$G$7$?!#(Jproof checker $@$O(J EKL $@$G$9$,!";d$,$b$A$@$7$?$N$O(J
$@%^%K%e%"%k$K:\$C$F$$$k$h$&$J@5<0$J8@MU$G$O$"$j$^$;$s!#(J

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

$@:#$7$P$i$/$N$*$D$-$"$$$r$*4j$$$7$^$9!#$?$@(Jequality$@$K4X$9$k5DO@$N<YKb$K(J
$@$J$C$F$$$J$1$l$PNI$$$N$G$9$,!#(J

////
//// Etsuro Minami: Computer Science Department, Stanford University
//// MSCS: minami@cs.stanford.edu
////