Abstract

Bounded Linear Logic (Girard,Scedrov,Scott,in TCS '92) was an early attempt to give an intrinsic notion of polynomial time computation within a logical system, using the Curry-Howard idea of "computation via cut-elimination ". It is based on a second-order version of intuitionistic linear logic, with a notion of "bounded exponential", allowing us to express the idea of bounded calls to memory. The fact that exactly Cobham's class of polytime functions are representable in BLL is technically very difficult, using a detailed analysis of proof-nets with boxes, and a special evaluation strategy.

In this paper, we give a realizability model for BLL-like languages, and a new proof that all numerical functions representable in the system are polytime. The model also highlights particular features of the syntax of BLL and suggests new rules and further extensions.

This is joint work with Martin Hofmann.