状态效应与异常效应的 Hilbert-Post 完备性
计算机科学中的逻辑
2015-10-09 v3
摘要
本文提出了一种研究计算效应句法完备性的新框架，并将其应用于异常效应（exception effect）。当应用于状态效应（states effect）时，我们的框架可视为 Pretnar 在此主题上工作的推广。我们首先引入了一个相对形式的 Hilbert-Post 完备性概念，该概念非常适合效应的组合。随后，我们证明了异常效应及其用于实现的“核心”语言均具有相对 Hilbert-Post 完备性；这些证明已使用证明辅助工具 Coq 进行了形式化和验证。
引用
@article{arxiv.1503.00948,
title = {Hilbert-Post completeness for the state and the exception effects},
author = {Jean-Guillaume Dumas and Dominique Duval and Burak Ekici and Damien Pous and Jean-Claude Reynaud},
journal= {arXiv preprint arXiv:1503.00948},
year = {2015}
}
备注
Siegfried Rump (Hamburg University of Technology), Chee Yap (Courant Institute, NYU). Sixth International Conference on Mathematical Aspects of Computer and Information Sciences , Nov 2015, Berlin, Germany. 2015, LNCS