Hostname: page-component-74656f9884-rdgjk Total loading time: 0 Render date: 2026-11-09T08:01:36.654Z Has data issue: false hasContentIssue false

An environment machine for the λμ-calculus

Published online by Cambridge University Press:  01 December 1998

PHILIPPE de GROOTE
Affiliation:
INRIA-Lorraine, 615 rue du Jardin Botanique – B.P. 101, F 54602 Villers-lès-Nancy Cedex – FRANCE. E-mail: Philippe.de.Groote@loria.fr
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

We introduce a natural deduction-like formalisation of Parigot's λμ-calculus. From this, we derive an environment machine that allows any well-typed λμ-term to be reduced to its weak head normal form. The soundness and completeness of the machine is proved.

Information

Type
Research Article
Copyright
© 1998 Cambridge University Press