文章基本信息

标题：From Mathematics to Abstract Machine: A formal derivation of an executable Krivine machine
本地全文：下载
作者：Wouter Swierstra
期刊名称：Electronic Proceedings in Theoretical Computer Science
电子版ISSN：2075-2180
出版年度：2012
卷号：76
页码：163-177
DOI：10.4204/EPTCS.76.10
出版社：Open Publishing Association
摘要：This paper presents the derivation of an executable Krivine abstract machine from a small step interpreter for the simply typed lambda calculus in the dependently typed programming language Agda.