{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T05:21:14Z","timestamp":1737091274196,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540432876"},{"type":"electronic","value":"9783540458425"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45842-5_10","type":"book-chapter","created":{"date-parts":[[2007,5,27]],"date-time":"2007-05-27T00:00:38Z","timestamp":1180224038000},"page":"145-159","source":"Crossref","is-referenced-by-count":1,"title":["Formalizing the Halting Problem in a Constructive Type Theory"],"prefix":"10.1007","author":[{"given":"Kristofer","family":"Johannisson","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,2,14]]},"reference":[{"issue":"3","key":"10_CR1","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1145\/828.1882","volume":"31","author":"R. S. Boyer","year":"1984","unstructured":"R. S. Boyer and J. St. Moore. A mechanical proof of the unsolvability of the halting problem. Journal of the Association for Computing Machinery, 31(3):441\u2013458, 1984.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"R. Constable and S. Smith. Computational foundations of basic recursive function theory. In Third IEEE Symposium on Logic in Computer Science, pages 360\u2013371, Edinburgh, Scotland, July 1988.","DOI":"10.1109\/LICS.1988.5133"},{"key":"10_CR3","unstructured":"Catarina Coquand. Homepage for Agda. URL: http:\/\/www.cs.chalmers.se\/~catarina\/agda\/ ."},{"key":"10_CR4","unstructured":"Thierry Coquand. Structured type theory. Postscript format, URL: http:\/\/www.cs.chalmers.se\/~coquand\/STT.ps.Z ."},{"key":"10_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/3-540-11157-3_38","volume-title":"Algorithms in Modern Mathematics and Computer Science","author":"A. P. Ershov","year":"1981","unstructured":"A. P. Ershov. Abstract computability on algebraic structures. In Algorithms in Modern Mathematics and Computer Science, volume 122 of Lecture Notes in Computer Science, pages 397\u2013420, Berlin, Heidelberg, New York, 1981. Springer-Verlag."},{"key":"10_CR6","unstructured":"Zohar Manna. Mathematical Theory of Computation. McGraw-Hill Book Company, 1974."},{"key":"10_CR7","volume-title":"Computability","author":"G. J. Tourlakis","year":"1984","unstructured":"George J. Tourlakis. Computability. Reston Publishing Company Inc., Reston, Virginia 22090, 1984."},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Eric G. Wagner. Uniformly Reflexive Structures: On the nature of g\u00f6delizations and relative computability. Transactions of the American Mathematical Society, 144:1\u201341, October 1969.","DOI":"10.2307\/1995267"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45842-5_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T18:23:57Z","timestamp":1737051837000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45842-5_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540432876","9783540458425"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/3-540-45842-5_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}