{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:13:07Z","timestamp":1775790787728,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642122507","type":"print"},{"value":"9783642122514","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12251-4_1","type":"book-chapter","created":{"date-parts":[[2010,4,9]],"date-time":"2010-04-09T23:32:42Z","timestamp":1270855962000},"page":"1-12","source":"Crossref","is-referenced-by-count":22,"title":["Beluga: Programming with Dependent Types, Contextual Data, and Contexts"],"prefix":"10.1007","author":[{"given":"Brigitte","family":"Pientka","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"Agda wiki (2009), http:\/\/wiki.portal.chalmers.se\/agda\/"},{"key":"1_CR2","volume-title":"Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. In: Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)"},{"key":"1_CR3","first-page":"259","volume-title":"Proceedings of the Joint International Conference and Symposium on Logic Programming","author":"G. Dowek","year":"1996","unstructured":"Dowek, G., Hardin, T., Kirchner, C., Pfenning, F.: Unification via explicit substitutions: The case of higher-order patterns. In: Maher, M. (ed.) Proceedings of the Joint International Conference and Symposium on Logic Programming, Bonn, Germany, pp. 259\u2013273. MIT Press, Cambridge (1996)"},{"key":"1_CR4","series-title":"ENTCS","first-page":"69","volume-title":"International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008)","author":"J. Dunfield","year":"2009","unstructured":"Dunfield, J., Pientka, B.: Case analysis of higher-order data. In: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008). ENTCS, vol.\u00a0228, pp. 69\u201384. Elsevier, Amsterdam (2009)"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Felty, A.P., Pientka, B.: Reasoning with higher-order abstract syntax and contexts: A comparison. Technical report, School of Computer Science, McGill University (January 2010)","DOI":"10.1007\/978-3-642-14052-5_17"},{"key":"1_CR6","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"W.D. Goldfarb","year":"1981","unstructured":"Goldfarb, W.D.: The undecidability of the second-order unification problem. Theoretical Computer Science\u00a013, 225\u2013230 (1981)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"1_CR7","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the ACM\u00a040(1), 143\u2013184 (1993)","journal-title":"Journal of the ACM"},{"key":"1_CR8","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/1596550.1596571","volume-title":"14th ACM SIGPLAN International Conference on Functional Programming","author":"D.R. Licata","year":"2009","unstructured":"Licata, D.R., Harper, R.: A universe of binding and computation. In: Hutton, G., Tolmach, A.P. (eds.) 14th ACM SIGPLAN International Conference on Functional Programming, pp. 123\u2013134. ACM Press, New York (2009)"},{"key":"1_CR9","first-page":"255","volume-title":"Eighth International Logic Programming Conference","author":"D. Miller","year":"1991","unstructured":"Miller, D.: Unification of simply typed lambda-terms as logic programming. In: Eighth International Logic Programming Conference, Paris, France, pp. 255\u2013269. MIT Press, Cambridge (1991)"},{"issue":"1","key":"1_CR10","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1017\/S0956796803004829","volume":"14","author":"C. McBride","year":"2004","unstructured":"McBride, C., McKinna, J.: The view from the left. Journal of Functional Programming\u00a014(1), 69\u2013111 (2004)","journal-title":"Journal of Functional Programming"},{"key":"1_CR11","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1145\/263699.263712","volume-title":"24th Annual Symposium on Principles of Programming Languages (POPL 1997)","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof-carrying code. In: 24th Annual Symposium on Principles of Programming Languages (POPL 1997), pp. 106\u2013119. ACM Press, New York (1997)"},{"key":"1_CR12","unstructured":"Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, Technical Report 33D (September 2007)"},{"issue":"3","key":"1_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1352582.1352591","volume":"9","author":"A. Nanevski","year":"2008","unstructured":"Nanevski, A., Pfenning, F., Pientka, B.: Contextual modal type theory. ACM Transactions on Computational Logic\u00a09(3), 1\u201349 (2008)","journal-title":"ACM Transactions on Computational Logic"},{"key":"1_CR14","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1145\/1389449.1389469","volume-title":"ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2008)","author":"B. Pientka","year":"2008","unstructured":"Pientka, B., Dunfield, J.: Programming with proofs and explicit contexts. In: ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2008), pp. 163\u2013173. ACM Press, New York (2008)"},{"key":"1_CR15","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1017\/CBO9780511569807.008","volume-title":"Logical Frameworks","author":"F. Pfenning","year":"1991","unstructured":"Pfenning, F.: Logic programming in the LF logical framework. In: Huet, G., Plotkin, G. (eds.) Logical Frameworks, pp. 149\u2013181. Cambridge University Press, Cambridge (1991)"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Pfenning, F.: Unification and anti-unification in the Calculus of Constructions. In: Sixth Annual IEEE Symposium on Logic in Computer Science, Amsterdam, The Netherlands, July 1991, pp. 74\u201385 (1991)","DOI":"10.1109\/LICS.1991.151632"},{"key":"1_CR17","unstructured":"Pfenning, F.: Computation and deduction (1997)"},{"key":"1_CR18","unstructured":"Pientka, B.: Tabled higher-order logic programming. PhD thesis, Department of Computer Science, Carnegie Mellon University, CMU-CS-03-185 (2003)"},{"issue":"2","key":"1_CR19","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/s10817-005-6534-3","volume":"34","author":"B. Pientka","year":"2005","unstructured":"Pientka, B.: Verifying termination and reduction properties about higher-order logic programs. Journal of Automated Reasoning\u00a034(2), 179\u2013207 (2005)","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR20","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1145\/1328438.1328483","volume-title":"35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2008)","author":"B. Pientka","year":"2008","unstructured":"Pientka, B.: A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In: 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2008), pp. 371\u2013382. ACM Press, New York (2008)"},{"key":"1_CR21","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1109\/LICS.2007.44","volume-title":"22nd IEEE Symposium on Logic in Computer Science (LICS 2007)","author":"F. Pottier","year":"2007","unstructured":"Pottier, F.: Static name control for FreshML. In: 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), pp. 356\u2013365. IEEE Computer Society, Los Alamitos (2007)"},{"key":"1_CR22","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Automated Deduction - CADE-16","author":"F. Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf \u2014 a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-78739-6_7","volume-title":"Programming Languages and Systems","author":"A.B. Poswolsky","year":"2008","unstructured":"Poswolsky, A.B., Sch\u00fcrmann, C.: Practical programming with higher-order encodings and dependent types. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 93\u2013107. Springer, Heidelberg (2008)"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1007\/3-540-61055-3_44","volume-title":"Programming Languages and Systems - ESOP \u201996","author":"E. Rohwedder","year":"1996","unstructured":"Rohwedder, E., Pfenning, F.: Mode and termination checking for higher-order logic programs. In: Riis Nielson, H. (ed.) ESOP 1996. LNCS, vol.\u00a01058, pp. 296\u2013310. Springer, Heidelberg (1996)"},{"key":"1_CR25","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1145\/944705.944729","volume-title":"8th International Conference on Functional Programming (ICFP 2003)","author":"M.R. Shinwell","year":"2003","unstructured":"Shinwell, M.R., Pitts, A.M., Gabbay, M.J.: FreshML: programming with binders made simple. In: 8th International Conference on Functional Programming (ICFP 2003), pp. 263\u2013274. ACM Press, New York (2003)"},{"key":"1_CR26","unstructured":"Twelf wiki (2009), http:\/\/twelf.plparty.org\/wiki\/Main_Page"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12251-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T22:23:13Z","timestamp":1740003793000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12251-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642122507","9783642122514"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12251-4_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}