[pukiwiki]
I am a huge fan of [[Diigo:http://www.diigo.com/user/ken_wakita%5D%5D!

– [[Computer Science 732: Type Systems for Programming Languages (Fall 2008):http://www.cs.uwm.edu/classes/cs732/index-fa08.html%5D%5D – SASyLF を採用した CMU での型理論の講義実施例
– [[SASyLF: An Educational Proof Assistant for Language Theory:http://www.cs.cmu.edu/~aldrich/SASyLF%5D%5D – 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.

[/pukiwiki]