{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,7]],"date-time":"2025-12-07T16:01:49Z","timestamp":1765123309097,"version":"3.40.5"},"reference-count":21,"publisher":"Cambridge University Press (CUP)","issue":"8","license":[{"start":{"date-parts":[[2018,4,17]],"date-time":"2018-04-17T00:00:00Z","timestamp":1523923200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2019,9]]},"abstract":"<jats:p>A new approach to inhabitation problems in simply typed lambda-calculus is shown, dealing with both decision and counting problems. This approach works by exploiting a representation of the search space generated by a given inhabitation problem, which is in terms of a lambda-calculus for proof search that the authors developed recently. The representation may be seen as extending the Curry\u2013Howard representation of proofs by lambda terms. Our methodology reveals inductive descriptions of the decision problems, driven by the syntax of the proof-search expressions, and produces simple, recursive decision procedures and counting functions. These allow to predict the number of inhabitants by testing the given type for syntactic criteria. This new approach is comprehensive and robust: based on the same syntactic representation, we also derive the state-of-the-art coherence theorems ensuring uniqueness of inhabitants.<\/jats:p>","DOI":"10.1017\/s0960129518000099","type":"journal-article","created":{"date-parts":[[2018,4,17]],"date-time":"2018-04-17T04:42:16Z","timestamp":1523940136000},"page":"1092-1124","source":"Crossref","is-referenced-by-count":3,"title":["Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search"],"prefix":"10.1017","volume":"29","author":[{"given":"JOS\u00c9","family":"ESP\u00cdRITO SANTO","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7299-2411","authenticated-orcid":false,"given":"RALPH","family":"MATTHES","sequence":"additional","affiliation":[]},{"given":"LU\u00cdS","family":"PINTO","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2018,4,17]]},"reference":[{"key":"S0960129518000099_ref6","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exi016"},{"key":"S0960129518000099_ref10","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009862"},{"key":"S0960129518000099_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511608865"},{"key":"S0960129518000099_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2015.05.004"},{"key":"S0960129518000099_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21691-6_8"},{"key":"S0960129518000099_ref21","unstructured":"Wells J. B. and Yakobowski B. (2004). Graph-based proof counting and enumeration with applications for program fragment synthesis. In: Proceedings of LOPSTR 2004, LNCS, vol. 3573, Springer, 262\u2013277."},{"key":"S0960129518000099_ref16","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139021326"},{"volume-title":"Introduction to Automata Theory, Languages and Computation","year":"1979","author":"Hopcroft","key":"S0960129518000099_ref14"},{"key":"S0960129518000099_ref15","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.07.041"},{"key":"S0960129518000099_ref12","unstructured":"Esp\u00edrito Santo J. , Matthes R. , and Pinto L. (2016). A coinductive approach to proof search through typed lambda-calculi. Available at http:\/\/arxiv.org\/abs\/1602.04382v2."},{"key":"S0960129518000099_ref2","unstructured":"Aoto T. and Ono H. (1994). Uniqueness of normal forms in \u2192, \u2227-fragment of NJ. Technical report, Research Report IS-RR-94-0024F."},{"key":"S0960129518000099_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139032636"},{"key":"S0960129518000099_ref17","first-page":"453","article-title":"A coherence theorem for cartesian closed categories (abstract)","volume":"44","author":"Mints","year":"1979","journal-title":"The Journal of Symbolic Logic"},{"key":"S0960129518000099_ref20","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0027"},{"key":"S0960129518000099_ref18","first-page":"213","volume-title":"Selected papers in proof theory","author":"Mints","year":"1992"},{"key":"S0960129518000099_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44602-7_26"},{"key":"S0960129518000099_ref19","unstructured":"Schubert A. , Dekkers W. and Barendregt H. P. (2015). Automata theoretic account of proof search. In: Kreutzer S. (ed.), Proceedings CSL 2015, LIPIcs, vol. 41, Schloss Dagstuhl, 128\u2013143."},{"key":"S0960129518000099_ref4","unstructured":"Ben-Yelles C.-B. (1979). Type Assignment in the Lambda-Calculus: Syntax & Semantics. PhD thesis, University College of Swansea."},{"key":"S0960129518000099_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-009-0119-5"},{"key":"S0960129518000099_ref9","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxn029"},{"key":"S0960129518000099_ref11","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.126.3"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129518000099","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T10:25:37Z","timestamp":1570530337000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129518000099\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,4,17]]},"references-count":21,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2019,9]]}},"alternative-id":["S0960129518000099"],"URL":"https:\/\/doi.org\/10.1017\/s0960129518000099","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2018,4,17]]}}}