{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:29Z","timestamp":1780994609697,"version":"3.54.1"},"reference-count":33,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2013,10,18]],"date-time":"2013-10-18T00:00:00Z","timestamp":1382054400000},"content-version":"unspecified","delay-in-days":47,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2013,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Many components of a dependently typed programming language are by now well understood, for example, the underlying type theory, type checking, unification and evaluation. How to combine these components into a realistic and usable high-level language is, however, folklore, discovered anew by successive language implementors. In this paper, I describe the implementation of\n                    <jats:sc>Idris<\/jats:sc>\n                    , a new dependently typed functional programming language.\n                    <jats:sc>Idris<\/jats:sc>\n                    is intended to be a\n                    <jats:italic>general-purpose<\/jats:italic>\n                    programming language and as such provides high-level concepts such as implicit syntax, type classes and\n                    <jats:monospace>do<\/jats:monospace>\n                    notation. I describe the high-level language and the underlying type theory, and present a tactic-based method for\n                    <jats:italic>elaborating<\/jats:italic>\n                    concrete high-level syntax with implicit arguments and type classes into a fully explicit type theory. Furthermore, I show how this method facilitates the implementation of new high-level language constructs.\n                  <\/jats:p>","DOI":"10.1017\/s095679681300018x","type":"journal-article","created":{"date-parts":[[2013,10,18]],"date-time":"2013-10-18T06:48:19Z","timestamp":1382078899000},"page":"552-593","source":"Crossref","is-referenced-by-count":208,"title":["Idris, a general-purpose dependently typed programming language: Design and implementation"],"prefix":"10.1017","volume":"23","author":[{"given":"EDWIN","family":"BRADY","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2013,10,18]]},"reference":[{"key":"S095679681300018X_ref33","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000098"},{"key":"S095679681300018X_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"S095679681300018X_ref29","unstructured":"Norell U. (2007). Towards a Practical Programming Language Based on Dependent Type Theory, PhD thesis, Chalmers University of Technology, Sweden."},{"key":"S095679681300018X_ref25","volume-title":"Types for Proofs and Programs (TYPES 2006)","author":"McBride","year":"2006"},{"key":"S095679681300018X_ref23","unstructured":"McBride C. (1999) Dependently Typed Functional Programs and their Proofs, PhD thesis, University of Edinburgh, Edinburgh, UK."},{"key":"S095679681300018X_ref22","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538356.001.0001","volume-title":"Computation and Reasoning: A Type Theory for Computer Science","author":"Luo","year":"1994"},{"key":"S095679681300018X_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/373243.360210"},{"key":"S095679681300018X_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211308"},{"key":"S095679681300018X_ref14","first-page":"227","volume-title":"Proceedings of the First IEEE Symposium on Logic in Computer Science ( LICS'86)","author":"Coquand","year":"1986"},{"key":"S095679681300018X_ref12","volume-title":"Sixth Symposium on Trends in Functional Programming","author":"Chapman","year":"2005"},{"key":"S095679681300018X_ref28","doi-asserted-by":"publisher","DOI":"10.1016\/0747-7171(92)90011-R"},{"key":"S095679681300018X_ref6","unstructured":"Brady E. (2005) Practical Implementation of a Dependently Typed Functional Programming Language, PhD thesis, University of Durham, Durham, NC."},{"key":"S095679681300018X_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"S095679681300018X_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_5"},{"key":"S095679681300018X_ref7","first-page":"145","volume-title":"Implementation and Application of Functional Languages (IFL'06)","author":"Brady","year":"2006"},{"key":"S095679681300018X_ref26","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"S095679681300018X_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22438-6_7"},{"key":"S095679681300018X_ref27","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006326"},{"key":"S095679681300018X_ref8","volume-title":"Proceedings of the International Symposium on Trends in Functional Programming (TFP11)","author":"Brady","year":"2011"},{"key":"S095679681300018X_ref30","first-page":"50","volume-title":"International Conference on Functional Programming (ICFP '06)","author":"Peyton Jones","year":"2006"},{"key":"S095679681300018X_ref18","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002864"},{"key":"S095679681300018X_ref9","volume-title":"Proceedings of the 5th ACM Workshop on Programming Languages Meets Program Verification (PLPV '11)","author":"Brady","year":"2011"},{"key":"S095679681300018X_ref11","volume-title":"Types for Proofs and Programs (TYPES 2003)","author":"Brady","year":"2003"},{"key":"S095679681300018X_ref21","doi-asserted-by":"crossref","unstructured":"L\u00f6h A. , McBride C. & Swierstra W. (2010) A tutorial implementation of a dependently typed lambda calculus. Fundamenta Informaticae 102(2), 177\u2013207.","DOI":"10.3233\/FI-2010-304"},{"key":"S095679681300018X_ref31","volume-title":"Informal Proceedings of First Workshop on Logical Frameworks, Antibes","author":"Pollack","year":"1990"},{"key":"S095679681300018X_ref3","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:18)2012"},{"key":"S095679681300018X_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44622-2_21"},{"key":"S095679681300018X_ref13","volume-title":"Proceedings of 15th ACM SIGPLAN International Conference on Functional Programming (ICFP '10)","author":"Chapman","year":"2010"},{"key":"S095679681300018X_ref10","unstructured":"Brady E. (2013). Programming in Idris : A Tutorial. Available at http:\/\/www.idris-lang.org\/documentation\/."},{"key":"S095679681300018X_ref24","volume-title":"Types for Proofs and Programs (TYPES 2000)","author":"McBride","year":"2000"},{"key":"S095679681300018X_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44404-1_7"},{"key":"S095679681300018X_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15975-4_48"},{"key":"S095679681300018X_ref19","volume-title":"Proceedings of the 6th ACM workshop on Programming Languages Meets Program Verification (PLPV '12)","author":"Kimmell","year":"2012"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S095679681300018X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:30Z","timestamp":1779834990000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S095679681300018X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9]]},"references-count":33,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2013,9]]}},"alternative-id":["S095679681300018X"],"URL":"https:\/\/doi.org\/10.1017\/s095679681300018x","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,9]]}}}