Realizability models for BLL-like languages.
We give a realizability model of Girard-Scedrov-Scott's Bounded Linear Logic (BLL). This gives a new proof that all numerical functions representable in that system are polytime. Our analysis naturally justifies the design of the BLL syntax and suggests further extensions.
Introduction
Bounded Linear Logic (BLL) [3] was an early attempt to provide an intrinsic notion of
polynomial time computation within a logical system. That is, the aim was not merely to
express polynomial time computability in terms of provability of certain restricted formulas,
but rather to provide a typed logical system in which computation via cut-elimination or
proof normalization is inherently polytime. Since the appearance of this paper, several
di#erent typed functional systems for analyzing ptime computability have appeared in the
literature [5, 4, 10, 11, 6, 7]. For deeper foundational purposes, we should mention Girard's
Light Linear Logic (LLL) [4] as a major improvement of the syntax of BLL, in that it
eliminates the explicit polynomial I/O size-bounds, but at the expense of introducing more
subtle typing distinctions. Moreover, while capturing the same extensional class of polytime
functions, it appears to be less flexible than BLL in terms of expressing concrete algorithms.
Furthermore BLL has its own merits: from the viewpoint of computer science, BLL is a
natural polymorphically-typed functional language in which bounded storage can represent
bounded calls to memory.
The main theorem in [3] is that the number-theoretic functions representable in BLL
are polytime. The proof of this result used sophisticated techniques from the proof theory
of linear logic, notably a very detailed analysis of normalization of proof nets with boxes.
The normalization strategy itself was of a special kind, inspired from Girard's Geometry
of Interaction program. In this paper, we give a direct, semantic proof of this main result
which does not involve any notion of reduction, term rewriting, or cut-elimination. Rather,
we assign polytime algorithms to proofs in a compositional, syntax-directed manner. We use
Research partially supported by EPSRC grant No. GR/N28436
Research supported by an operating grant from the Natural Sciences and Engineering Research Council
of Canada.
realizability to relate these algorithms to the intended set-theoretic meaning of the proofs
themselves. All this is presented in the form of a concrete categorical model of BLL which
interprets BLL-formulas as sets with some additional structure and proofs as functions witnessed
by polytime algorithms operating on this additional structure. At the same time, our
analysis gives a natural interpretation of the BLL syntax which justifies the fine points of
its design and might suggest further extensions. For example, our analysis encompasses an
a#ne variant of BLL.
Our proof is constructive, in the sense that it can be formalized in an extensional version
of the Calculus of Inductive Constructions [2]. This provides a new compilation method for
turning BLL proofs into equivalent polytime algorithms. Of course in practice one would
not use such a formalization, but rather derive the compilation algorithm by hand directly
from our proof.
Our interpretation bears an intriguing relationship to approaches based on finite model
theory, such as [5]. Namely, the polytime functions we obtain are of the form of Goerdt-
Gurevich's total global functions: they take one extra argument which is interpreted as a
bound on the size of all the actual inputs. However, unlike Goerdt's system which is a finite
model interpretation of G-odel's system T -hence the successor function is not injective- BLL
supports the usual semantics, including Peano's axioms, thus can be seen as a meaning-preserving
annotation to standard functional programming. We hope that this relationship
can be used to transfer Goerdt's characterizations of LOGSPACE and PSPACE to a similar
setting.
Bounded Linear Logic
We introduce the theory BLL of bounded linear logic, first proposed in [3]
2.1 Resource Polynomials
Resource polynomials [3] are finite sums of products of binomial coe#cients, i.e. P j#q Q i#p  x ij
where, for any fixed j, the variables x ij are distinct and n ij are non-negative integer constants

Resource polynomials are closed under sum, product, and composition. Given such
polynomials p, q write p # q to denote that q - p is a resource polynomial. If p # p # and
2.2 Syntax of BLL
are given by the following general syntax:
Here atomic formulae have the form #(p 0 , . , p n-1 ) , where # is a second-order variable of
given finite positive arity n and # list of resource polynomials
of length n. We assume that there are infinitely many second-order variables of each finite
arity.
The formula #.A denotes second order universal quantification, while ! x<p A is bounded
storage, where p is a resource polynomial not containing x and x is bound in ! x<p A.
Positive and negative occurrences of resource terms in formulae are defined by induction
as usual: in ! x<p A, p occurs negatively. The p i and their subterms occur positively in an
atomic formula #p). The
connectives# and # are monotone; the connective -# is antitone
in its first and monotone in its second argument so that for example, p occurs positively in
Let the free resource variables x 0 , . , x n-1 occur only positively in B. Then
is a (second order) abstraction term, say T . A[# := T ] denotes the result
of substituting T for # in A , i.e. of replacing the atoms #(p 0 , ., p n-1 ) in A by
Given types A and A # , write A # A # if A and A # only di#er in their choice of resource
polynomials, and
(i) for any positive occurrence of resource polynomial p in A, the homologous p # in A # is
such that p # p # .
(ii) for any negative occurrence of resource polynomial p in A, the homologous p # in A # is
such that p # p.
If # and # are finite multisets of formulae, # i# it is true componentwise.
Proofs are given by Gentzen sequents, as follows.
2.3 BLL Sequents
Sequents have the form # B , where # is a finite (possibly empty) multiset of formulae.
In order to avoid mentioning the permutation rule, the formulae in # are considered indexed
but not ordered. In what follows, p, q, w (possibly with subscripts) range over resource
polynomials.
Axiom (Waste of Resources) A # A # , where A # A # (Special case: A # A ).
Cut
# A #, A # B
#,
#, A -# B # C -#R
#, A # B
#, A[# := T
#.A
(provided # is not free in #)
Dereliction
#, A[x := 0] # B
Contraction
A.
(S!) Storage
and where all formulae to the left
of the # have the indicated form.
Remark 2.1
. The rules of BLL are written in such a way that given any proof # of a sequent # A
and given any # and A # A # then a simple change of resource parameters will
yield a proof # of # A # without altering the structure of the proof.
Note that the "waste" w in each of the rules associated with storage can without
loss of generality be assumed 0 as the general case can be recovered by cutting with
appropriate axioms. In this paper we are not interested in cut elimination, therefore,
we will adopt this simplification.
. We also introduce a unit
for# , denoted I. The ordinary LL rules for I are as follows:
#, I # B # I
. The data type of tally natural numbers of size at most x is:
Moreover, there are proofs representing "zero" and
"successor", resp. (see [3]).
. The data type of dyadic lists of size at most x is:
There are proofs # : N 2
representing zero and the two successor
functions, resp. (see [3]).
The following two rules are not contained in the definition of BLL [3], and as far as we can
see are not admissible in BLL.
These rules express functoriality and monoidalness of ! x<p . Note that they can be subsumed
under the following generalization of
Our semantics validates these rules, so as a result their addition does not increase the
computational strength of BLL. We note that in their presence the storage rule can be
replaced by the following axiom:
#<x
3 Main Result
We shall assume that our ambient set theory is constructive, so that we shall have a set
(of sets) U containing the natural numbers N , closed under product, function space, and
U-indexed products [9]. We discuss this point in more detail below in Section 5. This allows
us to interpret types as sets in the following way: given a formula A and an environment #
which assigns sets to type-variables, we obtain a set-theoretic interpretation A # as follows:
#p) #)
Notice that this interpretation of types ignores the resource polynomials.
To every proof # of a sequent A 1 , - , A n # B and environment #, we can assign a
set-theoretic function
1# .
by induction on derivations, in the obvious way. Observe that
C#U
There is a pair of functions # defined
as follows:
where in the definition of #, the symbols S and 0 are the usual successor and zero on N .
Note that #
Our main goal is to give a new proof of the following theorem, which is equivalent to
Theorem 5.4 in [3]:
Theorem 3.1 Let # be a proof of # N x -# N p(x) , where p does not contain any other free
resource variables except x. Let f : N # N be the function:
Then: f(n) is computable in polynomial time in n. Moreover, f(n) # p(n). and an algorithm
for f can be e#ectively obtained from the proof #.
An analogous result holds for the type of dyadic lists, as in Theorem 5.3 of [3].
4 A Realizability Model for BLL
We now introduce a refined model B for BLL based on realizability and ideas from [6].
This will allow us to obtain the above theorem as a direct corollary of soundness of the
interpretation. See the proof after Theorem 4.21.
4.1 Preliminaries
For x # N , we write for the binary length of x. We fix a linear time
computable pairing function # : N# N satisfying |#x,
We should also remark that the inverses of the pairing function are assumed to be linear
time computable.
Let X be a finite set of variables. We write V(X) for N X -the elements of V(X) are
called valuations (over X). If # V(X) and c # N then #[x # c] denotes the valuation which
maps x to c and acts like # otherwise. We assume some reasonable encoding of valuations
as integers allowing them to be passed as arguments to algorithms.
We write P(X) for the set of resource polynomials over X. If p # P(X) and # V(X)
we write p(#) for the number obtained by evaluating p with x #(x) for each x # X.
Let X, Y be finite sets of variables. A substitution from X to Y is a function
P(X). We may write a substitution from X to in the form
This is defined if p i # P(X) and in this case we have
. If the domain X is clear from the context, we may simply write
A substitution # from X to Y induces functions #(-)
in the obvious way, i.e., (#))(y)
We assume known the untyped lambda calculus as defined e.g. in [1]. An untyped
lambda term is a#ne linear if each variable (free or bound) appears at most once (up
to #-congruence). E.g. #x#y.yx and #x#y.y and #x.xy are a#ne linear; the term #x.xx is
not. Notice that such a term t is strongly normalisable in less than |t| steps where |t| is the
size of the term. The runtime of the computation leading to the normal form is therefore
O(|t| 2 ). We will henceforth use the expression a#ne lambda term for an untyped a#ne linear
lambda term which is in normal form. If s, t are a#ne lambda terms then their application
st is defined as the normal form of the lambda term st. Notice that the application st can
be computed in time O((|s|
If s, t are a#ne lambda terms we write
s# t for the a#ne lambda term #f.fst. If t is
an a#ne lambda term possibly containing the free variables x, y then we write
#x# y.t for
#u.u(#x#y.t). Notice that
(#x# y.t)(u#
More generally, if (t i ) i<n is a family of a#ne lambda terms, we write N i<n t i for
Tally natural numbers may be encoded as a#ne lambda terms by
#xy.x#xy.x
(#xy.y)# pnq. Dyadic lists may be encoded as
#xyz.x#xy.x and
#xyz.y# pwq and
#xyz.z# pwq.
We notice that pnq, resp. pwq can be computed in linear time from n, resp.
vice versa. Of course, only a few functions f on natural numbers or dyadic lists can be
represented by a#ne terms t in the sense that
We write # a for the set of closed a#ne lambda terms. Our subsequent development will be
modular in the sense that # a can be replaced by any other polynomial-time computable BCK-
algebra in the sense of [7]. For example, we can take Turing machines with the application
defined by ex = {e}(x) if this result can be obtained in time at most #(d(#(e) + #(x))) and
otherwise. Here # is a length function defined inductively by #x,
otherwise. The defect d is #(e) and we additionally require
Finally, # is a monotone, sublinear function satisfying #(x)) # |x|.
For example,
4.2 Realizability Sets
Definition 4.1 Let X be a finite set of resource variables. A realizability set over X is a
is a set and || A # V(X) - # a - |A| is a ternary relation
between valuations over X, a#ne lambda terms, and the set |A|. We write #, t || A
a for
(#, t, a) # || A
The intuition behind #, t || A
a is that a is an abstract semantic value, # measures the
abstract size of a, and the a#ne lambda term t encodes the abstract value a.
Example 4.2 The following are some useful examples of realizability sets, cf. Section 5 of
[3].
(i) The realizability set N x over {x} of tally natural numbers ("of size at most x") is
defined
#, t || Nx
(ii) The realizability set N 2
x over {x} of dyadic lists ("of length at most x") is defined by:
#, t || N 2
x
(iii) The realizability set I over # is defined by |I| = {#} and #x.x || I #
(iv) Given a substitution # from X to Y , and a realizability set A over Y , then a new
realizability set A[#] over X is defined
#, t || A[#]
a i#), t || A
a
The sets N x and N 2
x will turn out to be retracts of the denotations of the eponymous BLL
formulas in our model.
In order to model the notion of positive occurrence of a resource variable in BLL formulas
we introduce a corresponding concept for realizability sets.
Definition 4.3 Let A be a realizability set over X. We say that positive (resp.
negative) in A, if for all # V(X), t # a , a # |A| where # and # agree on X \ {x} and
a implies # , t || A
a.
We notice that x is positive in N x and N 2
x .
Definition 4.4 Let A, B be realizability sets over some set X. A morphism from A to B is
a function f : |A| # |B| satisfying the following condition:
There exists a function e : V(X) # a such that e(#) is computable in time q(#) for
some resource polynomial q and for each # V(X), t # a , a # |A|, we have
#, t || A
a #, e(#)t || B
f(a)
(1)
In this case we say that e witnesses f and write A f
e
in the notation the algorithm
e is presumed to exist.
Example 4.5 The following are some useful examples of numerical-valued morphisms:
. A morphism f : N x # N x is a function f : N # N that is computable in time
polynomial in the input n (not in |n|). Moreover, it satisfies f(n) # n (by letting
. Similarly, a morphism f : N 2
x is a function f : {0, 1} # {0, 1} # that is polytime
computable (in the usual sense) and moreover satisfies lh(f(w)) # lh(w).
. Let p(x) be a unary resource polynomial in x and let # be the substitution [{x}; x := p].
A morphism f : N x # N x [#] is a function f : N # N that is polytime computable
in the input (as above) for which f(n) # p(n). Composed with the above-mentioned
retractions, these morphisms will be denotations of closed proofs of # N x -# N p(x) .
The following lemma illustrates how realizability sets model the syntactical iteration lemma
for BLL (cf. Lemma 6.2 of [3]).
Lemma 4.6 (Iteration Lemma) Let T be a realizability set over {x} such that x is positive
in T . Let z : I # T [x := 0] be a morphism (over #) and let be a
morphism (over {x}). The function f : N # |T | defined by
from N x to T .
Proof. The witnesses of z, s give rise to an element e z # a and to a function e s
such that
and for each n # N ,
This is because by definition of substitution we have
#, t || T [x:=0]
We now have
whenever n # N . This follows by induction on n and the fact that x is positive in T .
We define e recursively by
It follows that
provided that n # N .
Furthermore, it is easy to see that e is polytime given that we have e(N
fixed P # a (independent of N ).
Therefore, # e(#(x)) witnesses the function
The following analogous version for dyadic lists (cf. Lemma 6.2 of [3]) is proved similarly.
Lemma 4.7 (Iteration lemma for dyadic lists) Let T be a realizability set over {x}
such that x is positive in T . Let z : I # T [x := 0] be a morphism (over #) and let
morphisms (over {x}). The function f : {0, 1} # |T | defined
by a morphism from N 2
x to T .
We remark that one can also prove more general versions of the preceding iteration lemmas
allowing for extra resource variables in T as parameters.
Proposition 4.8 Let X be a finite set (of resource variables). Realizability sets over X and
morphisms between them form a category B(X) such that the mapping
|A| extends to a functor from B(X) to the category Set of sets. This means that composition
in B(X) is given by ordinary set-theoretic composition of functions.
Proof. The identity function id : |A| # |A| is witnessed by the algorithm e(#x.x which
is clearly polytime computable.
If A 0
f
then the composition g | can be witnessed
by
#xyz.x(yz). Now e is polytime using the fact that application in # a is polytime.
Recall the definition in Example 4.2 of the realizability set A[#] over X when A is a
realizability set over Y and # is a substitution from X to Y .
Proposition 4.9 Let # be a substitution from X to Y . The assignment A # A[#] extends
to a functor
Proof. We have to show that if A f
e
then we can find e # so that A[#] f
Unfolding the definitions reveals that e #) = e(#)) does the job. #
This allows us to consider morphisms between realizability sets over di#erent sets of resource
variables. Namely, if X # Z we have a "weakening substitution" weak X,Z from Z to X given
by weak X,Z A is a realizability set over X and B is a realizability set over
Y we can consider morphisms from A[weak X,X#Y ] to B[weak Y,X#Y ]. Such a morphism is a
|B| such that there exists an algorithm e : V(X #Y ) # a such that e(#)
is computable in time q(#) for some resource polynomial q and
a #| Y , e(#)t
where #| X denotes the restriction of # to X. We shall sloppily refer to such morphisms as
being morphisms from A to B. In this sense, the only morphism from N x to N y where x #= y
is the constant zero function.
The following is immediate:
Lemma 4.10 Suppose that A # B(Y ) is a realizability set and are substitu-
tions. Suppose furthermore that #(y) # (y) if y occurs positively in A, that #(y) # (y)
if y occurs negatively in A, and that otherwise. Then the identity function is a
morphism from A[#] to A[# ].
4.3 The Category of Realizability Sets
We will now show that the categories B(X) have the appropriate categorical structure to
model the BLL connectives.
Definition 4.11 We define the following monoidal structure on B(X):
. I = (|I|, || I
arbitrary.
. If A 1 , A 2 are realizability sets over X we define A
1# A 2 by |A
#, t || A
a i for 2.
Proposition 4.12 Let f : A # B be a B(X) morphism, C # B(X). Then
i) The function
|B# C| defined by
(f# C)(a, c) = (f(a), c) is a
morphism from
A# C to
B# C.
ii) The canonical set-theoretic maps
|A# (B# C)| #
|(A# B)# C|,
|B# A|,
and
|A# I| # |A| induce isomorphisms between the associated objects.
iii) For appropriately typed substitution I and
This says in particular that B(X) is a symmetric monoidal category, and the forgetful functor
# Set is a monoidal functor. Clause (iii) states that substitution is a monoidal func-
tor. This says that the collection of the categories B(X) forms a fibred symmetric monoidal
category in the sense of [14].
Proof. Ad i). If e witnesses f then we define e
#x# y.e(#)x# y. Obviously, e # witnesses
f# C and, since e a the function e # is polytime. The other cases
are analogous. #
Proposition 4.13 For any two objects A, B # B(X), there is a linear function space object
a then #, t t # || B
f(a).
This structure makes B(X) a symmetric monoidal closed category, i.e. there is a natural
bijection
that -[#] is a monoidal closed functor.
Proof. The evaluation map
|A# by (a, f) # f(a) is witnessed by
#x# y.yx. If
C# A f
e
is witnessed by e
#xy.e(#)(x# y). Just as in Prop. 4.12, i) we have e
some P # a , which establishes that e # is polytime. #
We notice that the forgetful functor B(X) # Set is also monoidal closed, i.e.
sends# to -
and -# to #.
Definition 4.14 Given a polynomial p # P(X) and a realizability set A over X#{x} where
then we define a realizability set ! x<p A over X (i.e. x is "bound" by ! x<p ) by
. |! x<p
. #, t || ! x<pA
a if
a for each i < p(#).
Whenever we write ! x<p A in the sequel we implicitly assume that x does not occur in p.
Proposition 4.15 If f : A # B # B(X # {x}) is a morphism then ! x<p (f) def
f is a
This says that ! x<p extends to a functor from B(X # {x}) to
B(X) which is mapped to the identity by the forgetful functor to Set.
Proof. If A
f
e
then we can witness
We notice that
| {z }
p(#) times
for some P # a so that e #) is computable in time O((p(#)q(#)) 2 ) if e(#) is computable in
O(q(#)). Note that this is a rather generous estimate. #
We now show that we have the appropriate categorical structure to interpret the rules of
BLL.
Proposition 4.16 The following are morphisms:
where dA (a) = (a, a)
and x, y are fresh
(A# B)
Proof. The map # A can be witnessed by e(# N i<1 x i .x 0 . The map e A may be witnessed
by e(#y.#x.x. The map dA may be witnessed by
O
To see this, assume #, t || ! x<p+qA
a. Then
for each i < p(#) we have #[x#i], t i || A
a, so #, N i<p(#) t i
a. Moreover, for each
a, hence #[y#j], t j+p(#) || A[x:=p+y]
a. Therefore,
#,
a, so the result follows.
Next, # A may be witnessed by
O
O
The verification is similar to the one of dA .
Finally, # A,B may be witnessed by
x
O
We omit the "waste" morphism wA , which is obvious. #
4.4 Interpreting the Syntax in B
We shall now give the details of the interpretation of the syntax of BLL in terms of realizability
sets and morphisms between them.
Definition 4.17 Let X be a set of resource variables. A second-order environment over X
is a partial function # which assigns to a second-order variable # of arity n a pair (l, C) such
. list of n pairwise di#erent resource variables not occurring in X,
. C is a realizability set over X # {y 0 , . , y n-1 } in which the y i are positive.
For second-order environment # we write |#| for the mapping # |C| when #) = (l, C).
Y is a substitution and # is a second-order environment over Y we define a
second-order environment #] over X by C). We assume
here that the variables in l are not contained in Y . Otherwise, the substitution cannot be
defined.
Recall the set-theoretic semantics - defined in Section 3. From now on, we will write
- Set for this set-theoretic semantics to distinguish it from a realizability semantics - B
which we now define.
Let A be a BLL formula with free resource variables in X and # be an environment
over X defined on all free second-order variables occurring in A. We assume without loss of
generality that all bound variables in A and in # are distinct from each other.
By induction on A we define a realizability set A B # such that
|#|
The defining clauses are as follows:
where
#, t || #A B #
f |C| for all (l, C) as in Def. 4.17
The following lemmas are immediate by structural induction.
Lemma 4.18 Let # be a substitution from X to let A be a BLL
formula with free resource variables from Y and let # be an environment over Y such that
#] is defined. Then
Lemma 4.19 Let A be a BLL formula possibly containing the second-order variable # of
be a BLL formula containing free resource variables {y 0 , . , y n-1 } which do
not occur in A. Then
Lemma 4.20 Let A be a BLL formula in which resource variable x occurs positively (resp.
negatively) and # be an appropriate second-order environment. Then x is positive (resp.
negatively) in A B # .
Theorem 4.21 (Soundness) Let # be a proof of a sequent A 1 , - , A n # B involving resource
variables from X. Let # be a second-order environment binding all the second-order
variables occurring in the sequent. Then the set-theoretic function
1# .
|#|
|#|
is a morphism of realizability sets from A
1# .
. Recall that A
1# .
| A
1# .
Proof. By induction on BLL derivations using using Lemma 4.10 for the axiom; using
Propositions 4.12, 4.13, 4.15, 4.16 for the term formers associated
using
the above three lemmas for universal application and abstraction. We also make use of
obvious translations of syntactic constructs into categorical combinators, e.g. application
into evaluation and composition or storage into a combination of # , and functoriality of
Proof of Theorem 3.1 Applying the iteration principle (Theorem 4.6) to the denotations
of 0 and S shows that the function # : N # N x
Set is a morphism in B({x}) from N x to
Similarly, the function # : N p(x)
# N is a morphism in the other direction (by
polymorphic application). Thus the function in the theorem is a morphism.
The result follows by the analysis in Example 4.5. We proceed analogously in the case of
dyadic lists, using the corresponding iteration principle. #
5 Additional Remarks
We notice that for any realizability set A over X the unique function |A| #} is a morphism
A # I of realizability sets witnessed by e(#y.#x.x. In particular, this gives projections
for# . This shows that we can model an a#ne variant of BLL which has the following
additional rule Weak :
#, A # B
In particular, we see that this rule does not add computational strength.
Recall that we assumed the existence of a universe U in our ambient set theory which is
closed under U-indexed products. As is well-known, no such universe exists in classical ZF
set theory but it is consistent with constructive set theories [9, 13]. We found it convenient to
assume the existence of such a U because it allows the use of informal set-theoretic arguments
(provided they are constructive). For the reader who feels uneasy about such sleight-of-hand,
we o#er the following ways of making this rigorous (all of which, however, complicate the
. Formalize the entire discussion in the Calculus of Inductive Constructions [2].
. Formalize the entire discussion in a realizability topos [6, 13].
. Making the previous point explicit, we can stipulate that the carrier sets of realizability
sets must be a subquotient (by a per) of the set of untyped lambda terms (not
necessarily linear!). And furthermore, a morphism between realizability sets must be
uniformly tracked by an untyped lambda term, in the obvious sense. This would allow
one to interpret polymorphic quantification as intersection of pers.



--R

The Lambda Calculus
Springer LNCS 389
Bounded Linear Logic.
Light Linear Logic
Characterizing complexity classes by higher-type primitive recursive defini- tions
Linear types and non-size-increasing polynomial time computation
Type Systems for Polynomial-time Computation
Programming Languages capturing complexity classes
A small complete category
Stratified functional programs and computational complexity
Lambda calculus characterisations of polytime.
Categories for the Working Mathematician

Linear Logic
--TR
Bounded linear logic
Characterizing complexity classes by higher type primitive recursive definitions
Stratified functional programs and computational complexity
Lambda calculus characterizations of poly-time
Light linear logic
Polymorphism is Set Theoretic, Constructively
Inductively defined types
Phase semantics for light linear logic
Linear types and non-size-increasing polynomial time computation
complexity lambda calculus;finite model theory;linear logic