Re: imperative-to-functional compiler

Patryk Zadarnowski <>
Tue, 18 Jan 2011 17:50:47 +1100

          From comp.compilers

Related articles
imperative-to-functional compiler (nojb) (2011-01-17)
Re: imperative-to-functional compiler (Patryk Zadarnowski) (2011-01-18)
Re: imperative-to-functional compiler (2011-01-18)
Re: imperative-to-functional compiler (Alain Ketterlin) (2011-01-18)
Re: imperative-to-functional compiler (Martin Ward) (2011-01-18)
| List of all articles for this month |

From: Patryk Zadarnowski <>
Newsgroups: comp.compilers
Date: Tue, 18 Jan 2011 17:50:47 +1100
Organization: Compilers Central
References: 11-01-074
Keywords: functional
Posted-Date: 18 Jan 2011 10:24:19 EST

Hi N,

On 18/01/2011, at 1:53 PM, nojb <> wrote:

> Suppose you want to translate an imperative language (e.g. a suitable
> subset of Pascal) into a functional language that does not have
> mutable variables (e.g. ML). Is this possible? What would be the
> algorithms/theory that would be relevant to handle the mutability of
> the variables on the Pascal side? Is SSA relevant?

It's certainly possible, and hugely useful, although a lot harder in practice
than some would have you believe.

In my PhD thesis ( I present a complete translation
of an unabridged ISO 9899:1989 (AKA "ANSI C", "C89", etc) into a sugared, but
pure version of lambda calculus and show that structuring an entire compiler
around such a translation can make its formal verification all but trivial (my
translation includes a complete formal semantics of C and a semi-formally
verified compiler into Knuth's MMIX binaries.)

An alternative route is to translate into SSA first, which is effectively
purely functional. Depending on your source language, pointers and arrays can,
however, make that approach infeasible, since SSA doesn't deal with them
particularly well. Also, from my experience, generating functional
representation of ALGOL languages directly tends to be easier than going
through SSA first, as it can be made syntax driven, even in presence of
unrestricted goto's.

Hope that helps,

Post a followup to this message

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