Journal article icon

Journal article

Linearity in higher-order recursion schemes

Abstract:

Higher-order recursion schemes (HORS) have recently emerged as a promising foundation for higher-order program verification. We examine the impact of enriching HORS with linear types. To that end, we introduce two frameworks that blend non-linear and linear types: a variant of the λY-calculus and an extension of HORS, called linear HORS (LHORS). First we prove that the two formalisms are equivalent and there exist polynomial-time translations between them. Then, in order to support model-chec...

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed

Actions


Access Document


Files:
Publisher copy:
10.1145/3158127

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Oxford college:
Worcester College
Role:
Author
Publisher:
Association for Computing Machinery Publisher's website
Journal:
Proceedings of the ACM on Programming Languages Journal website
Volume:
2
Issue:
POPL
Article number:
39
Publication date:
2017-12-27
Acceptance date:
2017-10-26
DOI:
ISSN:
2475-1421
Source identifiers:
745068
Keywords:
Pubs id:
pubs:745068
UUID:
uuid:cce934d2-53f2-4b37-a768-2d92e4a969e9
Local pid:
pubs:745068
Deposit date:
2017-11-11

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP