TypeSoundnessCertifier：免费的认证类型声音！

类型SoundnessCertifier 作者：Matteo Cimini（ ） 使用包含2.0.2到2.0.5的Abella版本测试的工具。 快速链接 消息：临时停止：几天后，该项目将停止工作，因为几天后我将上传更多文件。 TypeSoundnessCertifier包含两个组件： Lang-n-Check：输入语言定义，并对其进行类型检查以查看其是否为声音。 Lang-n-Prove：输入已由Lang-n-Check进行类型检查的语言定义，并在Abella证明助手中生成机器检查的类型健全性证明。 更新（2017年12月）： 截至2017年7月（2018年POPL提交）， TypeSoundnessCertifier自动解决POPLMark Challenge 2A ！！ （即，该工具会根据其语言定义自动为System F生成带有受限子类型的完全机械化的完整性证明。） 有关此