The $\nabla$ -Calculus. Functional Programming with Higher-Order Encodings
- 1 January 2005
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
- p. 339-353
- https://doi.org/10.1007/11417170_25
Abstract
Higher-order encodings use functions provided by one language to represent variable binders of another. They lead to concise and elegant representations, which historically have been difficult to analyze and manipulate. In this paper we present the \(\nabla\)-calculus, a calculus for defining general recursive functions over higher-order encodings. To avoid problems commonly associated with using the same function space for representations and computations, we separate one from the other. The simply-typed λ-calculus plays the role of the representation-level. The computation-level contains not only the usual computational primitives but also an embedding of the representation-level. It distinguishes itself from similar systems by allowing recursion under representation-level λ-binders while permitting a natural style of programming which we believe scales to other logical frameworks. Sample programs include bracket abstraction, parallel reduction, and an evaluator for a simple language with first-class continuations.
Keywords
This publication has 7 references indexed in Scilit:
- Inductive definitions in the system Coq rules and propertiesPublished by Springer Science and Business Media LLC ,2005
- The $\nabla$ -Calculus. Functional Programming with Higher-Order EncodingsLecture Notes in Computer Science, 2005
- Primitive recursion for higher-order abstract syntaxTheoretical Computer Science, 2001
- Recursion for Higher-Order EncodingsLecture Notes in Computer Science, 2001
- Theoretical Computer Science, 2001
- MetaML and multi-stage programming with explicit annotationsTheoretical Computer Science, 2000
- An algorithm for testing conversion in type theoryPublished by Cambridge University Press (CUP) ,1991