Loading...
Please wait, while we are loading the content...
Similar Documents
Coinductive Natural Semantics for Compiler Verification in Coq
| Content Provider | MDPI |
|---|---|
| Author | Angel, Zúñiga Bel-Enguix, Gemma |
| Copyright Year | 2020 |
| Description | (Coinductive) natural semantics is presented as a unifying framework for the verification of total correctness of compilers in Coq (with the feature that a verified compiler can be obtained). In this way, we have a simple, easy, and intuitive framework; to carry out the verification of a compiler, using a proof assistant in which both cases are considered: terminating and non-terminating computations (total correctness). |
| Starting Page | 1573 |
| e-ISSN | 22277390 |
| DOI | 10.3390/math8091573 |
| Journal | Mathematics |
| Issue Number | 9 |
| Volume Number | 8 |
| Language | English |
| Publisher | MDPI |
| Publisher Date | 2020-09-12 |
| Access Restriction | Open |
| Subject Keyword | Mathematics Logic Natural Semantics Big-step Semantics Coinduction Compiler Verification Total Correctness Mini-ml Secd Machine Coq Proof Assistant |
| Content Type | Text |
| Resource Type | Article |