Dlal0705.bbl
\begin{thebibliography}{10}\setlength{\itemsep}{-1ex}\small

\bibitem{Asperti98}
A.~Asperti.
\newblock Light affine logic.
\newblock In {\em Proceedings LICS'98}. IEEE Computer Society, 1998.

\bibitem{AspertiRoversi02}
A.~Asperti and L.~Roversi.
\newblock Intuitionistic light affine logic.
\newblock {\em ACM Transactions on Computational Logic}, 3(1):1--39, 2002.

\bibitem{Baillot02}
P.~Baillot.
\newblock Checking polynomial time complexity with types.
\newblock In {\em Proceedings of IFIP TCS'02}, Montreal, 2002. Kluwer Academic
  Press.

\bibitem{Baillot03}
P.~Baillot.
\newblock Type inference for polynomial time complexity via constraints on
  words.
\newblock Preprint 02-03, LIPN, Universit\'e Paris XIII, january 2003.
\newblock submitted for publication.

\bibitem{Baillot00}
P.~Baillot.
\newblock Stratified coherence spaces: a denotational semantics for light
  linear logic.
\newblock {\em Theoretical Computer Science}, 2004.
\newblock to appear.

\bibitem{BarberPlotkin97}
A.~Barber and G.~Plotkin.
\newblock Dual intuitionistic linear logic.
\newblock Technical report, LFCS, University of Edinburgh, 1997.

\bibitem{BellantoniCook}
S.~Bellantoni and S.~Cook.
\newblock New recursion-theoretic characterization of the polytime functions.
\newblock {\em Computational Complexity}, 2:97--110, 1992.

\bibitem{BNS00}
S.~Bellantoni, K.-H. Niggl, and H.~Schwichtenberg.
\newblock Higher type recursion, ramification and polynomial time.
\newblock {\em Annals of Pure and Applied Logic}, 104(1-3), 2000.

\bibitem{Benton94}
N.~Benton.
\newblock A mixed linear and non-linear logic: Proofs, terms and models.
\newblock In {\em Proceedings of CSL'94}, number 933 in LNCS. Springer, 1994.

\bibitem{BBPH93}
N.~Benton, G.~Bierman, V.~de~Paiva, and M.~Hyland.
\newblock A term calculus for intuitionistic linear logic.
\newblock In {\em Proceedings TLCA'93}, volume 664 of {\em LNCS}. Springer
  Verlag, 1993.

\bibitem{CoppolaMartini01}
P.~Coppola and S.~Martini.
\newblock Typing lambda-terms in elementary logic with linear constraints.
\newblock In {\em Proceedings TLCA'01}, volume 2044 of {\em LNCS}, 2001.

\bibitem{CoppolaRonchi03}
P.~Coppola and S.~Ronchi~della Rocca.
\newblock Principal typing in {E}lementary {A}ffine {L}ogic.
\newblock In {\em Proceedings TLCA'03}, volume 2701 of {\em LNCS}, 2003.

\bibitem{DJS93}
V.~Danos, J.-B. Joinet, and H.~Schellinx.
\newblock On the linear decoration of intuitionistic derivations.
\newblock {\em Archive for Mathematical Logic}, 33(6), 1994.

\bibitem{Girard95a}
J.-Y. Girard.
\newblock Light linear logic.
\newblock {\em Information and Computation}, 143:175--204, 1998.

\bibitem{HillebrandKanellakis96}
G.~Hillebrand and P.~C. Kannelakis.
\newblock On the expressive power of simply typed and let-polymorphic lambda
  calculi.
\newblock In {\em Proceedings LICS'96}, pages 253--263. IEEE Computer Society,
  1996.

\bibitem{Hofmann99}
M.~Hofmann.
\newblock Linear types and non-size-increasing polynomial time computation.
\newblock In {\em Proceedings LICS'99}. IEEE Computer Society, 1999.

\bibitem{Hofmann00}
M.~Hofmann.
\newblock Safe recursion with higher types and {BCK}-algebra.
\newblock {\em Annals of Pure and Applied Logic}, 104(1-3), 2000.

\bibitem{HofmannJost}
M.~Hofmann and S.~Jost.
\newblock Static prediction of heap space usage for first-order functional
  programs.
\newblock In {\em Proc. ACM POPL'03}, 2003.

\bibitem{Lafont02}
Y.~Lafont.
\newblock Soft linear logic and polynomial time.
\newblock to appear in Theoretical Computer Science, 2004.

\bibitem{Leivant94}
D.~Leivant.
\newblock Predicative recurrence and computational complexity {I}: word
  recurrence and poly-time.
\newblock In {\em Feasible Mathematics II}, pages 320--343. Birkhauser, 1994.

\bibitem{Leivant02}
D.~Leivant.
\newblock Calibrating computational feasibility by abstraction rank.
\newblock In {\em Proceedings LICS'02}, pages 345--353. IEEE Computer Society,
  2002.

\bibitem{MairsonNeergard02}
H.~Mairson and P.~M. Neergard.
\newblock {LAL} is square: Representation and expressiveness in light affine
  logic, 2002.
\newblock Presented at the 4th International Workshop on Implicit Computational
  Complexity.

\bibitem{Maurel03}
F.~Maurel.
\newblock Nondederministic {L}ight {L}ogics and {NP}-time.
\newblock In {\em Proceedings of TLCA'03}, volume 2701 of {\em LNCS}. Springer,
  2003.

\bibitem{Schubert01}
A.~Schubert.
\newblock The complexity of beta-reduction in low orders.
\newblock In {\em Proceedings TLCA 2001}, LNCS, pages 400--414. Springer, 2001.

\bibitem{Terui01}
K.~Terui.
\newblock Light {A}ffine {L}ambda-calculus and polytime strong normalization.
\newblock In {\em Proceedings LICS'01}. IEEE Computer Society, 2001.
\newblock Full version available at http://research.nii.ac.jp/$\sim$ terui.

\bibitem{Terui04}
K.~Terui.
\newblock Light affine set theory: a naive set theory of polynomial time.
\newblock {\em Studia Logica}, 77:9--40, 2004.

\end{thebibliography}
