Personal tools
You are here: Home Events Abstract Archives 2000 Realizability models for BLL-like languages

Realizability models for BLL-like languages

Phil Scott University of Ottawa 4pm, Wednesday 7 June 2000 Room 2511, JCMB, King's Buildings

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.

Document Actions