CertiCoq : A verified compiler for Coq

Abhishek Anand,Andrew W. Appel,Greg Morrisett,Zoe Paraskevopoulou,Randy Pollack, Olivier Savary Bélanger,Matthieu Sozeau, Matthew Weaver

semanticscholar（2016）

引用 81|浏览3

暂无评分

摘要

CertiCoq is a mechanically verified, optimizing compiler for Coq that bridges the gap between certified high-level programs and their translation to machine language. We outline its design as well as the main foundational and engineering challenges involved in building and certifying a compiler for Coq in Coq.

查看译文

AI 理解论文

溯源树

样例

生成溯源树，研究论文发展脉络

Chat Paper

正在生成论文摘要