{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:12:26Z","timestamp":1761610346802,"version":"build-2065373602"},"reference-count":12,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":5688,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[1998]]},"DOI":"10.1016\/s1571-0661(05)01178-3","type":"journal-article","created":{"date-parts":[[2005,4,13]],"date-time":"2005-04-13T14:20:46Z","timestamp":1113402046000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["Embedding First-Order Tableaux into a Pure Type System"],"prefix":"10.1016","volume":"17","author":[{"given":"Michael","family":"Franssen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"issue":"4","key":"10.1016\/S1571-0661(05)01178-3_bib1","first-page":"432","article-title":"Apt. Ten years of Hoare's logic: A survey \u2013 part I","volume":"3","author":"Krzysztof","year":"1981","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/S1571-0661(05)01178-3_bib2","series-title":"Lambda Calculi with Types, volume 2 of Handbook of Logic in Computer Science","first-page":"118","author":"Barendregt","year":"1992"},{"key":"10.1016\/S1571-0661(05)01178-3_bib3","unstructured":"S Berardi. Towards a mathematical analysis of the Coquand-Huet calculus of constructions and the other systems in Barendregt's cube. Technical report, Dept. of Computer Science, Carnegie-Mellon University and Dipartimento Matem\u00e1tica, Universita di Torino, 1988."},{"key":"10.1016\/S1571-0661(05)01178-3_bib4","doi-asserted-by":"crossref","unstructured":"L.S. van Benthem Jutting, J. McKinna, and R. Pollack. Checking algorithms for pure type systems. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Propositions: International Workshop TYPES'93, volume 806 of LNCS, pages 19\u201361, Nijmegen, May 1993. Springer-Verlag 1994.","DOI":"10.1007\/3-540-58085-9_71"},{"key":"10.1016\/S1571-0661(05)01178-3_bib6","unstructured":"Michael Franssen. Tools for the construction of correct programs: an overview. Technical Report Report 97\u201306, Eindhoven University of Technology, 1997."},{"key":"10.1016\/S1571-0661(05)01178-3_bib7","unstructured":"J.H. Geuvers. Logics and Type Systems. PhD thesis, Catholic University of Nijmegen, 1993."},{"key":"10.1016\/S1571-0661(05)01178-3_bib8","unstructured":"T. Laan. The Evolution of Type Theory in Logic and Mathematics. PhD thesis, Eindhoven University of Technology, 1997."},{"author":"LEGO","key":"10.1016\/S1571-0661(05)01178-3_bib9"},{"key":"10.1016\/S1571-0661(05)01178-3_bib10","unstructured":"Twan Laan and Michael Franssen. Embedding first-order logic in a pure type system with parameters. Submitted for publication."},{"year":"1994","series-title":"Selected Papers on Automath, volume 133 of Studies in Logic and The Foundations of Mathematics","key":"10.1016\/S1571-0661(05)01178-3_bib11"},{"key":"10.1016\/S1571-0661(05)01178-3_bib12","unstructured":"J Terlouw. Een nadere bewijstheoretische analyse van GSTT's. Technical report, Department of Computer Science, University of Nijmegen, 1989."},{"author":"Zwanenburg","key":"10.1016\/S1571-0661(05)01178-3_bib13"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105011783?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105011783?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:06:26Z","timestamp":1761609986000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105011783"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"references-count":12,"alternative-id":["S1571066105011783"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)01178-3","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Embedding First-Order Tableaux into a Pure Type System","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(05)01178-3","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 1998 Elsevier Science B.V. Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}