CATEGORICAL MODELS OF COMPUTATION AND CODE GENERATION
Dr Alan Jeffrey, School of Cognitive and Computing Sciences, University of Sussex

Abstract: A common technique for compiling high level languages (for example ML or Haskell) down to lower-level languages (for example C or Java) is to use an intermediate language. The source language is translated into the intermediate language, and is then rewritten into a form which can be translated into the target language. This technique is used in (for example) SML/NJ and the Glasgow Haskell compiler.

This talk will cover some preliminary work in using categorical models of computation (notably Moggi monads and Power/Robinson adjunctions) to provide a mathematical basis for the rewrites performed on the intermediate language. The result of a compilation is not just object code, but also a proof of correctness of each of the intermediate rewrites.

This seminar was held at the Department of Computer Science, Royal Holloway, University of London on 9 April 1997.

back