I learned simply typed lambda calculus in a lecture, so I implement STLC interpreter. STLC terms are strongly normalizing, therefore it won't stuck in infinite loop! (https://github.com/hamukazu/lets-get-arrested)

The flag is located at /home/user/flag.

nc 34.85.75.40 30007

講義で単純型付きラムダ計算(STLC)を習ったので、STLCのインタプリタを実装してみました。 単純型のつくプログラムのみを実行すれば無限ループも起こらないし安全ですね！(https://github.com/hamukazu/lets-get-arrested)

フラグは /home/user/flag にあります。

nc 34.85.75.40 30007

> f = (\x:A. y)
y is free variable
(\x:A.y) can't be simply typed
> f = (\x:A. x)
f = (\x:A.x) :: (A->A)
> g = (\p:A->A. p)
g = (\p:(A->A).p) :: ((A->A)->(A->A))
> h = (\q:B->B. q)
h = (\q:(B->B).q) :: ((B->B)->(B->B))
> v1 = g f
v1 = (\x:A.x) :: (A->A)
> v2 = h f
type mismatched for typing (h f)
with applying ((B->B)->(B->B)) to (A->A)
(h f) can't be simply typed
> sub2 = (\x:I. dec (dec x))
sub2 = (\x:I.(dec (dec x))) :: (I->I)
> 3times = (\f:I->I. \n:I. f (f (f n)))
3times = (\f:(I->I).(\n:I.(f (f (f n))))) :: ((I->I)->(I->I))
> v3 = (3times sub2) 13
v3 = 7 :: I