ttlite:Martin-Löf类型理论的超级编译器

【文件属性】：
文件名称：ttlite:Martin-Löf类型理论的超级编译器
文件大小：403KB
文件格式：ZIP
更新时间：2021-05-04 21:01:58
programming-language dependent-types coq type-theory idris TT Lite TT Lite是Martin-Löf的类型理论（TT）的解释器，类型检查器和超级编译器。 它分为两个子项目： TT Lite核心-Martin-Löf的类型论的轻量级和模块化实现（TT Lite在设计时考虑了超级编译） TT Lite超级编译器-TT Lite的非常简单的超级编译器。 超级编译器的主要特征是，对于由超级编译器执行的任何转换，都提供了正确性的证明。 TT Lite还支持导出为Agda，Coq和Idris语言，从而可以独立于TT Lite来验证执行的转换和生成的证明。 预印本对TT Lite的技术内部进行了描述： Ilya Klyuchnikov，Sergei Romanenko。 TT Lite：Martin-Löf类型理论的超级编译器。 Keldysh Institute预印本，2013年，第73号，第28页。 以下文件描述了我们认证超级编译