{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T23:06:16Z","timestamp":1773097576331,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540255932","type":"print"},{"value":"9783540320142","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11417170_16","type":"book-chapter","created":{"date-parts":[[2010,12,16]],"date-time":"2010-12-16T19:29:35Z","timestamp":1292527775000},"page":"209-220","source":"Crossref","is-referenced-by-count":20,"title":["On the Degeneracy of \u03a3-Types in Presence of Computational Classical Logic"],"prefix":"10.1007","author":[{"given":"Hugo","family":"Herbelin","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","unstructured":"The Coq development team: The Coq Proof Assistant Reference Manual, Version\u00a08.0 (2004), Available at \n                    \n                      http:\/\/coq.inria.fr\/doc"},{"key":"#cr-split#-16_CR2.1","unstructured":"Coquand, T.: Metamathematical investigations of a calculus of constructions. In: Odifreddi, P. (ed.) Logic and Computer Science. Apic Series, vol.??31, pp. 91???122. Academic Press, London (1990);"},{"key":"#cr-split#-16_CR2.2","unstructured":"Also INRIA Research Report number 1088 (september 1989)"},{"issue":"6","key":"16_CR3","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1017\/S0956796899003512","volume":"9","author":"T. Crolard","year":"1999","unstructured":"Crolard, T.: A confluent lambda-calculus with a catch\/throw mechanism. Journal of Functional Programming\u00a09(6), 625\u2013647 (1999)","journal-title":"Journal of Functional Programming"},{"key":"16_CR4","unstructured":"Felleisen, M., Friedman, D.P., Kohlbecker, E., Duba, B.F.: Reasoning with continuations. In: First Symposium on Logic and Computer Science, pp. 131\u2013141 (1986)"},{"key":"16_CR5","first-page":"47","volume-title":"Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages, POPL 1990","author":"T.G. Griffin","year":"1990","unstructured":"Griffin, T.G.: The formulae-as-types notion of control. In: Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages, POPL 1990, San Francisco, CA, USA, January 17-19, pp. 47\u201357. ACM Press, New York (1990)"},{"key":"16_CR6","unstructured":"Martin-L\u00f6f, P.: Intuitionistic Type Theory. Bibliopolis (1984)"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/BFb0013061","volume-title":"Logic Programming and Automated Reasoning","author":"M. Parigot","year":"1992","unstructured":"Parigot, M.: Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol.\u00a0624, pp. 190\u2013201. Springer, Heidelberg (1992)"},{"key":"16_CR8","unstructured":"Pottinger, G.: Definite descriptions and excluded middle in the theory of constructions, Communication to the TYPES electronic mailing list (1989)"},{"key":"16_CR9","volume-title":"Natural Deduction - A Proof-Theoretical Study","author":"D. Prawitz","year":"1965","unstructured":"Prawitz, D.: Natural Deduction - A Proof-Theoretical Study. Almqvist & Wiksell, Stockholm (1965)"},{"key":"16_CR10","doi-asserted-by":"publisher","first-page":"840","DOI":"10.2307\/2274575","volume":"53","author":"J.M. Smith","year":"1988","unstructured":"Smith, J.M.: The independence of Peano\u2019s fourth axiom from Martin-L\u00f6f\u2019s type theory without universes. Journal of Symbolic Logic\u00a053, 840\u2013845 (1988)","journal-title":"Journal of Symbolic Logic"},{"key":"16_CR11","first-page":"1","volume-title":"Recursive Function Theory: Proc. Symposia in Pure Mathematics","author":"C. Spector","year":"1962","unstructured":"Spector, C.: Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics. In: Recursive Function Theory: Proc. Symposia in Pure Mathematics, vol.\u00a05, pp. 1\u201327. American Mathematical Society, Providence (1962)"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11417170_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:03:48Z","timestamp":1619507028000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11417170_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540255932","9783540320142"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/11417170_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}