文章基本信息

标题：Program Extraction from Proofs of Weak Head Normalization
本地全文：下载
作者：Malgorzata Biernacka ; Olivier Danvy ; Kristian Støvring 等
期刊名称：BRICS Report Series
印刷版ISSN：0909-0878
出版年度：2005
卷号：12
期号：12
出版社：Aarhus University
摘要：We formalize two proofs of weak head normalization for the simply typed lambda-calculus in first-order minimal logic: one for normal-order reduction, and one for applicative-order reduction in the object language. Subsequently we use Kreisel's modified realizability to extract evaluation algorithms from the proofs, following Berger; the proofs are based on Tait-style reducibility predicates, and hence the extracted algorithms are instances of (weak head) normalization by evaluation, as already identified by Coquand and Dybjer.