tag:blogger.com,1999:blog-301893373063372699.post6354990687442850953..comments2023-03-01T01:00:28.853+11:00Comments on Discus Development: Falling down the naming wellAnonymoushttp://www.blogger.com/profile/08287674468193351664noreply@blogger.comBlogger1125tag:blogger.com,1999:blog-301893373063372699.post-82991166524670079742011-04-20T12:26:18.854+10:002011-04-20T12:26:18.854+10:00Twelf will completely change your mind about varia...Twelf will completely change your mind about variable binding. HOAS makes dealing with names much easier. For proofs with low proof-theoretic complexity (like progress and preservation, but not like strong normalization), I think Twelf is a much more intuitive route.Jim Applehttps://www.blogger.com/profile/11080395413026172939noreply@blogger.com