Simpson, Todd G.2008-05-202008-05-201991-07-01http://hdl.handle.net/1880/46533A 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.EngComputer Scienceunknown1991-440-2410.11575/PRISM/31303