Fixpoint extensions of first-order logic and datalog-like languages, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp.71-79, 1989. ,
DOI : 10.1109/LICS.1989.39160
The Power of Linear Functions, Proceedings of the 20th International Workshop on Computer Science Logic (CSL '06), pp.119-134, 2006. ,
DOI : 10.1007/11874683_8
URL : https://hal.archives-ouvertes.fr/inria-00133321
Light affine logic, Proceedings. Thirteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.98CB36226), pp.300-308, 1998. ,
DOI : 10.1109/LICS.1998.705666
Intuitionistic Light Affine Logic, ACM Transactions on Computational Logic, vol.3, issue.1, pp.137-175, 2002. ,
DOI : 10.1145/504077.504081
Verification of Ptime Reducibility for System F Terms Via Dual Light Affine Logic, Proceedings of the 20th International Workshop on Computer Science Logic (CSL '06), pp.150-166, 2006. ,
DOI : 10.1007/11874683_10
URL : https://hal.archives-ouvertes.fr/hal-00021834
Checking Polynomial Time Complexity with Types, Proceedings of the 2nd IFIP International Conference on Theoretical Computer Science, pp.370-382, 2002. ,
DOI : 10.1007/978-0-387-35608-2_31
URL : https://hal.archives-ouvertes.fr/hal-00084626
Type inference for light affine logic via constraints on words, Theoretical Computer Science, vol.328, issue.3, pp.289-323, 2004. ,
DOI : 10.1016/j.tcs.2004.08.014
URL : https://hal.archives-ouvertes.fr/hal-00084611
Light logics and optimal reduction: Completeness and complexity, Proceedings of the Twenty- Second Annual IEEE Symposium on Logic in Computer Science (LICS '07), pp.421-430, 2007. ,
DOI : 10.1109/lics.2007.27
URL : https://hal.archives-ouvertes.fr/hal-00153136
Soft lambda-calculus: a language for polynomial time computation, Proceedings of the 7th International Conference on Foundations of Software Science and Computation Structures, pp.27-41, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00085129
Light types for polynomial time computation in lambda-calculus, Proceedings of the Nineteenth Annual IEEE Symposium on Logic in Computer Science (LICS '04), pp.266-275, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00003468
A Feasible Algorithm for Typing in Elementary Affine Logic, Proceedings of the 8th International Conference on Typed Lambda-Calculi and Applications (TLCA '05), pp.55-70, 2005. ,
DOI : 10.1007/11417170_6
URL : https://hal.archives-ouvertes.fr/hal-00084629
Lambda terms for natural deduction, sequent calculus and cut elimination, Journal of Functional Programming, vol.10, issue.1, pp.121-134, 2000. ,
DOI : 10.1017/S0956796899003524
The Lambda Calculus: Its Syntax and Semantics, 1984. ,
Predicative recursion and computational complexity, 1992. ,
A new recursion-theoretic characterization of the polytime functions, Computational Complexity, vol.106, issue.2, pp.97-110, 1992. ,
DOI : 10.1515/9781400858927
Higher type recursion, ramification and polynomial time, Annals of Pure and Applied Logic, vol.104, issue.1-3, pp.17-30, 2000. ,
DOI : 10.1016/S0168-0072(00)00006-3
URL : https://doi.org/10.1016/s0168-0072(00)00006-3
A term calculus for Intuitionistic Linear Logic, Proceedings of the 1st International Conference on Typed Lambda-Calculi and Applications (TLCA '93), pp.75-90, 1993. ,
DOI : 10.1007/BFb0037099
Stable models of typed ??-calculi, Fifth International Colloquium on Automata, Languages and Programming -ICALP'78, pp.72-89, 1978. ,
DOI : 10.1007/3-540-08860-1_7
Operational Properties of Lily, a Polymorphic Linear Lambda Calculus with Recursion, Electronic Notes in Theoretical Computer Science, vol.41, issue.3, p.41, 2000. ,
DOI : 10.1016/S1571-0661(04)80874-0
Computation models and function algebras, Proceedings of the International Workshop on Logic and Computational Complexity (LCC'94), pp.98-130, 1995. ,
DOI : 10.1007/3-540-60178-3_81
URL : http://www.cs.bc.edu/~clote/pub/handbook.ps
The intrinsic computational difficulty of functions, Proceedings of the International Congress for Logic, Methodology, and Philosophy of Science, pp.24-30, 1964. ,
Principal type schemes and lambda-calculus semantics, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp.535-560, 1980. ,
Elementary Affine Logic and the Call-by-Value Lambda Calculus, Proceedings of the 8th International Conference on Typed Lambda-Calculi and Applications (TLCA '05), volume 3461 of Lecture Notes in Computer Science, pp.131-145, 2005. ,
DOI : 10.1007/11417170_11
Typing Lambda Terms in Elementary Logic with Linear Constraints, Proceedings of the 6th International Conference on Typed Lambda-Calculi and Applications (TLCA '01), pp.76-90, 2001. ,
DOI : 10.1007/3-540-45413-6_10
Optimizing optimal reduction, ACM Transactions on Computational Logic, vol.7, issue.2, pp.219-260, 2006. ,
DOI : 10.1145/1131313.1131315
Principal Typing in Elementary Affine Logic, Proceedings of the 7th International Conference on Typed Lambda-Calculi and Applications (TLCA '03), pp.90-104, 2003. ,
DOI : 10.1007/3-540-44904-3_7
Definability and Full Abstraction, Electronic Notes in Theoretical Computer Science, vol.172, pp.301-310, 2007. ,
DOI : 10.1016/j.entcs.2007.02.011
URL : https://hal.archives-ouvertes.fr/hal-00144692
Modified basic functionality in combinatory logic, dialectica, vol.23, issue.2, 1969. ,
DOI : 10.1111/j.1746-8361.1969.tb01183.x
Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '82, pp.207-212, 1982. ,
DOI : 10.1145/582153.582176
Linear logic and elementary time, Information and Computation, vol.183, issue.1, pp.123-137, 2003. ,
DOI : 10.1016/S0890-5401(03)00010-5
URL : https://doi.org/10.1016/s0890-5401(03)00010-5
Abstract, The Journal of Symbolic Logic, vol.II, issue.03, pp.755-807, 1997. ,
DOI : 10.1007/BF00885763
URL : https://hal.archives-ouvertes.fr/inria-00528352
Sémantiques de la logique linéaire et temps de calcul, 2007. ,
A logical account of PSPACE, 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL Proceedings. to appear, 2008. ,
URL : https://hal.archives-ouvertes.fr/hal-00342323
Syntactical, operational and denotational linearity, Workshop on Linear Logic, Ludics, Implicit Complexity and Operator Algebras, 2007. ,
Soft linear logic and ?-calculus, 4th International Workshop on Proof, Computation, Complexity PCC'06, pp.Pro- ceedings, 2006. ,
A Soft Type Assignment System for ??-Calculus, Proceedings of the 21st International Workshop on Computer Science Logic (CSL '07), pp.253-267, 2007. ,
DOI : 10.1007/978-3-540-74915-8_21
A Type Inference Algorithm for a Stratified Polymorphic Type Discipline, Information and Computation, vol.109, issue.1-2, pp.115-173, 1994. ,
DOI : 10.1006/inco.1994.1015
Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-102, 1987. ,
DOI : 10.1016/0304-3975(87)90045-4
URL : https://hal.archives-ouvertes.fr/inria-00075966
Light Linear Logic, Information and Computation, vol.143, issue.2, pp.175-204, 1998. ,
DOI : 10.1006/inco.1998.2700
URL : https://doi.org/10.1006/inco.1998.2700
Bounded linear logic: a modular approach to polynomial-time computability, Theoretical Computer Science, vol.97, issue.1, pp.1-66, 1992. ,
DOI : 10.1016/0304-3975(92)90386-T
Characterizing complexity classes by higher type primitive recursive definitions, Theoretical Computer Science, vol.100, issue.1, pp.45-66, 1992. ,
DOI : 10.1016/0304-3975(92)90363-K
Semantics of Programming Languages: Structures and Techniques. foundations of Computing Series, 1992. ,
The Principal Type-Scheme of an Object in Combinatory Logic, Transactions of the American Mathematical Society, vol.146, pp.29-60, 1969. ,
DOI : 10.2307/1995158
Safe recursion with higher types and BCK-algebra, Annals of Pure and Applied Logic, vol.104, issue.1-3, pp.113-166, 2000. ,
DOI : 10.1016/S0168-0072(00)00010-5
URL : https://doi.org/10.1016/s0168-0072(00)00010-5
On Full Abstraction for PCF: I, II, and III, Information and Computation, vol.163, issue.2, pp.285-408, 1994. ,
DOI : 10.1006/inco.2000.2917
Descriptive Complexity, 1999. ,
DOI : 10.1007/978-1-4612-0539-5
The expressive power of higher-order types or, life without CONS, Journal of Functional Programming, vol.11, issue.1, pp.55-94, 2001. ,
DOI : 10.1017/S0956796800003889
Natural semantics, Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS), pp.22-39, 1987. ,
DOI : 10.1007/BFb0039592
URL : https://hal.archives-ouvertes.fr/inria-00075953
A direct algorithm for type inference in the rank-2 fragment of the second-order lambda-calculus, LISP and Functional Programming, pp.196-207, 1994. ,
A call-by-name lambda calculus machine. Higher Order and Symbolic Computation, 2007. ,
URL : https://hal.archives-ouvertes.fr/hal-00154508
Soft linear logic and polynomial time, Theoretical Computer Science, vol.318, issue.1-2, pp.163-180, 2004. ,
DOI : 10.1016/j.tcs.2003.10.018
A foundational delineation of computational feasibility, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp.2-11, 1991. ,
DOI : 10.1109/LICS.1991.151625
Lambda calculus characterizations of poly-time, Proceedings of the 1st International Conference on Typed Lambda-Calculi and Applications (TLCA '93), pp.274-288, 1993. ,
DOI : 10.1007/BFb0037112
Ramified recurrence and computational complexity II: Substitution and poly-space, Proceedings of the 8th International Workshop on Computer Science Logic (CSL '94), volume 933 of Lecture Notes in Computer Science, pp.486-500, 1994. ,
DOI : 10.1007/BFb0022277
Predicative functional recurrence and poly-space, Lecture Notes in Computer Science, vol.1214, pp.369-380, 1997. ,
DOI : 10.1007/BFb0030611
URL : https://link.springer.com/content/pdf/10.1007%2FBFb0030611.pdf
The sequentially realizable functionals. apal, pp.1-93, 2002. ,
On the Computational Complexity of Cut-Elimination in Linear Logic, ICTCS, volume 2841 of Lecture Notes in Computer Science, pp.23-36, 2003. ,
DOI : 10.1007/978-3-540-45208-9_4
A theory of type polymorphism in programming, Journal of Computer and System Sciences, vol.17, issue.3, pp.348-375, 1978. ,
DOI : 10.1016/0022-0000(78)90014-4
Type inference and type containment, Proc. of the international symposium on Semantics of data types, pp.257-277, 1984. ,
DOI : 10.1007/3-540-13346-1_13
Polymorphic type inference and containment. Information and Computation, pp.211-249, 1988. ,
DOI : 10.1016/0890-5401(88)90009-0
URL : https://doi.org/10.1016/0890-5401(88)90009-0
Classical Recursion Theory, 1999. ,
Implicit characterizations of pspace In Proof Theory in Computer Science, International Seminar, Proceedings, volume 2183 of Lecture Notes in Computer Science, pp.170-190, 2001. ,
Correspondence between operational and denotational semantics, Handbook of Logic in Computer Science, pp.269-356, 1995. ,
A stable programming language, Information and Computation, vol.204, issue.3, pp.339-375, 2006. ,
DOI : 10.1016/j.ic.2005.11.002
LCF considerd as a programming language, Theoretical Computer Science, vol.5, pp.225-255, 1977. ,
A structural approach to operational semantics, First appeared as DAIMI FN?19 technical report Aarhus University, pp.60-6117, 1981. ,
Simple, partial type-inference for system F based on type-containment, Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, pp.130-143, 2005. ,
Lambda calculus and intuitionistic linear logic, Studia Logica, issue.3, p.59, 1997. ,
Relationships between nondeterministic and deterministic tape complexities, Journal of Computer and System Sciences, vol.4, issue.2, pp.177-192, 1970. ,
DOI : 10.1016/S0022-0000(70)80006-X
URL : https://doi.org/10.1016/s0022-0000(70)80006-x
A type-theoretical alternative to ISWIM, CUCH, OWHY, Theoretical Computer Science, vol.121, issue.1-2, pp.411-440, 1993. ,
DOI : 10.1016/0304-3975(93)90095-B
Linear logical characterization of polyspace functions (extended abstract), Presented at the Workshop on Implicit Computational Complexity ICC'00, p.2000, 2000. ,
Light affine lambda calculus and polytime strong normalization, Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, pp.209-220, 2001. ,
DOI : 10.1109/LICS.2001.932498
Light logic and polynomial time computation, 2002. ,
Complexity and relational query languages, Fourteenth Symposium on Theory of Computing, pp.137-146, 1982. ,
Typability and type checking in the second-order ??-calculus are equivalent and undecidable, Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, pp.176-185, 1994. ,
DOI : 10.1109/LICS.1994.316068
Typability and type checking in System F are equivalent and undecidable, Annals of Pure and Applied Logic, vol.98, issue.1-3, pp.1-3111, 1999. ,
DOI : 10.1016/S0168-0072(98)00047-5