Correctness Proofs of Compilers

Dave Berry <db@dcs.ed.ac.uk> writes:


> We've done some work on producing tools from operational semantics. In
> our case we've looked at debuggers (which are harder than compilers). In
> my thesis I looked at the definition of evaluation step in terms of
> operational semantics, and described a system that generated animating
> interpreters from an operational semantics. Fabio da Silva is just
> completing his thesis on another, more rigorous, approach. He includes an
> algorithm from generating a deterministic semantics from a certain class
> of non-deterministic semantics.




This is to announce the availability of a report in which I summarise the
main results of my PhD Thesis. My thesis should also become available in
a few weeks. Both report and thesis can be obtained from Lorraine Edgar
(lme@dcs.ed.ac.uk). If anyone else is interested in the issues of
correctness proofs of compilers and debuggers I will be very glad to
exchange ideas and experiences.


@TechReport{,
    author = "Fabio Q. B. da Silva",
    title = "Correctness Proofs of Compilers and Debuggers: an
Overview of an Approach Based on Structural
Operational Semantics",
    institution = "LFCS, Department of Computer Science, University of
Edinburgh",
    year = "1992",
    OPTtype = "",
    number = "ECS-LFCS-92-233",
    address = "Edinburgh, EH9 3JZ, Scotland",
    month = "September",
    OPTnote = ""
}




@PhdThesis{,
    author = "Fabio Q. B. da Silva",
    title = "Correctness Proofs of Compilers and Debuggers: an
Approach Based on Structural Operational Semantics",
    OPTschool = "LFCS, Department of Computer Science, University of
Edinburgh",
    year = "1992",
    OPTaddress = "Edinburgh, EH9 3JZ, Scotland",
    OPTmonth = "",
    note = "Thesis submitted for the degree of Ph.D., LFCS, Department
of Computer Science, University of Edinburgh,
Edinburgh, EH9 3JZ, Scotland"
}




Fabio
--
Fabio Q. B. da Silva


University of Edinburgh JANET: fabio@uk.ac.ed.dcs
LFCS - Computer Science Dept. UUCP: ..!mcsun!ukc!lfcs!fabio
JCMB - The King's Buildings ARPA: fabio%dcs.ed.ac.uk@nsfnet-relay.ac.uk
Mayfield Road - Edinburgh
EH9 3JZ - Scotland
--

Return to the comp.compilers page.
Search the comp.compilers archives again.