{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:32:32Z","timestamp":1759638752963,"version":"3.41.2"},"reference-count":18,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2011,3,16]],"date-time":"2011-03-16T00:00:00Z","timestamp":1300233600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We present a Curry-style second-order type system with union and intersection\ntypes for the lambda-calculus with constructors of Arbiser, Miquel and Rios, an\nextension of lambda-calculus with a pattern matching mechanism for variadic\nconstructors. We then prove the strong normalisation and the absence of match\nfailure for a restriction of this system, by adapting the standard reducibility\nmethod.<\/jats:p>","DOI":"10.2168\/lmcs-7(1:2)2011","type":"journal-article","created":{"date-parts":[[2011,9,23]],"date-time":"2011-09-23T12:18:47Z","timestamp":1316780327000},"source":"Crossref","is-referenced-by-count":3,"title":["Semantics of Typed Lambda-Calculus with Constructors"],"prefix":"10.46298","volume":"Volume 7, Issue 1","author":[{"given":"Barbara","family":"Petit","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2011,3,16]]},"reference":[{"key":"10.2168\/LMCS-7(1:2)2011_Agda","doi-asserted-by":"crossref","unstructured":"The agda proof assistant. http:\/\/wiki.portal.chalmers.se\/agda\/. A. Arbiser, A. Miquel, and A. R\u00edos. A lambda-calculus with constructors. InRewriting Techniques and Applications, volume 4098 ofLecture Notes in Computer Science, pages 181-196. Springer, 2006.","DOI":"10.1007\/11805618_14"},{"issue":"5","key":"10.2168\/LMCS-7(1:2)2011_AAAjournal","doi-asserted-by":"crossref","first-page":"581","DOI":"10.1017\/S0956796809007369","volume":"19","author":"A. Arbiser, A. Miquel, and A. R\u00edos","year":"2009","journal-title":"Journal of Functional Programming"},{"key":"10.2168\/LMCS-7(1:2)2011_Bar84","unstructured":"H. Barendregt.The Lambda Calculus: Its Syntax and Semantics, volume 103 ofStudies in Logic and The Foundations of Mathematics. North-Holland, 1984."},{"key":"10.2168\/LMCS-7(1:2)2011_CirKir03","doi-asserted-by":"crossref","unstructured":"G. Barthe, H. Cirstea, C. Kirchner, and L. Liquori. Pure patterns type systems. InPrinciples of Programming Languages, pages 250-261, 2003.","DOI":"10.1145\/640128.604152"},{"key":"10.2168\/LMCS-7(1:2)2011_Coq","unstructured":"Y. Bertot and P. Cast\u00e9ran.Coq'Art: The Calculus of Inductive Constructions, volume 25 ofTexts in Theoretical Computer Science. EATCS, 2004."},{"key":"10.2168\/LMCS-7(1:2)2011_bondi","unstructured":"Bondi, a programming language centred on pattern-matching. http:\/\/www-staff.it.uts.edu.au\/ cbj\/bondi\/. H. Cirstea and C. Kirchner. Rho-calculus, its syntax and basic properties. In5th International Workshop on Constraints in Computational Logics, 1998."},{"issue":"3","key":"10.2168\/LMCS-7(1:2)2011_ludique","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1017\/S096012950100336X","volume":"11","author":"J.-Y. Girard","year":"2001","journal-title":"Mathematical Structures in Computer Science 2001"},{"key":"10.2168\/LMCS-7(1:2)2011_girard89","unstructured":"J.-Y. Girard, Y. Lafont, and P. Taylor.Proofs and Types. Cambridge University Press, 1989."},{"key":"10.2168\/LMCS-7(1:2)2011_snobol","unstructured":"R. E. Griswold, J. F. Poage, and I. P. Polonsky.The SNOBOL4 Programming Language. Prentice Hall, 1968."},{"key":"10.2168\/LMCS-7(1:2)2011_Haskell","doi-asserted-by":"crossref","unstructured":"P. Hudak, S. Peyton-Jones, and P. Wadler. Report on the programming language Haskell, a non-strict, purely functional language (Version 1.2). Sigplan Notices, 1992.","DOI":"10.1145\/130697.130699"},{"issue":"6","key":"10.2168\/LMCS-7(1:2)2011_Jay04","doi-asserted-by":"crossref","first-page":"911","DOI":"10.1145\/1034774.1034775","volume":"26","author":"C. B. Jay","year":"2004","journal-title":"ACM Transactions on Programming Languages and Systems 26(6):911-937, 2004"},{"key":"10.2168\/LMCS-7(1:2)2011_JayBook","doi-asserted-by":"crossref","unstructured":"C. B. Jay.Pattern Calculus: Computing with Functions and Data Structures. Springer, 2009.","DOI":"10.1007\/978-3-540-89185-7"},{"key":"10.2168\/LMCS-7(1:2)2011_JayKes06","doi-asserted-by":"crossref","unstructured":"C. B. Jay and D. Kesner. Pure pattern calculus. InEuropean Symposium on Programming, volume 3924 ofLecture Notes in Computer Science, pages 100-114. Springer, 2006.","DOI":"10.1007\/11693024_8"},{"key":"10.2168\/LMCS-7(1:2)2011_Ocaml","unstructured":"X. Leroy. The objective caml system. http:\/\/caml.inria.fr\/."},{"key":"10.2168\/LMCS-7(1:2)2011_Sml","unstructured":"R. Milner, M. Tofte, and R. Harper.The definition of Standard ML. MIT Press, 1990."},{"issue":"2\/3","key":"10.2168\/LMCS-7(1:2)2011_mitchell88","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1016\/0890-5401(88)90009-0","volume":"76","author":"J. C. Mitchell","year":"1988","journal-title":"Information and Computation"},{"key":"10.2168\/LMCS-7(1:2)2011_Petit09","doi-asserted-by":"crossref","unstructured":"B. Petit. A polymorphic type system for the lambda-calculus with constructors. InTyped Lambda Calculus and Applications, volume 5608 ofLecture Notes in Computer Science, pages 234-248, 2009.","DOI":"10.1007\/978-3-642-02273-9_18"},{"key":"10.2168\/LMCS-7(1:2)2011_colin07","doi-asserted-by":"crossref","unstructured":"C. Riba. On the stability by union of reducibility candidates. InFoundations of Software Science and Computation Structure, volume 4423 ofLecture Notes in Computer Science, pages 317-331. Springer, 2007.","DOI":"10.1007\/978-3-540-71389-0_23"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1067\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1067\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:02:40Z","timestamp":1681243360000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1067"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,3,16]]},"references-count":18,"URL":"https:\/\/doi.org\/10.2168\/lmcs-7(1:2)2011","relation":{"is-same-as":[{"id-type":"arxiv","id":"1009.3429","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1009.3429","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2011,3,16]]},"article-number":"1067"}}