, A slice of a term is obtained by removing all components but one from each box. Let S(t) be the set of slices of term t defined as follows
, S(?) = {?} if ? ? {a
,
, = {? 1
, S(! f (x ? ?a.a, ?a.a ? x)) = {! f (x ? ?a.a), ! f (?a.a ? x)}. As illustrated by this example, in general, a slice does not belong to the set of
, A term t is parsimonious if: 1. all its slices are affine, i.e. each variable occurs at most once in a slice, 2. box subterms do not contain free affine variables, 3. all exponential variables belong to a box subterm
a ? a is not parsimonious because of point 1. However, ?a.(?a.a)a is parsimonious ,
? ?a.a, ?a.a ? x) is parsimonious. Indeed the affine variables a is not free and x occurs exactly once in each slice ,
, ? ! f (a, x, y, c) is not parsimonious because of point 2
, ? x?! f (y, z) is not parsimonious because of point 3. Characterizations of other interesting complexity classes based on the BSS model such as parallel polynomial time and classes of the polynomial hierarchy can be
11 1.2 Decidability and complexity of the type inference, Typing rules for LAL ,
40 3.1 Big step operational semantics of imperative programs ,
Small step operational semantics of multi-threads ,
Small step operational semantics with deterministic scheduling, p.68 ,
90 3.15 Type system for the higher-order functional program, 69 3.7 Tier-based processes type system ,
, Non-uniform parsimonious logic type system
Certified Complexity (CerCo), FOPARA, pp.1-18, 2013. ,
COSTA: design and implementation of a cost and termination analyzer for Java bytecode, ESOP, pp.113-132, 2007. ,
Cost analysis of object-oriented bytecode programs, Theoretical Computer Science, vol.413, issue.1, pp.142-159, 2012. ,
Certifying and reasoning on cost annotations in C programs, FMICS, pp.32-46, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00702665
, Computational Complexity: A Modern Approach, 2009.
Verification of Ptime reducibility for system F terms: type inference in dual light affine logic, Logical Methods in Computer Science, vol.3, issue.4, 2007. ,
Silvano Dal Zilio, and Line Jakubiec. A functional scenario for bytecode verification of resource bounds, CSL, pp.265-279, 2004. ,
, Parallel cost analysis. Transactions on Computational Logic, vol.19, issue.4, p.31, 2018.
Feasible reactivity for synchronous cooperative threads, Electronic Notes in Theoretical Computer Science, vol.154, issue.3, pp.33-43, 2006. ,
Beta reduction is invariant, indeed, CSL and LICS, pp.1-10, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-01091551
Automating sized-type inference for complexity analysis, ICFP, vol.1, pp.1-29, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01639200
On sharing, memoization, and polynomial time, Information and Computation, vol.261, pp.3-22, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01231816
Type-based complexity analysis of probabilistic functional programs, LICS, pp.1-13, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-02381829
Analysing the complexity of functional programs: higher-order meets first-order, ICFP, vol.50, pp.152-164, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01231809
On probabilistic term rewriting, FLOPS, pp.132-148, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-02381877
Resource control for synchronous cooperative threads, CONCUR, pp.68-82, 2004. ,
A new order-theoretic characterisation of the polytime computable functions, Theoretical Computer Science, vol.585, pp.3-24, 2015. ,
Noncumulative resource analysis, TACAS, pp.85-100, 2015. ,
Termination of term rewriting using dependency pairs, Theoretical Computer Science, vol.236, issue.1-2, pp.133-178, 2000. ,
Heap space analysis for Java bytecode, ISMM, pp.105-116, 2007. ,
Heap space analysis for garbage collected languages, Science of Computer Programming, vol.78, issue.9, pp.1427-1448, 2013. ,
Static complexity analysis of higher order programs, FOPARA, pp.84-99, 2009. ,
Arithmetizing uniform NC, Annals of Pure and Applied Logic, vol.53, issue.1, pp.1-50, 1991. ,
Complexity analysis by rewriting, FLOPS, pp.130-146, 2008. ,
Dependency pairs and polynomial path orders, RTA, pp.48-62, 2009. ,
Closing the gap between runtime complexity and polytime computability, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.6, pp.33-48, 2010. ,
Complexity analysis by graph rewriting, FLOPS, pp.257-271, 2010. ,
Productive coprogramming with guarded recursion, ICFP, vol.48, pp.197-208, 2013. ,
Tyrolean complexity tool: Features and usage, RTA, volume 21 of LIPIcs. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 2013. ,
A combination framework for complexity. Information and Computation, vol.248, pp.22-55, 2016. ,
Max-plus quasi-interpretations, TLCA, pp.31-45 ,
URL : https://hal.archives-ouvertes.fr/hal-00146999
, , 2003.
Synthesis of max-plus quasi-interpretations, Fundamenta Informaticae, vol.65, issue.1-2, pp.29-60, 2005. ,
URL : https://hal.archives-ouvertes.fr/hal-00146968
TcT: Tyrolean complexity Tool, TACAS, pp.407-423, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01392188
Modular runtime complexity analysis of probabilistic while programs. DICE-FOPARA workshops, 2019. ,
Intuitionistic light affine logic, Transactions on Computational Logic, vol.3, issue.1, pp.137-175, 2002. ,
Light affine logic, LICS, pp.300-308, 1998. ,
POP* and semantic labeling using SAT, ESSLLI, pp.155-166, 2008. ,
The Lambda Calculus, vol.3, 1984. ,
General size-change termination and lexicographic descent, The essence of computation, pp.3-17, 2002. ,
On the linear ranking problem for integer linear-constraint loops, POPL, vol.48, pp.51-62, 2013. ,
On multiphase-linear ranking functions, CAV, pp.601-620, 2017. ,
On the termination of integer loops, Transactions on Programming Languages and Systems, vol.34, issue.4, p.16, 2012. ,
Checking polynomial time complexity with types, Foundations of Information Technology in the Era of Network and Mobile Computing, pp.370-382, 2002. ,
URL : https://hal.archives-ouvertes.fr/hal-00084626
Stratified coherence spaces: a denotational semantics for light linear logic, Theoretical Computer Science, vol.318, issue.1-2, pp.29-55, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00084609
Type inference for light affine logic via constraints on words, Theoretical Computer Science, vol.328, issue.3, pp.289-323, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00084611
Logique linéaire, types et complexité implicite. Mémoire d'habilitation à diriger des recherches, 2008. ,
Characterizing polynomial and exponential complexity classes in elementary lambda-calculus. Information and Computation, vol.261, pp.55-77, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01015171
A new recursion-theoretic characterization of the polytime functions, Computational Complexity, vol.2, issue.2, pp.97-110, 1992. ,
Implicit complexity over an arbitrary structure: Sequential and parallel polynomial time, Journal of Logic and Computation, vol.15, issue.1, pp.41-58, 2005. ,
URL : https://hal.archives-ouvertes.fr/inria-00102942
, Implicit complexity over an arbitrary structure: Quantifier alternations. Information and Computation, vol.204, pp.210-230, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00107811
Complexity classes and rewrite systems with polynomial interpretation, CSL, pp.372-384, 1998. ,
URL : https://hal.archives-ouvertes.fr/inria-00098689
Algorithms with polynomial interpretation termination proof, Journal of Functional Programming, vol.11, issue.1, pp.33-53, 2001. ,
URL : https://hal.archives-ouvertes.fr/inria-00100819
Pola: A language for ptime programming, FICS, pp.7-8, 2009. ,
Complexity invariance of real interpretations, TAMC, pp.139-150, 2010. ,
URL : https://hal.archives-ouvertes.fr/inria-00535784
Real or natural number interpretation and their effect on complexity, Theoretical Computer Science, vol.585, pp.25-40, 2015. ,
Higher-order interpretations and program complexity, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.16, pp.62-76, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00798298
Higher-order interpretations and program complexity, Information and Computation, vol.248, pp.56-81, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-00798298
On intersection types and probabilistic lambda calculi, PPDP, vol.8, pp.1-13, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01926420
A lambda-calculus foundation for universal probabilistic programming, ICFP, vol.51, pp.33-46, 2016. ,
On quasi-interpretations, blind abstractions and implicit complexity, Mathematical Structures in Computer Science, vol.22, issue.4, pp.549-580, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00798377
Predicative recursion and the polytime hierarchy, Feasible Mathematics II, pp.15-29, 1995. ,
Proving positive almost-sure termination, RTA, pp.323-337, 2005. ,
URL : https://hal.archives-ouvertes.fr/inria-00099867
Proving positive almost sure termination under strategies, RTA, pp.357-371, 2006. ,
Programs as polygraphs: computability and complexity, 2007. ,
Intensional properties of polygraphs, Electronic Notes in Theoretical Computer Science, vol.203, issue.1, pp.65-77, 2008. ,
URL : https://hal.archives-ouvertes.fr/inria-00129391
Combining linear logic and size types for implicit complexity, CSL, volume 119 of LIPIcs, pp.1-21, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01948196
Algebraic characterizations of complexity-theoretic classes of real functions, International Journal of Unconventional Computing, vol.7, issue.5, pp.331-351, 2011. ,
URL : https://hal.archives-ouvertes.fr/inria-00421561
Polynomial time corresponds to solutions of polynomial ordinary differential equations of polynomial length: The general purpose analog computer and computable analysis are two efficiently equivalent models of computations, ICALP, vol.55, pp.1-15, 2016. ,
Type-based termination with sized products, CSL, pp.493-507, 2008. ,
Real recursive functions and real extensions of recursive functions, MCU, pp.116-127, 2004. ,
URL : https://hal.archives-ouvertes.fr/inria-00100053
Automatic certification of heap consumption, LPAR, pp.347-362, 2004. ,
Integrity considerations for secure computer systems, 1977. ,
Recursion schemata for NC k, CSL, pp.49-63, 2008. ,
Non-idempotent intersection types for the lambda-calculus, Logic Journal of the IGPL, vol.25, issue.4, pp.431-464, 2017. ,
Complexity of strongly normalising ?terms via non-idempotent intersection types, FoSSaCS, pp.88-107, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-01110489
Function-algebraic characterizations of log and polylog parallel time, Computational Complexity, vol.4, issue.2, pp.175-205, 1994. ,
Sat modulo linear arithmetic for solving polynomial constraints, Journal of Automated Reasoning, vol.48, issue.1, pp.107-131, 2012. ,
Secure computer system: unified exposition and multics interpretation, Mitre corp Rep, 1976. ,
A machine-independent theory of the complexity of recursive functions, Journal of the ACM, vol.14, issue.2, pp.322-336, 1967. ,
Soft lambda-calculus: a language for polynomial time computation, FoSSaCS, pp.27-41, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00085129
Linear logic by levels and bounded time complexity, Theoretical Computer Science, vol.411, issue.2, pp.470-503, 2010. ,
URL : https://hal.archives-ouvertes.fr/hal-00488531
Indexed realizability for bounded-time programming with references and type fixpoints, APLAS, pp.264-279, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00735584
On lexicographic termination ordering with space bound certifications, PSI, pp.482-493 ,
URL : https://hal.archives-ouvertes.fr/inria-00100523
, , 2001.
Quasiinterpretations and small space bounds, RTA, pp.150-164, 2005. ,
URL : https://hal.archives-ouvertes.fr/inria-00001234
Quasiinterpretations a way to control resources, Theoretical Computer Science, vol.412, issue.25, pp.2776-2796, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00591862
Synthesis of quasi-interpretations, 2005. ,
URL : https://hal.archives-ouvertes.fr/inria-00000660
A characterization of alternating log time by first order functional programs, LPAR, pp.90-104 ,
URL : https://hal.archives-ouvertes.fr/inria-00110014
, , 2006.
Quasiinterpretation synthesis by decomposition, ICTAC, pp.410-424, 2007. ,
URL : https://hal.archives-ouvertes.fr/inria-00130920
Term Rewriting and All That, 1999. ,
Higher type recursion, ramification and polynomial time, Annals of Pure and Applied Logic, vol.104, issue.1-3, pp.17-30, 2000. ,
Machine models and simulations, Handbook of Theoretical Computer Science, vol.1, pp.1-66, 2014. ,
Some programming languages for Logspace and Ptime, AMAST, pp.66-80, 2006. ,
URL : https://hal.archives-ouvertes.fr/inria-00105744
Complexité implicite des calculs : interprétation de programmes. Mémoire d'habilitation à diriger des recherches, 2011. ,
Dual intuitionistic linear logic, 1996. ,
An embedding of the BSS model of computation in light affine lambda-calculus, 2006. ,
URL : https://hal.archives-ouvertes.fr/hal-00085547
Call-by-value, elementary time and intersection types, FOPARA, pp.40-59, 2015. ,
On a theory of computation over the real numbers; NP completeness, recursive functions and universal machines, FOCS, pp.387-397, 1988. ,
Light types for polynomial time computation in lambda-calculus, LICS, pp.266-275, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00003468
A feasible algorithm for typing in elementary affine logic, TLCA, pp.55-70, 2005. ,
URL : https://hal.archives-ouvertes.fr/hal-00084629
Light types for polynomial time computation in lambda calculus, Information and Computation, vol.207, issue.1, pp.41-62, 2009. ,
URL : https://hal.archives-ouvertes.fr/hal-00003468
Church => Scott = Ptime: an application of resource sensitive realizability, Electronic Proceedings in Theoretical Computer Science, vol.23, pp.31-46, 2010. ,
Quantum complexity theory, SIAM Journal on Computing, vol.26, issue.5, pp.1411-1473, 1997. ,
Hans Bugge Grathwohl, and Lars Birkedal. Programming and reasoning with guarded recursion for coinductive types, FoS-SaCS, pp.407-421, 2015. ,
Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, POPL, pp.238-252, 1977. ,
A higher-order removal method, Lisp and Symbolic Computation, vol.9, pp.287-322, 1996. ,
Compositional certified resource bounds, vol.50, pp.467-478, 2015. ,
Characterizations of the basic feasible functionals of finite type, Feasible mathematics, pp.71-96, 1990. ,
Arithmetic, Proof Theory, and Computational Complexity. Number 23, 1993. ,
Calculating sized types. Higher-Order and Symbolic Computation, vol.14, pp.261-300, 2001. ,
Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming, vol.9, pp.137-159, 1987. ,
Polynomial interpretations and the complexity of algorithms, CADE, pp.139-147, 1992. ,
Sequential, machine-independent characterizations of the parallel complexity classes Alogtime, AC k , NC k and NC, Feasible mathematics, pp.49-69, 1990. ,
Nondeterministic stack register machines, Theoretical Computer Science, vol.178, issue.1-2, pp.37-76, 1997. ,
Computation models and function algebras, Studies in Logic and the Foundations of Mathematics, vol.140, pp.589-681, 1999. ,
The light lexicographic path ordering, 2000. ,
URL : https://hal.archives-ouvertes.fr/inria-00099238
Typing lambda terms in elementary logic with linear constraints, TLCA, pp.76-90, 2001. ,
Mechanically proving termination using polynomial interpretations, Journal of Automated Reasoning, vol.34, issue.4, p.325, 2005. ,
URL : https://hal.archives-ouvertes.fr/inria-00001167
Using approximation to relate computational classes over the reals, MCU, pp.39-61, 2007. ,
The intrinsic computational difficulty of functions, 1965. ,
About primitive recursive algorithms, ICALP, pp.194-206 ,
, , 1989.
Type two computational complexity, STOC, pp.108-121, 1973. ,
Computability and complexity of higher type functions, Logic from Computer Science, pp.51-72, 1992. ,
Infinite objects in type theory, TYPES, vol.806, pp.62-78, 1994. ,
TERMINATOR: beyond safety, CAV, pp.415-418, 2006. ,
Space lower bounds for maze threadability on restricted machines, SIAM Journal on Computing, vol.9, issue.3, pp.636-652, 1980. ,
Alternation, FOCS, pp.98-108, 1976. ,
ML with Ptime complexity guarantees, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.16, pp.198-212, 2012. ,
The role of polymorphism in the characterisation of complexity by soft types. Information and Computation, vol.248, pp.130-149, 2016. ,
First order bounded arithmetic and small boolean circuit complexity classes, Feasible mathematics, pp.154-218, 1995. ,
Functional interpretations of feasibly constructive arithmetic, Annals of Pure and Applied Logic, vol.63, issue.2, pp.103-200, 1993. ,
An analytical approach to program as data objects, 2006. ,
Intersection types for light affine lambda calculus, Electronic Notes in Theoretical Computer Science, vol.136, pp.133-152, 2005. ,
Execution time of ?-terms via denotational semantics and intersection types, Mathematical Structures in Computer Science, vol.28, issue.7, pp.1169-1203, 2018. ,
A note on simplification orderings, Information Processing Letters, vol.9, issue.5, pp.212-215, 1979. ,
Orderings for term-rewriting systems, Theoretical Computer Science, vol.17, issue.3, pp.279-301, 1982. ,
Termination of rewriting, Journal of Symbolic Computation, vol.3, issue.1/2, pp.69-116, 1987. ,
Quantum theory, the Church-Turing principle and the universal quantum computer, Mathematical and Physical Sciences, vol.400, pp.97-117, 1818. ,
On the productivity of recursive definitions, vol.749, 1980. ,
Linear logic and elementary time, formation and Computation, vol.183, pp.123-137, 2003. ,
Linear dependent types and relative completeness, LICS, pp.133-142, 2011. ,
Probabilistic termination by monadic affine sized typing, Transactions on Programming Languages and Systems, vol.41, issue.2, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-01635077
Quantitative models and implicit complexity, FSTTCS, pp.189-200, 2005. ,
Realizability models and implicit complexity, Theoretical Computer Science, vol.412, issue.20, pp.2029-2047, 2011. ,
On constructor rewrite systems and the lambda-calculus, ICALP, pp.163-174, 2009. ,
Light logics and higherorder processes, Electronic Proceedings in Theoretical Computer Science, vol.41, pp.46-60, 2010. ,
URL : https://hal.archives-ouvertes.fr/hal-01400903
Light logics and higherorder processes, Mathematical Structures in Computer Science, vol.26, issue.6, pp.969-992, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01400903
Quantum implicit computational complexity, Theoretical Computer Science, vol.411, issue.2, pp.377-409, 2010. ,
Linear dependent types in a call-by-value scenario, Science of Computer Programming, vol.84, pp.77-100, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-00909317
Denotational cost semantics for functional languages with inductive types, ICFP, vol.50, pp.140-151, 2015. ,
Functional programming in sublinear space, ESOP, pp.205-225, 2010. ,
Computation by interaction for space-bounded functional programming. Information and Computation, vol.248, pp.150-194, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01337724
Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Ariya Isihara, and Jan Willem Klop. Productivity of stream definitions, Theoretical Computer Science, vol.241, issue.4-5, pp.765-782, 2010. ,
The differential lambda-calculus, Theoretical Computer Science, vol.309, issue.1-3, pp.1-41, 2003. ,
URL : https://hal.archives-ouvertes.fr/hal-00150572
Uniformity and the taylor expansion of ordinary lambda-terms, Theoretical Computer Science, vol.403, issue.2-3, pp.347-372, 2008. ,
URL : https://hal.archives-ouvertes.fr/hal-00150275
Matrix interpretations for proving termination of term rewriting, Journal of Automated Reasoning, vol.40, issue.2-3, pp.195-220, 2008. ,
Generalized first-order spectra and polynomial-time recognizable sets, Complexity of computation, vol.7, pp.43-73, 1974. ,
Probabilistic rewriting: Normalization, termination, and unique normal forms, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.1-25, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-02411553
SAT solving for termination analysis with polynomial interpretations, SAT, pp.340-354, 2007. ,
Interpretation of stream programs: Characterizing type 2 polynomial time complexity, ISAAC, pp.291-303, 2010. ,
Characterizing polynomial time complexity of stream programs using interpretations, Theoretical Computer Science, vol.585, pp.41-54, 2015. ,
Formal proof of polynomial-time complexity with quasi-interpretations, CPP, pp.146-157, 2018. ,
Analyzing program termination and complexity automatically with AProVE, LICS, vol.58, pp.3-31, 2017. ,
, Terminationsbeweise bei Termersetzungssystemen. diplomarbeit, 1988.
Generating polynomial orderings for termination proofs, RTA, pp.426-431, 1995. ,
Interprétation fonctionelle et élimination des coupures de l'arithmétique d'ordre supérieur, 1972. ,
Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-101, 1987. ,
URL : https://hal.archives-ouvertes.fr/inria-00075966
Light linear logic. Information and Computation, vol.143, pp.175-204, 1998. ,
The complexity of interaction, POPL, vol.51, pp.243-255, 2016. ,
SPEED: precise and efficient static estimation of program computational complexity, POPL, vol.44, pp.127-139, 2009. ,
A logical account of PSPACE, vol.43, pp.121-131, 2008. ,
URL : https://hal.archives-ouvertes.fr/hal-00342323
Soft linear logic and polynomial complexity classes, Electronic Notes in Theoretical Computer Science, vol.205, pp.67-87, 2008. ,
URL : https://hal.archives-ouvertes.fr/hal-00342320
Induction for positive almost sure termination, PPDP, pp.167-178, 2007. ,
URL : https://hal.archives-ouvertes.fr/inria-00182435
Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für mathematik und physik, vol.38, pp.173-198, 1931. ,
Characterizing complexity classes by general recursive definitions in higher types, Information and Computation, vol.101, issue.2, pp.202-218, 1992. ,
Global and local space properties of stream programs, FOPARA, pp.51-66, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00539835
Upper bounds on stream I/O using semantic interpretations, CSL, pp.271-286, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00431469
Algebras and coalgebras in the light affine lambda calculus, ICFP, vol.50, pp.114-126, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01112165
On bounding space usage of streams using interpretation analysis, Science of Computer Programming, vol.111, pp.395-425, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01112161
The expressive power of second order Horn logic, STACSs, pp.466-477, 1991. ,
Generalized sufficient conditions for modular termination of rewriting, Communication and Computing, vol.5, issue.3-4, pp.131-158, 1994. ,
A soft type assignment system for ?-calculus, CSL, pp.253-267, 2007. ,
Type inference for a polynomial lambda calculus, TYPES, pp.136-152, 2008. ,
A fast quantum mechanical algorithm for database search, STOC, pp.212-219, 1996. ,
Some classes of recursive functions, stytut Matematyczny Polskiej Akademi Nauk (Warszawa), 1953. ,
Bounded linear logic: a modular approach to polynomial-time computability, Theoretical Computer Science, vol.97, issue.1, pp.1-66, 1992. ,
SPEED: Symbolic complexity bound analysis, CAV, pp.51-62, 2009. ,
Algebras of feasible functions, FOCS, pp.210-214, 1983. ,
A typed lambda calculus with categorical type constructors, CTCS, vol.283, pp.140-57, 1987. ,
Multivariate amortized resource analysis, POPL, vol.46, pp.357-370, 2011. ,
Resource aware ML, CAV, pp.781-786, 2012. ,
Arithmetical hierarchy and complexity of computation, Theoretical Computer Science, vol.8, issue.2, pp.227-237, 1979. ,
Amortized resource analysis with polynomial potential, ESOP, pp.287-306, 2010. ,
Static prediction of heap space usage for firstorder functional programs, POPL, vol.38, pp.185-197, 2003. ,
Type-based amortised heap-space analysis, ESOP, pp.22-37, 2006. ,
Size-change termination and transition invariants, SAS, pp.22-50, 2010. ,
Automated complexity analysis based on the dependency pair method, IJCAR, pp.364-379, 2008. ,
Automated complexity analysis based on context-sensitive rewriting, TLCA and RTA, pp.257-271, 2014. ,
Amortised resource analysis and typed polynomial interpretations, TLCA and RTA, pp.272-286, 2014. ,
Multivariate amortised resource analysis for term rewrite systems, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.38, pp.241-256, 2015. ,
Type-based complexity analysis for fork processes, FoSSaCS, pp.305-320, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00755450
Termination proofs by multiset path orderings imply primitive recursive derivation lengths, Theoretical Computer Science, vol.105, issue.1, pp.129-140, 1992. ,
Linear types and non-size-increasing polynomial time computation, LICS, pp.464-473, 1999. ,
Safe recursion with higher types and BCK-algebra, Annals of Pure and Applied Logic, vol.104, issue.1-3, pp.113-166, 2000. ,
Termination proofs by context-dependent interpretations, RTA, pp.108-121, 2001. ,
The strength of non-size increasing computation, POPL, vol.37, issue.1, pp.260-269, 2002. ,
Linear types and non-size-increasing polynomial time computation. Information and Computation, vol.183, pp.57-85, 2003. ,
Objects in polynomial time, APLAS, pp.387-404, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01206161
Higher order interpretation for higher order complexity, LPAR, EPIC, pp.269-285, 2017. ,
A type-based complexity analysis of object oriented programs. Information and Computation, vol.261, pp.78-115, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01712506
Proving the correctness of reactive systems using sized types, POPL, pp.410-423, 1996. ,
Efficient type-checking for amortised heap-space analysis, CSL, pp.317-331, 2009. ,
Automatic type inference for amortised heap-space analysis, ESOP, pp.593-613, 2013. ,
Pure pointer programs and tree isomorphism, FoSSaCS, pp.321-336, 2013. ,
Pure pointer programs with iteration, Transactions on Computational Logic, vol.11, issue.4, p.26, 2010. ,
Automatic static cost analysis for parallel programs, ESOP, pp.132-157, 2015. ,
Termination of string rewriting with matrix interpretations, RTA, pp.328-342, 2006. ,
On characterizations of the basic feasible functionals, Part II, 2002. ,
Relational queries computable in polynomial time, Information and Control, vol.68, issue.1-3, pp.86-104, 1986. ,
Descriptive Complexity, 2012. ,
Featherweight Java: a minimal core calculus for Java and GJ, Transactions on Programming Languages and Systems, vol.23, issue.3, pp.396-450, 2001. ,
On characterizations of the basic feasible functionals, Part I, Journal of Functional Programming, vol.11, issue.1, pp.117-153, 2001. ,
Pointers in recursion: Exploring the tropics, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.1-18, 2019. ,
Static determination of quantitative resource usage for higher-order programs, POPL, vol.45, pp.223-236, 2010. ,
The flow of data and the complexity of algorithms, CIE, pp.263-274, 2005. ,
A flow calculus of mwp-bounds for complexity analysis, Transactions on Computational Logic, vol.10, issue.4, p.28, 2009. ,
Logspace and Ptime characterized by programming languages. Theoretical Computer Science, vol.228, pp.151-174, 1999. ,
The expressive power of higher-order types or, life without CONS, Journal of Functional Programming, vol.11, issue.1, pp.55-94, 2001. ,
A tutorial on (co)algebras and (co)induction, EATCS Bulletin, vol.62, pp.222-259, 1997. ,
Term Rewriting Systems, 2001. ,
Egyszerü példa eldönthetetlen aritmetikai problémára. Mate és fizikai lapok, vol.50, pp.1-23, 1943. ,
Attempts for generalizing the recursive path orderings, 1980. ,
A new characterization of Mehlhorn's polynomial time functionals, FOCS, pp.342-347, 1991. ,
A new characterization of type-2 feasibility, SIAM Journal on Computing, vol.25, issue.1, pp.117-132, 1996. ,
On the termination problem for probabilistic higher-order recursive programs, LICS, pp.1-14, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-02399361
Weakest precondition reasoning for expected runtimes of probabilistic programs, ESOP, pp.364-389, 2016. ,
A theory of positive integers in formal logic. Part I, American Journal of Mathematics, vol.57, issue.1, pp.153-173, 1935. ,
General recursive functions of natural numbers, Mathematische annalen, vol.112, issue.1, pp.727-742, 1936. ,
On recursive path ordering, Theoretical Computer Science, vol.40, pp.323-328, 1985. ,
On the computational complexity of imperative programming languages, Theoretical Computer Science, vol.318, issue.1-2, pp.139-161, 2004. ,
, Complexity Theory of Real Functions. Birkhäuser, 1991.
Modularity of simple termination of term rewriting systems with shared constructors, Theoretical Computer Science, vol.103, issue.2, pp.273-282, 1992. ,
Semantics of probabilistic programs, SFCS, pp.101-114, 1979. ,
The Unix Programming Environment, 1984. ,
Type-two polynomial-time and restricted lookahead, LICS, pp.579-588, 2018. ,
Making resource analysis practical for real-time Java, Electronic Proceedings in Theoretical Computer Science, vol.298, pp.135-144, 2012. ,
Complexity classes and fragments of C. Information Processing Letters, vol.88, pp.213-218, 2003. ,
Types as resources for classical natural deduction, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.84, pp.1-17, 2017. ,
Soft linear logic and polynomial time, Theoretical Computer Science, vol.318, issue.1-2, pp.163-180, 2004. ,
On proving term rewriting systems are Noetherien, 1979. ,
A note on polynomial interpretation, Bulletin of the EATCS, vol.36, pp.129-130, 1988. ,
Ramified recurrence and computational complexity I: Word recurrence and poly-time, Feasible mathematics, pp.320-343, 1995. ,
A characterization of NC by tree recurrence, FOCS, pp.716-724, 1998. ,
The size-change principle for program termination, POPL, vol.36, pp.81-92, 2001. ,
Lambda calculus characterizations of polytime, TLCA, pp.274-288, 1993. ,
Ramified recurrence and computational complexity II: substitution and poly-space, CSL, pp.486-500, 1994. ,
A characterization of alternating log time by ramified recurrence, Theoretical Computer Science, vol.236, issue.1-2, pp.193-208, 2000. ,
URL : https://hal.archives-ouvertes.fr/inria-00099078
Evolving graph-structures and their implicit computational complexity, ICALP, pp.349-360, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00939484
Obsessional cliques: a semantic characterization of bounded time complexity, LICS, pp.179-188, 2006. ,
URL : https://hal.archives-ouvertes.fr/hal-00096274
Polynomials over the reals in proofs of termination: from theory to practice, RAIRO-Theoretical Informatics and Applications, vol.39, issue.3, pp.547-586, 2005. ,
Practical use of polynomials over the reals in proofs of termination, PPDP, pp.39-50, 2007. ,
An elementary affine ?-calculus with multithreading and side effects, TLCA, pp.138-152, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00610012
A polynomial time ?-calculus with multithreading and side effects, PPDP, pp.55-66, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00735544
A type system for complexity flow analysis, LICS, pp.123-132, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00591853
Nondeterministic light logics and NP-time, TLCA, pp.241-255, 2003. ,
An infinitary affine lambda-calculus isomorphic to the full lambda-calculus, LICS, pp.471-480, 2012. ,
Non-uniform polytime computation in the infinitary affine lambda-calculus, ICALP, pp.305-317, 2014. ,
Simple parsimonious types and logarithmic space, CSL, volume 41 of LIPIcs, pp.24-40, 2015. ,
Polynomial and abstract subrecursive classes, Journal of Computer and System Sciences, vol.12, issue.2, pp.147-178, 1976. ,
Efficient first order functional program interpreter with time bound certifications, LPAR, pp.25-42, 2000. ,
URL : https://hal.archives-ouvertes.fr/inria-00099178
On the termination of markov algorithms, HICSS, pp.789-792, 1970. ,
On an interpretation of safe recursion in light affine logic, Theoretical Computer Science, vol.318, issue.1-2, pp.197-223, 2004. ,
, Resource control graphs. Transactions on Computational Logic, vol.10, issue.4, p.29, 2009.
Resource analysis by sup-interpretation, FLOPS, pp.163-176, 2006. ,
URL : https://hal.archives-ouvertes.fr/inria-00000661
Analyzing the implicit computational complexity of object-oriented programs, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.2, pp.316-327, 2008. ,
URL : https://hal.archives-ouvertes.fr/inria-00332550
A characterization of NC k by first order functional programs, TAMC, pp.136-147, 2008. ,
Characterizations of polynomial complexity classes with a better intensionality, PPDP, pp.79-88, 2008. ,
URL : https://hal.archives-ouvertes.fr/inria-00332389
Sup-interpretations, a semantic method for static analysis of program resources, Transactions on Computational Logic, vol.10, issue.4, p.27, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00446057
Complexity information flow in a multithreaded imperative language, TAMC, pp.124-140, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-00684026
Proving quadratic derivational complexities using context dependent interpretations, RTA, pp.276-290, 2008. ,
The derivational complexity induced by the dependency pair method, RTA, pp.255-269, 2009. ,
Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.10, pp.235-250, 2011. ,
Complexity analysis of term rewriting based on matrix and context dependent interpretations, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.2, pp.304-315, 2008. ,
Parsimonious types and non-uniform computation, ICALP, pp.350-361, 2015. ,
Klassifizierungen der primitiv-rekursiven Funktionen, 1974. ,
Bounded expectations: resource analysis for probabilistic programs, PLDI, vol.53, pp.496-512 ,
Analyzing innermost runtime complexity of term rewriting by dependency pairs, Journal of Automated Reasoning, vol.51, issue.1, pp.27-56, 2013. ,
The µ-measure as a tool for classifying computational complexity, Archive for Mathematical Logic, vol.39, issue.7, pp.515-539, 2000. ,
Polynomial interpretations over the reals do not subsume polynomial interpretations over the integers, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.6, pp.243-258, 2010. ,
Certifying polynomial time and linear/polynomial space for imperative programs, SIAM Journal on Computing, vol.35, issue.5, pp.1122-1147, 2006. ,
Revisiting matrix interpretations for polynomial derivational complexity of term rewriting, LPAR, pp.550-564, 2010. ,
Implicit characterizations of PSPACE, PTCS, pp.170-190 ,
, , 2001.
, Christos Papadimitriou. Computational Complexity, 2003.
Synthesis of sup-interpretations: a survey, Theoretical Computer Science, vol.467, pp.30-52, 2013. ,
Quantum entanglement analysis based on abstract interpretation, SAS, pp.270-282, 2008. ,
Paths-based criteria and application to linear logic subsystems characterizing polynomial time, Information and Computation, vol.261, pp.23-54, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-02154716
Recursive Functions, 1967. ,
Basic Category Theory for Computer Scientists, 1991. ,
Types and Programming Languages, 2002. ,
A quantifier-free theory based on a string algebra for NC 1, Proof complexity and feasible arithmetics, pp.229-252, 1998. ,
A recursively defined ordering for proving termination of term rewriting systems, 1978. ,
Transition invariants, LICS, pp.32-41, 2004. ,
Multiplexor categories and models of soft linear logic, LFCS, pp.472-485, 2007. ,
Undirected connectivity in log-space, Journal of the ACM, vol.55, issue.4, p.17, 2008. ,
Definitional interpreters for higher-order programming languages, Proceedings of the ACM annual conference, vol.2, pp.717-740 ,
Towards a theory of type structure, Programming Symposium, pp.408-425, 1974. ,
Classes of predictably computable functions, Transactions of the American Mathematical Society, vol.106, issue.1, pp.139-173, 1963. ,
Subrecursion: Functions and Hierarchies, 1987. ,
A p-time completeness proof for light logics, CSL, pp.469-483 ,
, , 1999.
On uniform circuit complexity, Journal of Computer and System Sciences, vol.22, issue.3, pp.365-383, 1981. ,
Complexity analysis for a lazy higher-order language, ESOP, pp.361-376, 1990. ,
Time analysis, cost equivalence and program refinement, FSTTCS, pp.25-39, 1991. ,
Models of Computation, vol.136, 1998. ,
Polynomial computability and recursivity in finite domains, Elektronische Informationsverarbeitung und Kybernetik, vol.16, issue.7, pp.319-323, 1980. ,
Rekursionszahlen und die Grzegorczyk-Hierarchie, Archiv für mathematische Logik und Grundlagenforschung, vol.12, issue.1-2, pp.85-97, 1969. ,
Stratified bounded affine logic for logarithmic space, LICS, vol.7, pp.411-420, 2007. ,
Towards a quantum programming language, Mathematical Structures in Computer Science, vol.14, issue.4, pp.527-586, 2004. ,
A light modality for recursion, FoSSaCS, pp.499-516, 2017. ,
Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer, SIAM Journal on Computing, vol.26, issue.5, pp.1484-1509, 1997. ,
On the productivity of recursive list definitions, Transactions on Programming Languages and Systems, vol.11, issue.4, pp.633-649, 1989. ,
Introduction to the Theory of Computation, Thomson Course Technology, 2006. ,
Test-based inference of polynomial loop-bound functions, PPDP, pp.99-108, 2010. ,
Dimensions and principles of declassification, CSFW, pp.255-269, 2005. ,
Proving polynomials positive, FSTTCS, pp.191-202 ,
, , 1992.
Secure information flow in a multi-threaded imperative language, POPL, pp.355-364, 1998. ,
A lambda calculus for quantum computation with classical control, Mathematical Structures in Computer Science, vol.16, issue.3, pp.527-552, 2006. ,
URL : https://hal.archives-ouvertes.fr/hal-00483924
Collected size semantics for strict functional programs over general polymorphic lists, FOPARA, pp.143-159, 2013. ,
Polynomial size analysis of first-order shapely functions, Logical Methods in Computer Science, vol.5, issue.2, 2009. ,
Polynomial size analysis of first-order functions, TLCA, pp.351-365, 2007. ,
The Pi-calculus: a Theory of Mobile Processes, 2003. ,
A Decision Method for Elementary Algebra and Geometry, 1951. ,
Light affine lambda calculus and polytime strong normalization, LICS, pp.209-220, 2001. ,
The complexity of relational query languages, STOC, pp.137-146, 1982. ,
Space cost analysis using sized types, 2008. ,
A sound type system for secure flow analysis, Journal of Computer Security, vol.4, issue.2/3, pp.167-188, 1996. ,
Type-based allocation analysis for co-recursion in lazy functional languages, ESOP, pp.787-811, 2015. ,
Recursion theoretic characterizations of complexity classes of counting functions, Theoretical Computer Science, vol.163, issue.1-2, pp.245-258, 1996. ,
Polynomially bounded matrix interpretations, of LIPIcs. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.6, 2010. ,
Matrix interpretations on polyhedral domains, RTA, vol.36, 2015. ,
Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths, Theoretical Computer Science, vol.139, issue.1-2, pp.355-362, 1995. ,
Computable Analysis: An Introduction, 2000. ,
The Formal Semantics of Programming Languages: An Introduction, 1993. ,
A note on categorical datatypes, CTCS, vol.389, pp.118-127, 1993. ,
Confluence and termination of simply typed term rewriting systems, RTA, pp.338-352, 2001. ,
, A schematic definition of quantum polynomial time computability, 2018.
, Complexity