{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:52Z","timestamp":1751660512102,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662466681"},{"type":"electronic","value":"9783662466698"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46669-8_28","type":"book-chapter","created":{"date-parts":[[2015,4,1]],"date-time":"2015-04-01T14:37:37Z","timestamp":1427899057000},"page":"685-709","source":"Crossref","is-referenced-by-count":5,"title":["Full Reduction in the Face of Absurdity"],"prefix":"10.1007","author":[{"given":"Gabriel","family":"Scherer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Didier","family":"R\u00e9my","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"28_CR1","doi-asserted-by":"crossref","unstructured":"Boespflug, M., D\u00e9n\u00e8s, M., Gr\u00e9goire, B.: Full reduction at full throttle. In: Certified Programs and Proofs, CPP (2011)","DOI":"10.1007\/978-3-642-25379-9_26"},{"key":"28_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-540-24849-1_8","volume-title":"Types for Proofs and Programs","author":"E. Brady","year":"2004","unstructured":"Brady, E., McBride, C., McKinna, J.: Inductive families need not store their indices. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 115\u2013129. Springer, Heidelberg (2004)"},{"issue":"1","key":"28_CR3","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/S0304-3975(97)00250-8","volume":"198","author":"N. \u00c7a\u011fman","year":"1998","unstructured":"\u00c7a\u011fman, N., Hindley, J.R.: Combinatory weak reduction in lambda calculus. Theoretical Computer Science\u00a0198(1), 239\u2013247 (1998)","journal-title":"Theoretical Computer Science"},{"key":"28_CR4","unstructured":"Cardelli, L.: An implementation of FSub. Research Report\u00a097 (1993)"},{"key":"28_CR5","unstructured":"Cretin, J.: Erasable coercions: a unified approach to type systems. PhD thesis, Universit\u00e9 Paris-Diderot, Paris 7 (2014)"},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"Cretin, J., R\u00e9my, D.: System F with Coercion Constraints. In: Logics In Computer Science (LICS), ACM (July 2014)","DOI":"10.1145\/2603088.2603128"},{"issue":"9","key":"28_CR7","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1145\/583852.581501","volume":"37","author":"B. Gr\u00e9goire","year":"2002","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. ACM SIGPLAN Notices\u00a037(9), 235\u2013246 (2002)","journal-title":"ACM SIGPLAN Notices"},{"key":"28_CR8","unstructured":"Hendriks, D., van Oostrom, V.: adbmal. In: CADE (2003)"},{"key":"28_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/978-3-540-74915-8_20","volume-title":"Computer Science Logic","author":"D. Kesner","year":"2007","unstructured":"Kesner, D.: The theory of calculi with explicit substitutions revisited. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol.\u00a04646, pp. 238\u2013252. Springer, Heidelberg (2007)"},{"key":"28_CR10","doi-asserted-by":"crossref","unstructured":"Le Botlan, D., R\u00e9my, D.: MLF: Raising ML to the power of System-F. In: ICFP 1980 (August 2003)","DOI":"10.1145\/944705.944709"},{"key":"28_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-39185-1_12","volume-title":"Types for Proofs and Programs","author":"P. Letouzey","year":"2003","unstructured":"Letouzey, P.: A New Extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol.\u00a02646, pp. 200\u2013219. Springer, Heidelberg (2003)"},{"key":"28_CR12","doi-asserted-by":"crossref","unstructured":"Mitchell, J.C.: Polymorphic type inference and containment. Information and Computation\u00a02\/3(76) (1988)","DOI":"10.1016\/0890-5401(88)90009-0"},{"key":"28_CR13","volume-title":"Programming in Martin-L\u00f6fs type theory","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.M.: Programming in Martin-L\u00f6fs type theory. Oxford University Press, Oxford (1990)"},{"issue":"4","key":"28_CR14","first-page":"312","volume":"7","author":"F. Pottier","year":"2000","unstructured":"Pottier, F.: A versatile constraint-based type inference system. Nordic Journal of Computing\u00a07(4), 312\u2013347 (2000)","journal-title":"Nordic Journal of Computing"},{"key":"28_CR15","doi-asserted-by":"crossref","unstructured":"Simonet, V., Pottier, F.: A constraint-based approach to guarded algebraic data types. TOPLAS\u00a029(1) (2007)","DOI":"10.1145\/1180475.1180476"},{"key":"28_CR16","doi-asserted-by":"crossref","unstructured":"Sulzmann, M., Chakravarty, M.M.T., Jones, S.L.P., Donnelly, K.: System f with type equality coercions. In: TLDI, pp. 53\u201366 (2007)","DOI":"10.1145\/1190315.1190324"},{"issue":"1","key":"28_CR17","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1006\/inco.1995.1057","volume":"118","author":"M. Takahashi","year":"1995","unstructured":"Takahashi, M.: Parallel reductions in lambda-calculus. Inf. Comput.\u00a0118(1), 120\u2013127 (1995)","journal-title":"Inf. Comput."},{"key":"28_CR18","unstructured":"Vytiniotis, D., Jones, S.P.: Practical aspects of evidence-based compilation in system FC (2011)"},{"key":"28_CR19","doi-asserted-by":"crossref","unstructured":"Weirich, S., Hsu, J., Eisenberg, R.A.: System FC with explicit kind equality. In: ICFP, pp. 275\u2013286 (2013)","DOI":"10.1145\/2544174.2500599"},{"issue":"2","key":"28_CR20","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1017\/S0956796806006216","volume":"17","author":"H. Xi","year":"2007","unstructured":"Xi, H.: Dependent ml an approach to practical programming with dependent types. J. Funct. Program.\u00a017(2), 215\u2013286 (2007)","journal-title":"J. Funct. Program."}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46669-8_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T14:29:21Z","timestamp":1559140161000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46669-8_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466681","9783662466698"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46669-8_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}