DESIGN AND VERIFICATION OF IFL: A WIDE-SPECTRUM INTERMEDIATE FUNCTIONAL LANGUAGE
Date
1991-07-01
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
A large number of functional languages have been developed in the last
decade. While semantic differences do occur between them, they differ
mainly in syntax. This thesis extracts a common basis for these languages
into an Intermediate Functional Language (IFL). IFL provides a portable,
high level form which reduces the overhead for implementing functional
languages. This is used to advantage by formally specifying and proving
a compiler from IFL to a low level language. The low level language may
then be targeted at either conventional or functional hardware. The SECD
machine is used as an example of the latter and a compiler from the low
level language to SECD machine code is specified and shown to be semantics
preserving. The result is a (partially) proven compiler from IFL to the
machine level. An optimization to the compiler is derived from the number
of times variables are referenced.
Description
Keywords
Computer Science