{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T09:49:06Z","timestamp":1648547346483},"reference-count":19,"publisher":"Association for Computing Machinery (ACM)","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2006,4]]},"abstract":"We propose a type inference algorithm for lambda terms in elementary affine logic (EAL). The algorithm decorates the syntax tree of a simple typed lambda term and collects a set of linear constraints. The result is a parametric elementary type that can be instantiated with any solution of the set of collected constraints.We point out that the typeability of lambda terms in EAL has a practical counterpart, since it is possible to reduce any EAL-typeable lambda terms with the Lamping's abstract algorithm obtaining a substantial increase of performances.We show how to apply the same techniques to obtain decorations of intuitionistic proofs into linear logic proofs.<\/jats:p>","DOI":"10.1145\/1131313.1131315","type":"journal-article","created":{"date-parts":[[2006,7,25]],"date-time":"2006-07-25T14:14:26Z","timestamp":1153836866000},"page":"219-260","source":"Crossref","is-referenced-by-count":6,"title":["Optimizing optimal reduction"],"prefix":"10.1145","volume":"7","author":[{"given":"Paolo","family":"Coppola","sequence":"first","affiliation":[{"name":"Universit\u00e0 di Udine, Udine UD, Italy"}]},{"given":"Simone","family":"Martini","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Bologna, Bologna BO, Italy"}]}],"member":"320","reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/788020.788931"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325707"},{"key":"e_1_2_1_3_1","volume-title":"The Optimal Implementation of Functional Programming Languages. Cambridge Tracts in Theoretical Computer Science","volume":"45","author":"Asperti A."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/647319.721016"},{"key":"e_1_2_1_5_1","unstructured":"Baillot P. 2003. Type inference for polynomial time complexity via constraints on words. Tech. rep. Laboratoire d'Informatique de Paris Nord Universit\u00e9 Paris 13 Institut Galil\u00e9e.]] Baillot P. 2003. Type inference for polynomial time complexity via constraints on words. Tech. rep. Laboratoire d'Informatique de Paris Nord Universit\u00e9 Paris 13 Institut Galil\u00e9e.]]"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the 1st International Conference, (TLCA'93","volume":"664","author":"Benton N."},{"key":"e_1_2_1_7_1","volume-title":"5th International Conference, (TLCA","volume":"2044","author":"Coppola P.","year":"2001"},{"key":"e_1_2_1_8_1","volume-title":"6th International Conference, (TLCA","volume":"2701","author":"Coppola P.","year":"2003"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00010-5"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02390456"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2700"},{"key":"e_1_2_1_12_1","unstructured":"Kathail V. K. 1990. Optimal interpreters for lambda-calculus based functional programming languages. Ph.D. thesis MIT.]] Kathail V. K. 1990. Optimal interpreters for lambda-calculus based functional programming languages. Ph.D. thesis MIT.]]"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96711"},{"key":"e_1_2_1_14_1","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"L\u00e9vy J.-J."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90020-G"},{"key":"e_1_2_1_16_1","unstructured":"Prawitz D. 1965. Natural Deduction. Almqvist & Wiksell.]] Prawitz D. 1965. Natural Deduction. Almqvist & Wiksell.]]"},{"key":"e_1_2_1_17_1","volume-title":"Theoretical Computer Science: Proceedings of the 4th Italian Conference World Scientific, L'Aquila (Italy), 330--344","author":"Roversi L.","year":"1992"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49366-2_4"},{"key":"e_1_2_1_19_1","unstructured":"Schellinx H. 1994. The noble art of linear decorating. Ph.D. thesis Institute for Logic Language and Computation University of Amsterdam.]] Schellinx H. 1994. The noble art of linear decorating. Ph.D. thesis Institute for Logic Language and Computation University of Amsterdam.]]"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1131313.1131315","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,2,20]],"date-time":"2021-02-20T07:08:11Z","timestamp":1613804891000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1131313.1131315"}},"subtitle":["A type inference algorithm for elementary affine logic"],"short-title":[],"issued":{"date-parts":[[2006,4]]},"references-count":19,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2006,4]]}},"alternative-id":["10.1145\/1131313.1131315"],"URL":"http:\/\/dx.doi.org\/10.1145\/1131313.1131315","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":[[2006,4]]}}}