从数学到抽象机：可执行 Krivine 机的形式化推导
编程语言
2012-02-15 v1
摘要
本文展示了在依赖类型编程语言 Agda 中，从简单类型 lambda 演算的小步解释器推导出可执行 Krivine 抽象机的过程。
引用
@article{arxiv.1202.2924,
title = {From Mathematics to Abstract Machine: A formal derivation of an executable Krivine machine},
author = {Wouter Swierstra},
journal= {arXiv preprint arXiv:1202.2924},
year = {2012}
}
备注
In Proceedings MSFP 2012, arXiv:1202.2407