Group items tagged

Smalltalk@Wikipedia から流れついた項目。プラトンのイデア論と関連があるのか？Inheritance と Prototyping との関係について考察する素材になりそう。

LFやTwelfの流れを汲む証明系。証明木が見易いのが売りのようです。 [Types ML より] If you're planning to teach a programming language or logic foundations course and are thinking about using a proof assistant, you might consider SASyLF. SASyLF (Second-order Abstract Syntax Logical Framework) is an LF-based proof assistant that the same logical foundation and many of the same advantages as Twelf (in particular, variable binding is "built in"). However, it uses a syntax very close to that used for proofs on paper, giving the tool a much gentler learning curve--and much better error messages--than many alternatives.

SASyLF を採用した CMU での型理論の講義実施例