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提交), Typ