A geometry of interaction machine for Gödel's System T

Mackie, Ian (2017) A geometry of interaction machine for Gödel's System T. Published in: Kennedy, Juliette and de Queiroz, Ruy J G B, (eds.) Proceedings of the 24th International Workshop on Logic, Language, Information, and Computation; London, UK; 18-21 July 2017. 10388 229-241. Springer Verlag ISSN 9783662553855 ISBN 0302-9743

[img] PDF - Accepted Version
Download (264kB)

Abstract

Gödel’s System T is the simply typed lambda calculus extended with numbers and an iterator. The higher-order nature of the language gives it enormous expressive power—the language can represent all the primitive recursive functions and beyond, for instance Ackermann’s function. In this paper we use System T as a minimalistic functional language. We give an interpretation using a data-flow model that incorporates ideas from the geometry of interaction and game semantics. The contribution is a reversible model of higher-order computation which can also serve as a novel compilation technique.

Item Type: Conference Proceedings
Schools and Departments: School of Engineering and Informatics > Informatics
Research Centres and Groups: Foundations of Software Systems
Depositing User: Ian Mackie
Date Deposited: 17 Jul 2017 12:25
Last Modified: 17 Jul 2017 13:04
URI: http://srodev.sussex.ac.uk/id/eprint/69302

View download statistics for this item

📧 Request an update