Formal Proof of a Machine Closed Theorem in Coq

The paper presents a formal proof of a machine closed theorem of TLA+ in the theorem proving system Coq. A shallow embedding scheme is employed for the proof which is independent of concrete syntax. Fundamental concepts need to state that the machine closed theorems are addressed in the proof platfo...

Full description

Saved in:
Bibliographic Details
Main Authors: Hai Wan, Anping He, Zhiyang You, Xibin Zhao
Format: Article
Language:English
Published: Wiley 2014-01-01
Series:Journal of Applied Mathematics
Online Access:http://dx.doi.org/10.1155/2014/892832
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1832552313008422912
author Hai Wan
Anping He
Zhiyang You
Xibin Zhao
author_facet Hai Wan
Anping He
Zhiyang You
Xibin Zhao
author_sort Hai Wan
collection DOAJ
description The paper presents a formal proof of a machine closed theorem of TLA+ in the theorem proving system Coq. A shallow embedding scheme is employed for the proof which is independent of concrete syntax. Fundamental concepts need to state that the machine closed theorems are addressed in the proof platform. A useful proof pattern of constructing a trace with desired properties is devised. A number of Coq reusable libraries are established.
format Article
id doaj-art-a87e44c578144db18265734b5bcd8e37
institution Kabale University
issn 1110-757X
1687-0042
language English
publishDate 2014-01-01
publisher Wiley
record_format Article
series Journal of Applied Mathematics
spelling doaj-art-a87e44c578144db18265734b5bcd8e372025-02-03T05:59:02ZengWileyJournal of Applied Mathematics1110-757X1687-00422014-01-01201410.1155/2014/892832892832Formal Proof of a Machine Closed Theorem in CoqHai Wan0Anping He1Zhiyang You2Xibin Zhao3School of Software, Tsinghua University, NLIST, KLISS, Beijing 100084, ChinaGuangxi Key Laboratory of Hybrid Computation and IC Design Analysis, Guangxi University for Nationalities, Nanning, Guangxi 530006, ChinaGeneral office of the Guangxi Zhuang Autonomous Region People’s Government, Nanning, Guangxi 530003, ChinaSchool of Software, Tsinghua University, NLIST, KLISS, Beijing 100084, ChinaThe paper presents a formal proof of a machine closed theorem of TLA+ in the theorem proving system Coq. A shallow embedding scheme is employed for the proof which is independent of concrete syntax. Fundamental concepts need to state that the machine closed theorems are addressed in the proof platform. A useful proof pattern of constructing a trace with desired properties is devised. A number of Coq reusable libraries are established.http://dx.doi.org/10.1155/2014/892832
spellingShingle Hai Wan
Anping He
Zhiyang You
Xibin Zhao
Formal Proof of a Machine Closed Theorem in Coq
Journal of Applied Mathematics
title Formal Proof of a Machine Closed Theorem in Coq
title_full Formal Proof of a Machine Closed Theorem in Coq
title_fullStr Formal Proof of a Machine Closed Theorem in Coq
title_full_unstemmed Formal Proof of a Machine Closed Theorem in Coq
title_short Formal Proof of a Machine Closed Theorem in Coq
title_sort formal proof of a machine closed theorem in coq
url http://dx.doi.org/10.1155/2014/892832
work_keys_str_mv AT haiwan formalproofofamachineclosedtheoremincoq
AT anpinghe formalproofofamachineclosedtheoremincoq
AT zhiyangyou formalproofofamachineclosedtheoremincoq
AT xibinzhao formalproofofamachineclosedtheoremincoq