Abstract
The graph rewriting system of interaction nets has been very successful for the implementation of the lambda calculus. In this paper we show how the ideas can be extended and simplified to encode Gödel’s System T —the simply typed λ-calculus extended with numbers. Surprisingly, using some results about System T, we obtain a very simple system of interaction nets that is significantly more efficient than a direct encoding for the evaluation of programs.
Cite
CITATION STYLE
Mackie, I., & Sato, S. (2016). An interaction net encoding of Gödel’s System T declarative pearl. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9613, pp. 80–93). Springer Verlag. https://doi.org/10.1007/978-3-319-29604-3_6
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
