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
![]() |
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