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...
Saved in:
| Main Authors: | , , , |
|---|---|
| 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 |