Polynomial time and dependent types

Research output: Contribution to journalArticlepeer-review

33 Downloads (Pure)

Abstract

We combine dependent types with linear type systems that soundly and completely capture polynomial time computation. We explore two systems for capturing polynomial time: one system that disallows construction of iterable data, and one, based on the LFPL system of Martin Hofmann, that controls construction via a payment method. Both of these are extended to full dependent types via Quantitative Type Theory, allowing for arbitrary computation in types alongside guaranteed polynomial time computation in terms. We prove the soundness of the systems using a realisability technique due to Dal Lago and Hofmann.

Our long-term goal is to combine the extensional reasoning of type theory with intensional reasoning about the resources intrinsically consumed by programs. This paper is a step along this path, which we hope will lead both to practical systems for reasoning about programs’ resource usage, and to theoretical use as a form of synthetic computational complexity theory.
Original languageEnglish
Article number76
Pages (from-to)2288–2317
Number of pages30
JournalProceedings of the ACM on Programming Languages (PACMPL)
Volume8
Issue numberPOPL
DOIs
Publication statusPublished - 5 Jan 2024

Keywords

  • implicit computational complexity
  • linear logic
  • type theory

Fingerprint

Dive into the research topics of 'Polynomial time and dependent types'. Together they form a unique fingerprint.

Cite this