もうすぐ2016年も終わるので今年したこととかをまとめる。 研究・勉強 割とずっとtyped lambda calculusのsyntaxやらsemanticsやらやってた気がする。 Proof Assistantももう少し調べなきゃなーと思いながらあんまり欲しい結果を出してる論文とかもないしこ…

前回はsimply-typedの拡張としてλμを実装したけれど、 今回はsimply-typedにrecursive typeを実装してみた。 recursive typeはいわゆる(G)ADT相当の機能だけど、型パラメータを持たないのでADTの真面目な実装に比べると楽だと思う。 recursive typeはType ->…

λμのtypecheckerを実装したので (ソースコードは参考文献[3]を参照) λμ[1]はλ→に継続(callCC)を入れたもの(CCC + Continuation monad)。 syntax的にはμ-abstractionとnaming(termに名前をつける)が追加される。 型なしの項を受け取って、それにうまく型をつ…

この記事はTheorem Prover Advent Calendar 2016 12日目の記事です。 この記事は定理証明初心者向けの記事です。 普段から依存型を用いた定理証明をされている方は読む必要がありません。 "coherence condition"と呼ばれる条件があり、訳すと「一貫性条件」…

今から大体3年くらい前の、大学学部2回生の頃に唐突に精神が死んだことがあった。 という話をするけど、この先読んでも特にオチはありません。 ただの身の上話なので。 非常に運がよかったため自分は3回生の進路振り分け的なものに必要な単位を前期で全て揃…

この記事はTheorem Prover Advent Calendar 2016の1日目の記事です。 今年も残り1ヶ月になったことを信じたくないと思いつつ、 まあ学生的には4月始まりだから大丈夫と自分に言い聞かせてます。 今回のアドベントカレンダーのネタを必死に1週間くらい前から…