Type-And-Scope Safe Programs And Their Proofs
POPL(2017)
摘要
We abstract the common type-and-scope safe structure from computations on lambda-terms that deliver, e.g., renaming, substitution, evaluation, CPS-transformation, and printing with a name supply. By exposing this structure, we can prove generic simulation and fusion lemmas relating operations built this way. This work has been fully formalised in Agda.
更多查看译文
关键词
Lambda-calculus,Mechanized Meta-Theory,Normalisation by Evaluation,Semantics,Generic Programming,Agda
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要