{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:17:31Z","timestamp":1725470251434},"reference-count":12,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1109\/lics.2004.1319614","type":"proceedings-article","created":{"date-parts":[[2004,11,12]],"date-time":"2004-11-12T19:14:14Z","timestamp":1100286854000},"page":"202-210","source":"Crossref","is-referenced-by-count":0,"title":["The omega rule is \/spl Pi\/\/sub 2\/\/sup 0\/-hard in the \/spl lambda\/\/spl beta\/-calculus"],"prefix":"10.1109","author":[{"given":"B.","family":"Intrigila","sequence":"first","affiliation":[]},{"given":"R.","family":"Statman","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"article-title":"Introduction to HOL: a theorem proving environment for higher order logic","year":"1993","author":"gordon","key":"ref4"},{"key":"ref3","article-title":"The Coq Proof Assistant: A Tutorial: Version 7.2","author":"huet","year":"2002","journal-title":"Technical Report N 256"},{"key":"ref10","article-title":"Gentzen's notion of a direct proof","author":"statman","year":"1978","journal-title":"Handbook of Mathematical Logic"},{"key":"ref6","article-title":"Solution to a Problem of Barendregt","author":"intrigila","year":"0","journal-title":"unpublished paper"},{"key":"ref11","article-title":"Normal varieties of combinators","author":"statman","year":"1988","journal-title":"Mathematics Department Research Report 89&#x2013;61"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2003.05.001"},{"key":"ref12","article-title":"Numeration, ?-calculus and arith-metic","author":"visser","year":"1980","journal-title":"To H B Curry Essays on combinatory logic lambda calculus and formalism"},{"journal-title":"Theory of Recursive Functions and Effective Computability","year":"1967","author":"rogers","key":"ref8"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(87)90040-6"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-66473-1"},{"journal-title":"The Lambda Calculus","year":"1984","author":"barendregt","key":"ref1"}],"event":{"name":"Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004.","start":{"date-parts":[[2004,7,17]]},"location":"Turku, Finland","end":{"date-parts":[[2004,7,17]]}},"container-title":["Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004."],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/9221\/29239\/01319614.pdf?arnumber=1319614","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,13]],"date-time":"2017-03-13T22:14:24Z","timestamp":1489443264000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1319614\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"references-count":12,"URL":"https:\/\/doi.org\/10.1109\/lics.2004.1319614","relation":{},"subject":[],"published":{"date-parts":[[2004]]}}}