{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T16:38:21Z","timestamp":1761323901307,"version":"3.41.2"},"reference-count":39,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,6,20]],"date-time":"2012-06-20T00:00:00Z","timestamp":1340150400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"DOI":"10.13039\/501100001665","name":"French National Research Agency","doi-asserted-by":"crossref","award":["ANR-10-BLAN-0305"],"award-info":[{"award-number":["ANR-10-BLAN-0305"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001665","name":"French National Research Agency","doi-asserted-by":"crossref","award":["ANR-07-BLAN-0324"],"award-info":[{"award-number":["ANR-07-BLAN-0324"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We prove \"untyping\" theorems: in some typed theories (semirings, Kleene\nalgebras, residuated lattices, involutive residuated lattices), typed equations\ncan be derived from the underlying untyped equations. As a consequence, the\ncorresponding untyped decision procedures can be extended for free to the typed\nsettings. Some of these theorems are obtained via a detour through fragments of\ncyclic linear logic, and give rise to a substantial optimisation of standard\nproof search algorithms.<\/jats:p>","DOI":"10.2168\/lmcs-8(2:13)2012","type":"journal-article","created":{"date-parts":[[2013,9,23]],"date-time":"2013-09-23T14:50:43Z","timestamp":1379947843000},"source":"Crossref","is-referenced-by-count":1,"title":["Untyping Typed Algebras and Colouring Cyclic Linear Logic"],"prefix":"10.46298","volume":"Volume 8, Issue 2","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1220-4399","authenticated-orcid":false,"given":"Damien","family":"Pous","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,6,20]]},"reference":[{"issue":"2","key":"10.2168\/LMCS-8(2:13)2012_Adams06","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1017\/S0956796805005770","volume":"16","author":"R. Adams","year":"2006","journal-title":"J. Funct. Program."},{"issue":"3","key":"10.2168\/LMCS-8(2:13)2012_Andreoli92:focalisation","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J.-M. Andreoli","year":"1992","journal-title":"Journal of Logic and Computation"},{"key":"10.2168\/LMCS-8(2:13)2012_BellinF98","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/s001530050101","volume":"37","author":"G. Bellin and A. Fleury","year":"1998","journal-title":"Archive for Mathematical Logic"},{"key":"10.2168\/LMCS-8(2:13)2012_BellinS94","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/0304-3975(94)00104-9","volume":"135","author":"G. Bellin and P. Scott","year":"1994","journal-title":"TCS"},{"doi-asserted-by":"crossref","unstructured":"T. Braibant and D. Pous. An efficient Coq tactic for deciding Kleene algebras. InProc. ITP, volume 6172 ofLNCS, pages 163-178. Springer, 2010.","key":"10.2168\/LMCS-8(2:13)2012_atbr:itp","DOI":"10.1007\/978-3-642-14052-5_13"},{"doi-asserted-by":"crossref","unstructured":"P. Burmeister. Partial algebra -- an introductory survey. InAlgebras and Orders, volume 389 ofNATO ASI, pages 1-70. Kluwer Pub., 1993.","key":"10.2168\/LMCS-8(2:13)2012_burmeister:partialalgebra","DOI":"10.1007\/978-94-017-0697-1_1"},{"issue":"23-24","key":"10.2168\/LMCS-8(2:13)2012_Diaconescu09","doi-asserted-by":"crossref","first-page":"1245","DOI":"10.1016\/j.ipl.2009.09.008","volume":"109","author":"R. Diaconescu","year":"2009","journal-title":"Inf. Process. Lett."},{"issue":"4","key":"10.2168\/LMCS-8(2:13)2012_DBLP:journals\/fuin\/Dojer04","first-page":"375","volume":"63","author":"N. Dojer","year":"2004","journal-title":"Fund. Inf."},{"issue":"1-2","key":"10.2168\/LMCS-8(2:13)2012_DBW97","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/S0304-3975(96)00154-5","volume":"179","author":"H. Doornbos, R. Backhouse, and J. van de","year":"1997","journal-title":"TCS"},{"unstructured":"P. Freyd and A. Scedrov.Categories, Allegories. North Holland, 1990.","key":"10.2168\/LMCS-8(2:13)2012_FreydScedrov90"},{"key":"10.2168\/LMCS-8(2:13)2012_galatos2007residuated","first-page":"532","volume":"151","author":"N. Galatos, P. Jipsen, T. Kowalski, and","year":"2007","journal-title":"Stud. in Log. and Found. of Math."},{"unstructured":"H. Geuvers and B. Werner. On the Church-Rosser property for expressive type systems and its consequences for their metatheoretic study. InProc. LICS, pages 320-329. IEEE, 1994.","key":"10.2168\/LMCS-8(2:13)2012_GeuversWerner94"},{"key":"10.2168\/LMCS-8(2:13)2012_Girard87:ll","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","journal-title":"TCS"},{"doi-asserted-by":"crossref","unstructured":"B. Gr\u00e9goire and A. Mahboubi. Proving equalities in a commutative ring done right in Coq. InProc. TPHOLs, volume 3603 ofLNCS, pages 98-113. Springer, 2005.","key":"10.2168\/LMCS-8(2:13)2012_GregoireM05","DOI":"10.1007\/11541868_7"},{"doi-asserted-by":"crossref","unstructured":"J. Harrison. A HOL decision procedure for elementary real algebra. InHUG, volume 780 ofLNCS, pages 426-435. Springer, 1993.","key":"10.2168\/LMCS-8(2:13)2012_Harrison93","DOI":"10.1007\/3-540-57826-9_153"},{"key":"10.2168\/LMCS-8(2:13)2012_higgins:manysorted","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1002\/mana.19630270108","volume":"27","author":"P. Higgins","year":"1963","journal-title":"Math. Nach."},{"key":"10.2168\/LMCS-8(2:13)2012_Hindley69","first-page":"29","volume":"146","author":"R. Hindley","year":"1969","journal-title":"Transactions of the American Mathematical Society 1969"},{"issue":"2","key":"10.2168\/LMCS-8(2:13)2012_Jipsen04","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1023\/B:STUD.0000032089.54776.63","volume":"76","author":"P. Jipsen","year":"2004","journal-title":"Stud. Log."},{"doi-asserted-by":"crossref","unstructured":"P. Jipsen and C. Tsinakis. A survey of residuated lattices.Ord. Alg. Struct., 2002.","key":"10.2168\/LMCS-8(2:13)2012_Jipsen:Survey","DOI":"10.1007\/978-1-4757-3627-4_3"},{"unstructured":"M. Kanovich. The complexity of neutrals in linear logic. InProc. LICS, pages 486-495. IEEE, 1995.","key":"10.2168\/LMCS-8(2:13)2012_kanovich65"},{"doi-asserted-by":"crossref","unstructured":"S. C. Kleene. Representation of events in nerve nets and finite automata. InAutomata Studies, pages 3-41. Princeton University Press, 1956.","key":"10.2168\/LMCS-8(2:13)2012_Kle56","DOI":"10.1515\/9781400882618-002"},{"issue":"2","key":"10.2168\/LMCS-8(2:13)2012_Koz94b","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1006\/inco.1994.1037","volume":"110","author":"D. Kozen","year":"1994","journal-title":"Inf. and Comput."},{"issue":"3","key":"10.2168\/LMCS-8(2:13)2012_K97c","first-page":"427","volume":"19","author":"D. Kozen","year":"1997","journal-title":"Trans. PLS"},{"unstructured":"D. Kozen. Typed Kleene algebra. Technical Report 98-1669, Cornell Univ., 1998.","key":"10.2168\/LMCS-8(2:13)2012_Koz98b"},{"issue":"2","key":"10.2168\/LMCS-8(2:13)2012_Krob91a","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1016\/0304-3975(91)90395-I","volume":"89","author":"D. Krob","year":"1991","journal-title":"TCS"},{"key":"10.2168\/LMCS-8(2:13)2012_Lambek58","doi-asserted-by":"crossref","first-page":"154","DOI":"10.2307\/2310058","volume":"65","author":"J. Lambek","year":"1958","journal-title":"American Mathematical Monthly"},{"issue":"3","key":"10.2168\/LMCS-8(2:13)2012_Milner78","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R. Milner","year":"1978","journal-title":"J. Comput. Syst. Sci."},{"issue":"2","key":"10.2168\/LMCS-8(2:13)2012_Mossakowski02","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1016\/S0304-3975(01)00369-3","volume":"286","author":"T. Mossakowski","year":"2002","journal-title":"TCS"},{"doi-asserted-by":"crossref","unstructured":"M. Norrish. Complete integer decision procedures as derived rules in HOL. InProc. TPHOLs, volume 2758 ofLNCS, pages 71-86. Springer, 2003.","key":"10.2168\/LMCS-8(2:13)2012_Norrish03","DOI":"10.1007\/10930755_5"},{"issue":"2","key":"10.2168\/LMCS-8(2:13)2012_OkadaT99","doi-asserted-by":"crossref","first-page":"790","DOI":"10.2307\/2586501","volume":"64","author":"M. Okada and K. Terui","year":"1999","journal-title":"J. Sym. Log."},{"issue":"1","key":"10.2168\/LMCS-8(2:13)2012_OnoK85","doi-asserted-by":"crossref","first-page":"169","DOI":"10.2307\/2273798","volume":"50","author":"H. Ono and Y. Komori","year":"1985","journal-title":"J. Sym. Log."},{"issue":"1-3","key":"10.2168\/LMCS-8(2:13)2012_Pentus06","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1016\/j.tcs.2006.03.018","volume":"357","author":"M. Pentus","year":"2006","journal-title":"TCS"},{"doi-asserted-by":"crossref","unstructured":"D. Pous. Web appendix for pous:csl10:utas and this paper, http:\/\/perso.ens-lyon.fr\/damien.pous\/utas. D. Pous. Untyping typed algebraic structures and colouring proof nets of cyclic linear logic. InProc. CSL, volume 6247 ofLNCS, pages 484-498. Springer, August 2010.","key":"10.2168\/LMCS-8(2:13)2012_this:web","DOI":"10.1007\/978-3-642-15205-4_37"},{"doi-asserted-by":"crossref","unstructured":"V. R. Pratt. Action logic and pure induction. InProc. JELIA, volume 478 ofLNCS, pages 97-120. Springer, 1990.","key":"10.2168\/LMCS-8(2:13)2012_Pratt90","DOI":"10.1007\/BFb0018436"},{"key":"10.2168\/LMCS-8(2:13)2012_redko64","first-page":"120","volume":"16","author":"V. Redko","year":"1964","journal-title":"Ukrain. Mat. Z."},{"unstructured":"L. Regnier.Lambda-calcul et r\u00e9seaux. Th\u00e8se de doctorat, Univ. Paris VII, 1992.","key":"10.2168\/LMCS-8(2:13)2012_regnierPhD"},{"doi-asserted-by":"crossref","unstructured":"V. Siles and H. Herbelin. Equality is typable in semi-full pure type systems. InProc. LICS, pages 21-30. IEEE, 2010.","key":"10.2168\/LMCS-8(2:13)2012_SilesHerbelin10","DOI":"10.1109\/LICS.2010.19"},{"key":"10.2168\/LMCS-8(2:13)2012_Wille03:involrl","doi-asserted-by":"crossref","first-page":"449","DOI":"10.1007\/s00012-005-1957-6","volume":"54","author":"A. Wille","year":"2005","journal-title":"Alg. Univ."},{"issue":"1","key":"10.2168\/LMCS-8(2:13)2012_Yetter90","doi-asserted-by":"crossref","first-page":"41","DOI":"10.2307\/2274953","volume":"55","author":"D. Yetter","year":"1990","journal-title":"J. Sym. Log."}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/718\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/718\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:54:34Z","timestamp":1681242874000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/718"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,20]]},"references-count":39,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(2:13)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1205.3612","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1205.3612","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,6,20]]},"article-number":"718"}}