Isabelle中函数逻辑编程语义的形式化
计算机科学中的逻辑
2009-08-05 v1
摘要
现代函数逻辑编程语言（如Toy或Curry）具有非严格非确定性函数，这些函数在调用时选择语义下运行。该语义的标准表述是CRWL逻辑，它指定了一个用于计算每个表达式可能结果集的证明演算。本文在Isabelle/HOL证明助手中对该演算进行了形式化。我们证明了CRWL的一些基本性质：在c-替换下的封闭性、极性以及组合性。我们还讨论了一些已获得的见解，例如程序规则的左线性对于这些结果的成立并非必要。
引用
@article{arxiv.0908.0494,
title = {A Formalization of the Semantics of Functional-Logic Programming in Isabelle},
author = {Francisco López Fraguas and Stephan Merz and Juan Rodríguez Hortalá},
journal= {arXiv preprint arXiv:0908.0494},
year = {2009}
}