<p>The keywords you are looking for are "Implicit Computational Complexity". The field studies for instance variants of linear logic and the complexity bounds they can guarantee on the terms underlying the derivations.</p>

CC BY-SA 4.0
2018-10-25T15:27:15.573Z
Do you have any nice reference for the same? I would really like to understand this better?
Vinothkumar Raman
CC BY-SA 4.0
2018-10-26T04:18:01.403Z
@VinothkumarRaman I would look for the work of (Martin) Hofmann and (Jan) Hoffmann.
xrq
CC BY-SA 4.0
2018-10-25T10:30:41.193Z
2018-10-25T10:30:41.193Z
gallais
<p>Is there a type system, which restricts the lambda terms to the terms which fall inside a complexity class? Like the typable terms in the theory are strictly inside the complexity class ? Or is it not possible at all?</p>

<p>I find the there are lot of studies on expressibility of the type theory, like provably terminating, extended polynomials etc.. But is there any way to restrict that to a complexity class?</p>

CC BY-SA 4.0
2018-10-25T11:19:52.667Z
This topic is part of the area of Implicit Computational Complexity, where there are lots of results of that type. Type systems considered there are "ramified types" or variants of linear logic, e.g. Light Affine Logic or Soft Affine Logic.
Jan Johannsen
<complexity-classes><type-theory>
Type theory and computational complexity
Vinothkumar Raman
# Type theory and computational complexity

(Asked by: username_0 on 2018-10-25)

Is there a type system, which restricts the lambda terms to the terms which fall inside a complexity class? Like the typable terms in the theory are strictly inside the complexity class ? Or is it not possible at all?

I find the there are lot of studies on expressibility of the type theory, like provably terminating, extended polynomials etc.. But is there any way to restrict that to a complexity class?

**Tags:** complexity-classes, type-theory

> **Comments:**
> **username_1**: This topic is part of the area of Implicit Computational Complexity, where there are lots of results of that type. Type systems considered there are "ramified types" or variants of linear logic, e.g. Light Affine Logic or Soft Affine Logic.  

---

## 1 answers

### Answer by username_2 on 2018-10-25. Score: 10 | Accepted answer

The keywords you are looking for are "Implicit Computational Complexity". The field studies for instance variants of linear logic and the complexity bounds they can guarantee on the terms underlying the derivations.

> **Comments:**
> **username_0**: Do you have any nice reference for the same? I would really like to understand this better?  
> **username_3**: @VinothkumarRaman I would look for the work of (Martin) Hofmann and (Jan) Hoffmann.  

---

