{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T19:31:54Z","timestamp":1673292714560},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2012,4]]},"abstract":"\n We present a type system for an extension of lambda calculus with a conditional construction, named STA\n B<\/jats:sub>\n , that characterizes the PSPACE class. This system is obtained by extending STA, a type assignment for lambda-calculus inspired by Lafont\u2019s Soft Linear Logic and characterizing the PTIME class. We extend STA by means of a ground type and terms for Booleans and conditional. The key issue in the design of the type system is to manage the contexts in the rule for conditional in an additive way. Thanks to this rule, we are able to program polynomial time Alternating Turing Machines. From the well-known result APTIME = PSPACE, it follows that STA\n B<\/jats:sub>\n is complete for PSPACE.\n <\/jats:p>\n Conversely, inspired by the simulation of Alternating Turing machines by means of Deterministic Turing machine, we introduce a call-by-name evaluation machine with two memory devices in order to evaluate programs in polynomial space. As far as we know, this is the first characterization of PSPACE that is based on lambda calculus and light logics.<\/jats:p>","DOI":"10.1145\/2159531.2159540","type":"journal-article","created":{"date-parts":[[2012,4,24]],"date-time":"2012-04-24T18:41:10Z","timestamp":1335292870000},"page":"1-36","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["An Implicit Characterization of PSPACE"],"prefix":"10.1145","volume":"13","author":[{"given":"Marco","family":"Gaboardi","sequence":"first","affiliation":[{"name":"Universit\u00e0 degli Studi di Bologna"}]},{"given":"Jean-Yves","family":"Marion","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Lorraine"}]},{"given":"Simona","family":"Ronchi Della Rocca","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Torino"}]}],"member":"320","published-online":{"date-parts":[[2012,4]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the 4th Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, 71--79","author":"Abiteboul S.","unstructured":"Abiteboul , S. and Vianu , V . 1989. Fixpoint extensions of first-order logic and datalog-like languages . In Proceedings of the 4th Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, 71--79 . Abiteboul, S. and Vianu, V. 1989. Fixpoint extensions of first-order logic and datalog-like languages. In Proceedings of the 4th Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, 71--79."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/504077.504081"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021863"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2008.08.005"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_7"},{"key":"e_1_2_1_6_1","volume-title":"Revised Ed","author":"Barendregt H.","unstructured":"Barendregt , H. 1984. The Lambda Calculus: Its Syntax and Semantics , Revised Ed . Elsevier . Barendregt, H. 1984. The Lambda Calculus: Its Syntax and Semantics, Revised Ed. Elsevier."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(00)00006-3"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322243"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_11"},{"key":"e_1_2_1_10_1","first-page":"4","article-title":"Light logics and the call-by-value lambda calculus","volume":"4","author":"Coppola P.","year":"2008","unstructured":"Coppola , P. , Dal Lago , U. , and Ronchi Della Rocca , S. 2008 . Light logics and the call-by-value lambda calculus . Logic. Meth. Comput. Sci. 4 , 4 . Coppola, P., Dal Lago, U., and Ronchi Della Rocca, S. 2008. Light logics and the call-by-value lambda calculus. Logic. Meth. Comput. Sci. 4, 4.","journal-title":"Logic. Meth. Comput. Sci."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_12"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111053"},{"key":"e_1_2_1_13_1","unstructured":"Gaboardi M. 2007. Linearity: An analytic tool in the study of complexity and semantics of programming languages. Ph.D. thesis Universit\u00e0 degli Studi di Torino---Institut National Polytechnique de Lorraine. Gaboardi M. 2007. Linearity: An analytic tool in the study of complexity and semantics of programming languages. Ph.D. thesis Universit\u00e0 degli Studi di Torino---Institut National Polytechnique de Lorraine."},{"key":"e_1_2_1_14_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 16th Conference in Computer Science Logic","author":"Gaboardi M.","unstructured":"Gaboardi , M. and Ronchi Della Rocca , S. 2007. A soft type assignment system for \u03bb-calculus . In Proceedings of the 16th Conference in Computer Science Logic . Lecture Notes in Computer Science , vol. 4646 , Springer , 253--267. Gaboardi, M. and Ronchi Della Rocca, S. 2007. A soft type assignment system for \u03bb-calculus. In Proceedings of the 16th Conference in Computer Science Logic. Lecture Notes in Computer Science, vol. 4646, Springer, 253--267."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzp019"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328456"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.03.066"},{"key":"e_1_2_1_18_1","unstructured":"Girard J.-Y. 1972. Interpr\u00e9tation fonctionelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Th\u00e8se de doctorat d\u2019\u00e9tat Universit\u00e9 Paris VII. Girard J.-Y. 1972. Interpr\u00e9tation fonctionelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Th\u00e8se de doctorat d\u2019\u00e9tat Universit\u00e9 Paris VII."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2700"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90363-K"},{"key":"e_1_2_1_21_1","unstructured":"Gr\u00e4del E. Kolaitis P. Libkin L. Marx M. Spencer J. Vardi M. Venema Y. and Weinstein S. 2007. Finite Model Theory and Its Applications. Springer. Gr\u00e4del E. Kolaitis P. Libkin L. Marx M. Spencer J. Vardi M. Venema Y. and Weinstein S. 2007. Finite Model Theory and Its Applications . Springer."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/788021.788962"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00009-9"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800003889"},{"key":"e_1_2_1_25_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 6th Symposium on Theoretical Aspects of Computer Science","author":"Kahn G.","unstructured":"Kahn , G. 1987. Natural semantics . In Proceedings of the 6th Symposium on Theoretical Aspects of Computer Science . Lecture Notes in Computer Science , vol. 247 , Springer-Verlag , 22--39. Kahn, G. 1987. Natural semantics. In Proceedings of the 6th Symposium on Theoretical Aspects of Computer Science. Lecture Notes in Computer Science, vol. 247, Springer-Verlag, 22--39."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9018-9"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.10.018"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/645891.671419"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/647844.736567"},{"key":"e_1_2_1_30_1","volume-title":"-Y","author":"Leivant D.","year":"1997","unstructured":"Leivant , D. and Marion , J . -Y . 1997 . Predicative functional recurrence and poly-space. In Theory and Practice of Software Development. Lecture Notes in Computer Science, vol. 1214 , Springer-Verlag , 369--380. Leivant, D. and Marion, J.-Y. 1997. Predicative functional recurrence and poly-space. In Theory and Practice of Software Development. Lecture Notes in Computer Science, vol. 1214, Springer-Verlag, 369--380."},{"key":"e_1_2_1_31_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 6th International Conference on Typed Lambda Calculi and Applications","author":"Maurel F.","unstructured":"Maurel , F. 2003. Nondeterministic light logics and NP-time . In Proceedings of the 6th International Conference on Typed Lambda Calculi and Applications . Lecture Notes in Computer Science , vol. 2701 , Springer , 241--255. Maurel, F. 2003. Nondeterministic light logics and NP-time. In Proceedings of the 6th International Conference on Typed Lambda Calculi and Applications. Lecture Notes in Computer Science, vol. 2701, Springer, 241--255."},{"key":"e_1_2_1_32_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the Seminar on Proof Theory in Computer Science","author":"Oitavem I.","unstructured":"Oitavem , I. 2001. Implicit characterizations of pspace . In Proceedings of the Seminar on Proof Theory in Computer Science . Lecture Notes in Computer Science , vol. 2183 , Springer , 170--190. Oitavem, I. 2001. Implicit characterizations of pspace. In Proceedings of the Seminar on Proof Theory in Computer Science. Lecture Notes in Computer Science, vol. 2183, Springer, 170--190."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200610056"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2004.03.009"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(70)80006-X"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/11874683_40"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.45"},{"key":"e_1_2_1_38_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 5th International Conference on Typed Lambda Calculi and Applications","author":"Schubert A.","unstructured":"Schubert , A. 2001. The complexity of beta-reduction in low orders . In Proceedings of the 5th International Conference on Typed Lambda Calculi and Applications . Lecture Notes in Computer Science , vol. 2044 , Springer , 400--414. Schubert, A. 2001. The complexity of beta-reduction in low orders. In Proceedings of the 5th International Conference on Typed Lambda Calculi and Applications. Lecture Notes in Computer Science, vol. 2044, Springer, 400--414."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(76)90061-X"},{"key":"e_1_2_1_40_1","volume-title":"2nd Workshop on Implicit Computational Complexity.","author":"Terui K.","year":"2000","unstructured":"Terui , K. 2000 . Linear logical characterization of polyspace functions (extended abstract) . 2nd Workshop on Implicit Computational Complexity. Terui, K. 2000. Linear logical characterization of polyspace functions (extended abstract). 2nd Workshop on Implicit Computational Complexity."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802186"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2159531.2159540","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T19:01:02Z","timestamp":1672340462000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2159531.2159540"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,4]]},"references-count":41,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,4]]}},"alternative-id":["10.1145\/2159531.2159540"],"URL":"http:\/\/dx.doi.org\/10.1145\/2159531.2159540","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":["Computational Mathematics","Logic","General Computer Science","Theoretical Computer Science"],"published":{"date-parts":[[2012,4]]},"assertion":[{"value":"2010-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-04-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}