@MISC\{IMM2007-05345,
    author       = "K. Svendsen",
    title        = "Analyzing Action Semantics",
    year         = "2007",
    publisher    = "Informatics and Mathematical Modelling, Technical University of Denmark, {DTU}",
    address      = "Richard Petersens Plads, Building 321, {DK-}2800 Kgs. Lyngby",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/5345-full.html",
    abstract     = "Programmers usually assume that when they compile a program, the behavior of the generated code corresponds to the semantics assigned to the program by the programming language. However, writing a correct compiler, that generates reasonably efficient code, is a difficult and expensive task. A lot of research has therefore focussed on automatically generating complete compilers from formal specifications of languages. In some cases, even with an accompanying proof of correctness of the generated compiler.

In this thesis we develop a tool for analyzing semantic descriptions of programming langauges, specified in a subset of the semantic description language, Action Semantics. The purpose of the tool is to function as a component of a compiler generator.

The tool implements two analyses: The first analysis is a type and termination analysis, which annotates semantic descriptions with type information about the values, that programs written in the described language can produce. The second analysis analyzes the use of bindings in the languages specification, to generate a bindings analysis for the source language."
}