Hostname: page-component-7c8c6479df-5xszh Total loading time: 0 Render date: 2024-03-19T09:42:11.445Z 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

Abstract

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.

Type
Research Article
Copyright
© 1998 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)