{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:39:51Z","timestamp":1750307991308,"version":"3.41.0"},"reference-count":17,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2006,4,1]],"date-time":"2006-04-01T00:00:00Z","timestamp":1143849600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2006,4]]},"abstract":"<jats:p>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","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"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","published-online":{"date-parts":[[2006,4]]},"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.","unstructured":"Asperti , A. and Guerrini , S . 1998 . The Optimal Implementation of Functional Programming Languages. Cambridge Tracts in Theoretical Computer Science , vol. 45 . Cambridge University Press.]] Asperti, A. and Guerrini, S. 1998. The Optimal Implementation of Functional Programming Languages. Cambridge Tracts in Theoretical Computer Science, vol. 45. Cambridge University Press.]]"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/647319.721016"},{"volume-title":"Laboratoire d'Informatique de Paris Nord, Universit\u00e9 Paris 13","author":"Baillot P.","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.","unstructured":"Benton , N. , Bierman , G. , de Paiva , V. , and Hyland , M . 1993. A term calculus for intuitionistic linear logic. In Typed Lambda Calculus and Applications . In Proceedings of the 1st International Conference, (TLCA'93 , Utrecht), M. Benzen and J. Groote, eds. Lecture Notes in Computer Science , vol. 664 . Springer, 75--90.]] Benton, N., Bierman, G., de Paiva, V., and Hyland, M. 1993. A term calculus for intuitionistic linear logic. In Typed Lambda Calculus and Applications. In Proceedings of the 1st International Conference, (TLCA'93, Utrecht), M. Benzen and J. Groote, eds. Lecture Notes in Computer Science, vol. 664. Springer, 75--90.]]"},{"key":"e_1_2_1_7_1","volume-title":"5th International Conference, (TLCA","volume":"2044","author":"Coppola P.","year":"2001","unstructured":"Coppola , P. and Martini , S . 2001. Typing lambda terms in elementary logic with linear constraints. In Typed Lambda Calculi and Applications , 5th International Conference, (TLCA 2001 , Krakow), S. Abramsky, ed. Lecture Notes in Computer Science , vol. 2044 . Springer, 76--90.]] Coppola, P. and Martini, S. 2001. Typing lambda terms in elementary logic with linear constraints. In Typed Lambda Calculi and Applications, 5th International Conference, (TLCA 2001, Krakow), S. Abramsky, ed. Lecture Notes in Computer Science, vol. 2044. Springer, 76--90.]]"},{"key":"e_1_2_1_8_1","volume-title":"6th International Conference, (TLCA","volume":"2701","author":"Coppola P.","year":"2003","unstructured":"Coppola , P. and Rocca , S. R. D. 2003. Principal typing in elementary affine logic. In Typed Lambda Calculi and Applications , 6th International Conference, (TLCA 2003 , Valencia) M. Hofmann, ed. Lecture Notes in Computer Science , vol. 2701 . Springer, 90--104.]] Coppola, P. and Rocca, S. R. D. 2003. Principal typing in elementary affine logic. In Typed Lambda Calculi and Applications, 6th International Conference, (TLCA 2003, Valencia) M. Hofmann, ed. Lecture Notes in Computer Science, vol. 2701. Springer, 90--104.]]"},{"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_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96711"},{"volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"L\u00e9vy J.-J.","key":"e_1_2_1_14_1","unstructured":"L\u00e9vy , J.-J. 1980. Optimal reductions in the lambda-calculus . In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism , J. P. Seldin and J. R. Hindley, eds. Academic Press , London , 159--191.]] L\u00e9vy, J.-J. 1980. Optimal reductions in the lambda-calculus. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J. P. Seldin and J. R. Hindley, eds. Academic Press, London, 159--191.]]"},{"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","unstructured":"Roversi , L. 1992 . A compiler from Curry-typed \u03bb-terms to linear-\u03bb-terms . In Theoretical Computer Science: Proceedings of the 4th Italian Conference World Scientific, L'Aquila (Italy), 330--344 .]] Roversi, L. 1992. A compiler from Curry-typed \u03bb-terms to linear-\u03bb-terms. In Theoretical Computer Science: Proceedings of the 4th Italian Conference World Scientific, L'Aquila (Italy), 330--344.]]"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49366-2_4"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1131313.1131315","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1131313.1131315","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:06:16Z","timestamp":1750259176000},"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":17,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2006,4]]}},"alternative-id":["10.1145\/1131313.1131315"],"URL":"https:\/\/doi.org\/10.1145\/1131313.1131315","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2006,4]]},"assertion":[{"value":"2006-04-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}