Department of Computer Science
King's College, London
4pm Tuesday 19 October 2004
Room 2511, JCMB, King's Buildings
We present an efficient implementation of the lambda-calculus using the graph rewriting formalism of interaction nets. Building upon a series of previous works, we obtain one of the most efficient implementations of this kind to date: out performing existing interaction net implementations, as well as other approaches. The evaluator is capable of producing full normal forms of typed or untyped terms (either open or closed), and thus opens up additional applications such as the use in proof assistants, where normal forms of such terms are often required. We conclude with extensive testing to demonstrate the capabilities of this evaluator.