Hostname: page-component-8448b6f56d-mp689 Total loading time: 0 Render date: 2024-04-23T12:38:26.942Z Has data issue: false hasContentIssue false

Normalization by evaluation with typed abstract syntax

Published online by Cambridge University Press:  28 November 2001

OLIVIER DANVY
Affiliation:
BRICS
Basic Research in Computer Science (www.brics.dk), funded by the Danish National Research Foundation.
, Department of Computer Science, University of Aarhus, Ny Munkegade, Building 540, DK-8000 Aarhus C, Denmark; (e-mail: danvy@brics.dk, mrhiger@brics.dk), (Home pages: http://www.brics.dk/~danvy, http://www.brics.dk/~mrhiger)
MORTEN RHIGER
Affiliation:
BRICS
Basic Research in Computer Science (www.brics.dk), funded by the Danish National Research Foundation.
, Department of Computer Science, University of Aarhus, Ny Munkegade, Building 540, DK-8000 Aarhus C, Denmark; (e-mail: danvy@brics.dk, mrhiger@brics.dk), (Home pages: http://www.brics.dk/~danvy, http://www.brics.dk/~mrhiger)
KRISTOFFER H. ROSE
Affiliation:
IBM T. J. Watson Research Center, 30 Saw Mill River Road, Hawthorne, NY 10532, USA; (e-mail: krisrose@us.ibm.com)
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.

In higher-order abstract syntax, the variables and bindings of an object language are represented by variables and bindings of a meta-language. Let us consider the simply typed λ-calculus as object language and Haskell as meta-language. For concreteness, we also throw in integers and addition, but only in this section.

Type
Functional Pearls
Copyright
© 2001 Cambridge University Press
Submit a response

Discussions

No Discussions have been published for this article.