{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T18:29:10Z","timestamp":1790965750166,"version":"4.1.0"},"reference-count":36,"publisher":"Oxford University Press (OUP)","issue":"1","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Logic Computation"],"published-print":{"date-parts":[[2016,2]]},"DOI":"10.1093\/logcom\/ext028","type":"journal-article","created":{"date-parts":[[2013,8,2]],"date-time":"2013-08-02T00:19:02Z","timestamp":1375402742000},"page":"293-335","source":"Crossref","is-referenced-by-count":5,"title":["An open logical framework"],"prefix":"10.1093","volume":"26","author":[{"given":"Furio","family":"Honsell","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marina","family":"Lenisa","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ivan","family":"Scagnetto","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Luigi","family":"Liquori","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Petar","family":"Maksimovic","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"286","published-online":{"date-parts":[[2013,7,31]]},"reference":[{"key":"2016102400372692000_26.1.293.1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00245294"},{"key":"2016102400372692000_26.1.293.2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005060022386"},{"key":"2016102400372692000_26.1.293.3","unstructured":"Barendregt H. Lambda Calculus: Its Syntax and Semantics. North Holland; 1984."},{"key":"2016102400372692000_26.1.293.4","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1093\/oso\/9780198537618.003.0002","article-title":"Lambda calculi with types","volume-title":"Handbook of Logic in Computer Science","volume":"II","author":"Barendregt","year":"1992"},{"key":"2016102400372692000_26.1.293.5","doi-asserted-by":"publisher","DOI":"10.1023\/A:1015761529444"},{"key":"2016102400372692000_26.1.293.6","doi-asserted-by":"crossref","unstructured":"Barthe G. Cirstea H. Kirchner C. Liquori L. POPL\u201803. The ACM Press; 2003. Pure pattern type systems; p. 250-261.","DOI":"10.1145\/640128.604152"},{"key":"2016102400372692000_26.1.293.7","first-page":"349","article-title":"From formal proofs to mathematical proofs: a safe, incremenental way for building in first-order decision procedures","volume":"273","author":"Blanqui","year":"2008","journal-title":"IFIP TCS"},{"key":"2016102400372692000_26.1.293.8","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1093\/mind\/IV.14.278","article-title":"What the tortoise said to achilles","volume":"4","author":"Carroll","year":"1895","journal-title":"Mind"},{"key":"2016102400372692000_26.1.293.9","unstructured":"Chlipala A. Library reflection. http:\/\/adam.chlipala.net\/cpdt\/html\/Reflection.html ."},{"key":"2016102400372692000_26.1.293.10","unstructured":"Cirstea H. Kirchner C. Liquori L. FOSSACS\u201801, Vol. 2030 of LNCS. 2001. The rho cube; p. 166-180."},{"key":"2016102400372692000_26.1.293.11","doi-asserted-by":"crossref","unstructured":"Cousineau D. Dowek G. Embedding pure type systems in the lambda-pi-calculus modulo. In: Rocca S. R. , editor. Typed Lambda Calculi and Applications, Vol. 4583 of Lecture Notes in Computer Science. Springer Berlin Heidelberg; 2007. p. 102-117.","DOI":"10.1007\/978-3-540-73228-0_9"},{"key":"2016102400372692000_26.1.293.12","doi-asserted-by":"crossref","unstructured":"Crary K. ICFP \u201810. ACM; 2010. Higher-order representation of substructural logics; p. 131-142.","DOI":"10.1145\/1863543.1863565"},{"key":"2016102400372692000_26.1.293.13","doi-asserted-by":"crossref","unstructured":"de Bruijn N. Automation and Reasoning, Vol. 2, of Classical Papers on Computational Logic 1967\u20131970. Springer Verlag; 1968. Automath, a language for mathematics; p. 159-200.","DOI":"10.1007\/978-3-642-81955-1_11"},{"key":"2016102400372692000_26.1.293.14","doi-asserted-by":"publisher","DOI":"10.1023\/A:1027357912519"},{"key":"2016102400372692000_26.1.293.15","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"2016102400372692000_26.1.293.16","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006430"},{"key":"2016102400372692000_26.1.293.17","first-page":"399","article-title":"A framework for defining logical frameworks","volume":"172","author":"Honsell","year":"2007","journal-title":"Volume in Honor of G. Plotkin, ENTCS"},{"key":"2016102400372692000_26.1.293.18","doi-asserted-by":"crossref","unstructured":"Honsell F. Lenisa M. Liquori L. Maksimovic P. Scagnetto I. Technical report. Italy: Universit\u00e0 di Udine; 2012. LF P \u2013 a logical framework with external predicates. www.dimi.uniud.it\/scagnetto\/Papers\/lfp-full.pdf .","DOI":"10.1093\/logcom\/ext028"},{"key":"2016102400372692000_26.1.293.19","doi-asserted-by":"crossref","unstructured":"Honsell F. Lenisa M. Liquori L. Maksimovic P. Scagnetto I. Proceedings of the seventh international workshop on Logical frameworks and meta-languages, theory and practice, LFMTP 2012. ACM Digital Library; 2012. LF P \u2013 a logical framework with external predicates; p. 13-22.","DOI":"10.1145\/2364406.2364409"},{"key":"2016102400372692000_26.1.293.20","doi-asserted-by":"crossref","unstructured":"Honsell F. Lenisa M. Liquori L. Scagnetto I. LPAR\u201808, Vol. 5330 of LNCS. Springer; 2008. A conditional logical framework; p. 143-157.","DOI":"10.1007\/978-3-540-89439-1_10"},{"key":"2016102400372692000_26.1.293.21","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00095-5"},{"key":"2016102400372692000_26.1.293.22","doi-asserted-by":"crossref","unstructured":"Licata D. Harper R. ICFP \u201809. ACM; 2009. A universe of binding and computation; p. 123-134.","DOI":"10.1145\/1596550.1596571"},{"key":"2016102400372692000_26.1.293.23","unstructured":"Meyer B. Advances in Object-Oriented Software Engineering. Englewood Cliffs, NJ: Prentice Hall; 1991. Design by contract; p. 1-50."},{"key":"2016102400372692000_26.1.293.24","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1352582.1352591","article-title":"Contextual model type theory","volume":"9","author":"Nanevski","year":"2008","journal-title":"ACM Transactions on Computational Logic"},{"key":"2016102400372692000_26.1.293.25","unstructured":"Pfenning F. LICS\u201893. 1993. Intensionality, extensionality, and proof irrelevance in modal type theory; p. 221-230."},{"key":"2016102400372692000_26.1.293.26","unstructured":"Pfenning F. Schuermann C. Twelf user's guide, chapter 6: constraint domains. Online at http:\/\/www.cs.cmu.edu\/~twelf\/guide-1-4\/twelf_6.html. Accessed January 2013."},{"key":"2016102400372692000_26.1.293.27","doi-asserted-by":"crossref","unstructured":"Pientka B. Dunfield J. PPDP\u201808. ACM; 2008. Programming with proofs and explicit contexts; p. 163-173.","DOI":"10.1145\/1389449.1389469"},{"key":"2016102400372692000_26.1.293.28","doi-asserted-by":"crossref","unstructured":"Pientka B. Dunfield J. Automated Reasoning, Vol. 6173 of Lecture Notes in Computer Science. Berlin \/ Heidelberg: Springer; 2010. Beluga: a framework for programming and reasoning with deductive systems (system description); p. 15-21.","DOI":"10.1007\/978-3-642-14203-1_2"},{"key":"2016102400372692000_26.1.293.29","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"2016102400372692000_26.1.293.30","unstructured":"Poincar\u00e9 H. La Science et l'Hypoth\u00e8se. Paris: Flammarion; 1902."},{"key":"2016102400372692000_26.1.293.31","doi-asserted-by":"crossref","unstructured":"Polakow J. Pfenning F. Natural deduction for intuitionistic non-commutative linear logic. In: Girard J.-Y. , editor. Typed Lambda Calculi and Applications \u201899, Vol. 1581 of Lecture Notes in Computer Science. Springer; 1999. p. 295-309.","DOI":"10.1007\/3-540-48959-2_21"},{"key":"2016102400372692000_26.1.293.32","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.120"},{"key":"2016102400372692000_26.1.293.33","unstructured":"Shopenhauer A. Il mondo come volont\u00e0 e rappresentazione. Newton Compton; 2011."},{"key":"2016102400372692000_26.1.293.34","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.121"},{"key":"2016102400372692000_26.1.293.35","unstructured":"Virga R. Higher-Order Rewriting with Dependent Types. Pittsburgh: Carnegie Mellon University; 1999. PhD thesis."},{"key":"2016102400372692000_26.1.293.36","doi-asserted-by":"crossref","unstructured":"Watkins K. Cervesato I. Pfenning F. Walker D. Technical Report CMU-CS-02-101. School of Computer Science, Carnegie-Mellon University; 2002. A concurrent logical framework I: judgments and properties.","DOI":"10.21236\/ADA418517"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/26\/1\/293\/7950810\/ext028.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,15]],"date-time":"2024-05-15T22:32:20Z","timestamp":1715812340000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article-lookup\/doi\/10.1093\/logcom\/ext028"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,7,31]]},"references-count":36,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2016,1,28]]},"published-print":{"date-parts":[[2016,2]]}},"alternative-id":["10.1093\/logcom\/ext028"],"URL":"https:\/\/doi.org\/10.1093\/logcom\/ext028","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,7,31]]}}}