{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T11:02:13Z","timestamp":1740135733586,"version":"3.37.3"},"reference-count":23,"publisher":"Cambridge University Press (CUP)","issue":"3-4","license":[{"start":{"date-parts":[[2018,8,10]],"date-time":"2018-08-10T00:00:00Z","timestamp":1533859200000},"content-version":"unspecified","delay-in-days":40,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2018,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>First-order resolution has been used for type inference for many years, including in Hindley-Milner type inference, type-classes, and constrained data types. Dependent types are a new trend in functional languages. In this paper, we show that proof-relevant first-order resolution can play an important role in automating type inference and term synthesis for dependently typed languages. We propose a calculus that translates type inference and term synthesis problems in a dependently typed language to a logic program and a goal in the proof-relevant first-order Horn clause logic. The computed answer substitution and proof term then provide a solution to the given type inference and term synthesis problem. We prove the decidability and soundness of our method.<\/jats:p>","DOI":"10.1017\/s1471068418000212","type":"journal-article","created":{"date-parts":[[2018,8,10]],"date-time":"2018-08-10T09:44:17Z","timestamp":1533894257000},"page":"484-501","source":"Crossref","is-referenced-by-count":2,"title":["Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis"],"prefix":"10.1017","volume":"18","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8177-1322","authenticated-orcid":false,"given":"FRANTI\u0160EK","family":"FARKA","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"EKATERINA","family":"KOMENDANTSKYA","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"KEVIN","family":"HAMMOND","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2018,8,10]]},"reference":[{"key":"S1471068418000212_ref18","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/978-3-642-14203-1_2","volume-title":"Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings","author":"Pientka","year":"2010"},{"key":"S1471068418000212_ref10","first-page":"96","volume-title":"Proceedings of the 12th Symposium on Dynamic Languages, DLS 2016, Amsterdam, The Netherlands, November 1, 2016","author":"Hemann","year":"2016"},{"key":"S1471068418000212_ref19","first-page":"40","volume-title":"Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings","author":"Slama","year":"2017"},{"key":"S1471068418000212_ref5","first-page":"311","volume-title":"Logic-Based Program Synthesis and Transformation - 26th International Symposium, LOPSTR 2016, Edinburgh, UK, September 6-8, 2016, Revised Selected Papers","author":"Farka","year":"2016"},{"key":"S1471068418000212_ref15","first-page":"35","article-title":"Type inference with constrained types","volume":"5","author":"Odersky","year":"1999","journal-title":"TAPOS"},{"key":"S1471068418000212_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"S1471068418000212_ref7","unstructured":"Fu P. , Komendantskaya E. , Schrijvers T. , and Pond A. 2016. Proof relevant corecursive resolution. See Kiselyov and King (2016), 126\u2013143."},{"key":"S1471068418000212_ref16","unstructured":"Peyton Jones S. , Jones M. , and Meijer E. 1997. Type classes: an exploration of the design space. In Haskell workshop."},{"key":"S1471068418000212_ref4","doi-asserted-by":"crossref","DOI":"10.1145\/3122955","volume-title":"Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell, Oxford, United Kingdom, September 7-8, 2017","author":"Diatchki","year":"2017"},{"key":"S1471068418000212_ref22","first-page":"1","article-title":"Refinement reflection: complete verification with SMT","volume":"2","author":"Vazou","year":"2018","journal-title":"PACMPL"},{"key":"S1471068418000212_ref12","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-29604-3","volume-title":"Functional and Logic Programming - 13th International Symposium, FLOPS 2016, Kochi, Japan, March 4-6, 2016, Proceedings","author":"Kiselyov","year":"2016"},{"key":"S1471068418000212_ref23","first-page":"1","article-title":"A specification for dependent types in haskell","volume":"1","author":"Weirich","year":"2017","journal-title":"PACMPL"},{"key":"S1471068418000212_ref1","unstructured":"Ahn K. Y. and Vezzosi A. 2016. Executable relational specifications of polymorphic type systems using prolog. See Kiselyov and King (2016), 109\u2013125."},{"key":"S1471068418000212_ref21","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006569"},{"key":"S1471068418000212_ref8","first-page":"95","article-title":"An introduction to small scale reflection in Coq","volume":"3","author":"Gonthier","year":"2010","journal-title":"J. Formalized Reasoning"},{"key":"S1471068418000212_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-016-0403-1"},{"key":"S1471068418000212_ref17","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000408"},{"key":"S1471068418000212_ref2","unstructured":"Bottu G. , Karachalias G. , Schrijvers T. , d. S. Oliveira B. C. , and Wadler P. 2017. Quantified class constraints. See Diatchki (2017), 148\u2013161."},{"key":"S1471068418000212_ref11","unstructured":"Karachalias G. and Schrijvers T. 2017. Elaboration on functional dependencies: functional dependencies are dead, long live functional dependencies! See Diatchki (2017), 133\u2013147."},{"key":"S1471068418000212_ref20","first-page":"167","volume-title":"Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002.","author":"Stuckey","year":"2002"},{"key":"S1471068418000212_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"S1471068418000212_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139021326"},{"key":"S1471068418000212_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/1042038.1042041"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068418000212","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,29]],"date-time":"2022-08-29T00:56:39Z","timestamp":1661734599000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068418000212\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7]]},"references-count":23,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2018,7]]}},"alternative-id":["S1471068418000212"],"URL":"https:\/\/doi.org\/10.1017\/s1471068418000212","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"type":"print","value":"1471-0684"},{"type":"electronic","value":"1475-3081"}],"subject":[],"published":{"date-parts":[[2018,7]]}}}