Abstract
A methodology for the verification of compiler correctness based on the LF logical framework as realized within the Elf programming language is presented. This technique is used to specify, implement, and verify a compiler from a simple functional programming language to a variant of the Categorical Abstract Machine (CAM).
| Original language | English (US) |
|---|---|
| Title of host publication | Proceedings - Symposium on Logic in Computer Science |
| Publisher | Publ by IEEE |
| Pages | 407-418 |
| Number of pages | 12 |
| ISBN (Print) | 0818627352 |
| State | Published - Jun 1992 |
| Event | Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science - Santa Cruz, CA, USA Duration: Jun 22 1992 → Jun 25 1992 |
Other
| Other | Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science |
|---|---|
| City | Santa Cruz, CA, USA |
| Period | 6/22/92 → 6/25/92 |
All Science Journal Classification (ASJC) codes
- General Engineering