{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:36:04Z","timestamp":1753889764355,"version":"3.41.2"},"reference-count":6,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2005,10,5]],"date-time":"2005-10-05T00:00:00Z","timestamp":1128470400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/assumed-1991-2003"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>A modified realisability interpretation of infinitary logic is formalised and\nproved sound in constructive type theory (CTT). The logic considered subsumes\nfirst order logic. The interpretation makes it possible to extract programs\nwith simplified types and to incorporate and reason about them in CTT.<\/jats:p>","DOI":"10.2168\/lmcs-1(2:2)2005","type":"journal-article","created":{"date-parts":[[2005,10,5]],"date-time":"2005-10-05T07:43:14Z","timestamp":1128498194000},"source":"Crossref","is-referenced-by-count":0,"title":["Internalising modified realisability in constructive type theory"],"prefix":"10.46298","volume":"Volume 1, Issue 2","author":[{"given":"Erik","family":"Palmgren","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2005,10,5]]},"reference":[{"key":"10.2168\/LMCS-1(2:2)2005_BBSS:PfThyWo","doi-asserted-by":"crossref","unstructured":"H. Benl, U. Berger, M. Seisenberger, H. Schwichtenberg, and W. Zuber,Proof theory at work: Program development in the Minlogsystem, Automated Deduction, Vol. II (W. Bibel and P.H. Schmitt, eds.), Kluwer, 1998. U. Berger, W. Buchholz, and H. Schwichtenberg,Refined program extraction from classical proofs, Annals of Pure and Applied Logic \\textbf114 (2002), 3-25.","DOI":"10.1007\/978-94-017-0435-9_2"},{"key":"10.2168\/LMCS-1(2:2)2005_CCoquand:Agda","unstructured":"C. Coquand,The interactive theorem prover agda, Chalmers University of Technology, Department of Computer Science and Engineering, URL: \\tt www.cs.chalmers.se\/ { catarina\/agda\/}, 2000. P. Letouzey,Programmation fonctionelle certifi\u00e9e: L'extraction de programmes dans l'assistant {Coq.}, Ph.D. thesis, Universit\u00e9 de Paris Sud, 2004."},{"key":"10.2168\/LMCS-1(2:2)2005_LetouzeyThesis","unstructured":"P. Letouzey,Programmation fonctionelle certifi\u00e9e: L'extraction de programmes dans l'assistant {Coq.}, Ph.D. thesis, Universit\u00e9 de Paris Sud, 2004."},{"key":"10.2168\/LMCS-1(2:2)2005_ML:AITT","doi-asserted-by":"crossref","unstructured":"P. Martin-L\u00f6f,An intuitionistic theory of types, Twenty-Five Years of Type Theory (G. Sambin and J.M. Smith, eds.), Oxford University Press, 1998, pp. 127-172. H. Schwichtenberg,Minimal logic for computable functions., Mathematisches Institut der Universit\u00e4t M\u00fcnchen, Preprint October, 2004.","DOI":"10.1093\/oso\/9780198501275.003.0010"},{"key":"10.2168\/LMCS-1(2:2)2005_Schwicht:MLCF","unstructured":"H. Schwichtenberg,Minimal logic for computable functions., Mathematisches Institut der Universit\u00e4t M\u00fcnchen, Preprint October, 2004."},{"key":"10.2168\/LMCS-1(2:2)2005_Troelstra:Meta","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066739"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/2266\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/2266\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:11:02Z","timestamp":1681243862000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/2266"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,10,5]]},"references-count":6,"URL":"https:\/\/doi.org\/10.2168\/lmcs-1(2:2)2005","relation":{"is-same-as":[{"id-type":"arxiv","id":"math\/0505418","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.math\/0505418","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2005,10,5]]},"article-number":"2266"}}