@inproceedings{da823293914649ea87b2b606a392257b,
title = "An approach to verifiable compiling specification and prototyping",
abstract = "A compiler may be specified as a set of theorems, each describing how a construct in the programming language is translated into a sequence of machine instructions. The machine may be specified as an interpreter written in the programming language itself. Using refinement algebra, it can then be verified that interpreting a compiled program is the same or better than executing the original source program. The compiling specification is very similar to a logic program and thus a prototype compiler (and interpreter) may easily be produced in a language such as Prolog. A subset of the occam programming language and the transputer instruction set are used to illustrate the approach. An advantage of the method is that new programming constructs can be added without necessarily affecting existing development work.",
author = "Jonathan Bowen and He Jifeng and Paritosh Pandya",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1990.; 2nd International Workshop on Programming Language Implementation and Logic Programming, PLILP 1990 ; Conference date: 20-08-1990 Through 22-08-1990",
year = "1990",
doi = "10.1007/bfb0024175",
language = "英语",
isbn = "9783540530107",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "45--59",
editor = "Pierre Deransart and Jan Maluszynski",
booktitle = "Programming Language Implementation and Logic Programming - International Workshop PLILP 1990, Proceedings",
address = "德国",
}