{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,5]],"date-time":"2025-03-05T05:49:31Z","timestamp":1741153771228,"version":"3.38.0"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2011,4,16]],"date-time":"2011-04-16T00:00:00Z","timestamp":1302912000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2011,5]]},"DOI":"10.1007\/s00236-011-0136-9","type":"journal-article","created":{"date-parts":[[2011,4,15]],"date-time":"2011-04-15T08:58:14Z","timestamp":1302857894000},"page":"191-211","source":"Crossref","is-referenced-by-count":1,"title":["Refined typing to localize the impact of forced strictness on free theorems"],"prefix":"10.1007","volume":"48","author":[{"given":"Daniel","family":"Seidel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Janis","family":"Voigtl\u00e4nder","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,4,16]]},"reference":[{"key":"136_CR1","unstructured":"Augustsson, L.: Putting Curry-Howard to work (Invited talk). At: Approaches and Applications of Inductive Programming (2009)"},{"key":"136_CR2","first-page":"125","volume-title":"European Symposium on Programming, Proceedings, volume 6012 of LNCS","author":"J.-P. Bernardy","year":"2010","unstructured":"Bernardy J.-P., Jansson P., Claessen K.: Testing polymorphic properties. In: Gordon, A. (ed.) European Symposium on Programming, Proceedings, volume 6012 of LNCS, pp. 125\u2013144. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-11957-6_8"},{"key":"136_CR3","doi-asserted-by":"crossref","unstructured":"Crary, K.: Logical relations and a case study in equivalence checking. In: [22], chapter6, pp. 223\u2013244 (2005)","DOI":"10.7551\/mitpress\/1104.003.0010"},{"key":"136_CR4","unstructured":"Day, N., Launchbury, J., Lewis, J.: Logical abstractions in Haskell. In: Meijer, E. (ed.) Haskell Workshop, Proceedings. Technical Report UU-CS-1999-28, Utrecht University (1999)"},{"issue":"3","key":"136_CR5","doi-asserted-by":"crossref","first-page":"795","DOI":"10.2307\/2275431","volume":"57","author":"R. Dyckhoff","year":"1992","unstructured":"Dyckhoff R.: Contraction-free sequent calculi for intuitionistic logic. J. Symb. Log. 57(3), 795\u2013807 (1992). doi: 10.2307\/2275431","journal-title":"J. Symb. Log."},{"key":"136_CR6","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1145\/1291201.1291216","volume-title":"Haskell Workshop, Proceedings","author":"J. Fernandes","year":"2007","unstructured":"Fernandes J., Pardo A., Saraiva J.: A shortcut fusion rule for circular program calculation. In: Keller, G. (ed.) Haskell Workshop, Proceedings, pp. 95\u2013106. ACM, New York (2007). doi: 10.1145\/1291201.1291216"},{"key":"136_CR7","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1145\/165180.165214","volume-title":"Functional Programming Languages and Computer Architecture, Proceedings","author":"A. Gill","year":"1993","unstructured":"Gill A., Launchbury J., Peyton Jones S.: A short cut to deforestation. In: Arvind, (ed.) Functional Programming Languages and Computer Architecture, Proceedings, pp. 223\u2013232. ACM, New York (1993). doi: 10.1145\/165180.165214"},{"key":"136_CR8","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1145\/1706356.1706379","volume-title":"Partial Evaluation and Program Manipulation, Proceedings","author":"S. Holdermans","year":"2010","unstructured":"Holdermans S., Hage J.: Making \u201cstricterness\u201d more relevant. In: Gallagher, J., Voigtl\u00e4nder, J. (eds) Partial Evaluation and Program Manipulation, Proceedings, pp. 121\u2013130. ACM, New York (2010). doi: 10.1145\/1706356.1706379"},{"key":"136_CR9","first-page":"12-1","volume-title":"History of Programming Languages, Proceedings","author":"P. Hudak","year":"2007","unstructured":"Hudak P., Hughes R., Peyton Jones S., Wadler P.: A history of Haskell: being lazy with class. In: Ryder, B., Hailpern, B. (eds) History of Programming Languages, Proceedings, pp. 12-1\u201312-55. ACM, New York (2007). doi: 10.1145\/1238844.1238856"},{"key":"136_CR10","first-page":"112","volume-title":"Programs as Data Objects 1985, Proceedings, volume 217 of LNCS","author":"R. Hughes","year":"1986","unstructured":"Hughes R.: Strictness detection in non-flat domains. In: Ganzinger, H., Jones, N. (eds) Programs as Data Objects 1985, Proceedings, volume 217 of LNCS, pp. 112\u2013135. Springer, Heidelberg (1986). doi: 10.1007\/3-540-16446-4_7"},{"issue":"4","key":"136_CR11","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1017\/S0956796802004409","volume":"13","author":"P. Johann","year":"2003","unstructured":"Johann P.: Short cut fusion is correct. J. Funct. Program. 13(4), 797\u2013814 (2003). doi: 10.1017\/S0956796802004409","journal-title":"J. Funct. Program."},{"issue":"2","key":"136_CR12","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1017\/S0960129504004578","volume":"15","author":"P. Johann","year":"2005","unstructured":"Johann P.: On proving the correctness of program transformations based on free theorems for higher-order polymorphic calculi. Math. Struct. Comput. Sci. 15(2), 201\u2013229 (2005). doi: 10.1017\/S0960129504004578","journal-title":"Math. Struct. Comput. Sci."},{"key":"136_CR13","first-page":"99","volume-title":"Principles of Programming Languages, Proceedings, volume 39(1) of ACM SIGPLAN Not.","author":"P. Johann","year":"2004","unstructured":"Johann P., Voigtl\u00e4nder J.: Free theorems in the presence of seq. In: Leroy, X. (ed.) Principles of Programming Languages, Proceedings, volume 39(1) of ACM SIGPLAN Not., pp. 99\u2013110. ACM, New York (2004). doi: 10.1145\/982962.964010"},{"issue":"1\u20132","key":"136_CR14","first-page":"63","volume":"69","author":"P. Johann","year":"2006","unstructured":"Johann P., Voigtl\u00e4nder J.: The impact of seq on free theorems-based program transformations. Fundam. Inform. 69(1\u20132), 63\u2013102 (2006)","journal-title":"Fundam. Inform."},{"key":"136_CR15","first-page":"204","volume-title":"European Symposium on Programming, Proceedings, volume 1058 of LNCS","author":"J. Launchbury","year":"1996","unstructured":"Launchbury J., Paterson R.: Parametricity and unboxing with unpointed types. In: Riis Nielson, H. (ed.) European Symposium on Programming, Proceedings, volume 1058 of LNCS, pp. 204\u2013218. Springer, Heidelberg (1996). doi: 10.1007\/3-540-61055-3_38"},{"key":"136_CR16","first-page":"269","volume-title":"Colloque International sur la Programmation, Proceedings, volume 83 of LNCS","author":"A. Mycroft","year":"1980","unstructured":"Mycroft A.: The theory and practice of transforming call-by-need into call-by-value. In: Robinet, B. (ed.) Colloque International sur la Programmation, Proceedings, volume 83 of LNCS, pp. 269\u2013281. Springer, Heidelberg (1980). doi: 10.1007\/3-540-09981-6_19"},{"key":"136_CR17","first-page":"114","volume-title":"Festschrift to Hans Langmaack: Correct System Design, Recent Insight and Advances, volume 1710 of LNCS","author":"F. Nielson","year":"1999","unstructured":"Nielson F., Riis Nielson H.: Type and effect systems. In: Olderog, E.-R., Steffen, B. (eds) Festschrift to Hans Langmaack: Correct System Design, Recent Insight and Advances, volume 1710 of LNCS, pp. 114\u2013136. Springer, Heidelberg (1999). doi: 10.1007\/3-540-48092-7_6"},{"key":"136_CR18","first-page":"109","volume-title":"Aspect-Oriented Software Development, Proceedings","author":"B. Oliveira","year":"2010","unstructured":"Oliveira B., Schrijvers T., Cook W.: EffectiveAdvice: disciplined advice with explicit effects. In: J\u00e9z\u00e9quel, J.-M., S\u00fcdholt, M. (eds) Aspect-Oriented Software Development, Proceedings, pp. 109\u2013120. ACM, New York (2010). doi: 10.1145\/1739230.1739244"},{"key":"136_CR19","volume-title":"The Implementation of Functional Programming Languages","author":"S. Peyton Jones","year":"1987","unstructured":"Peyton Jones S.: The Implementation of Functional Programming Languages. Prentice-Hall, Englewood Cliffs (1987)"},{"volume-title":"Haskell 98 Language and Libraries: The Revised Report","year":"2003","key":"136_CR20","unstructured":"Peyton Jones, S. (ed.): Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, Cambridge (2003). doi: 10.2277\/0521826144"},{"key":"136_CR21","volume-title":"Types and Programming Languages","author":"B. Pierce","year":"2002","unstructured":"Pierce B.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"volume-title":"Advanced Topics in Types and Programming Languages","year":"2005","key":"136_CR22","unstructured":"Pierce, B. (ed.): Advanced Topics in Types and Programming Languages. MIT Press, London (2005)"},{"key":"136_CR23","doi-asserted-by":"crossref","unstructured":"Pitts, A.: Typed operational reasoning. In: [22], chapter 7, pp. 245\u2013289 (2005)","DOI":"10.7551\/mitpress\/1104.003.0011"},{"key":"136_CR24","unstructured":"Plasmeijer, R., van Eekelen, M.: Clean version 2.1 language report (2002). http:\/\/clean.cs.ru.nl\/download\/Clean20\/doc\/CleanLangRep.2.1.pdf"},{"key":"136_CR25","first-page":"408","volume-title":"Colloque sur la Programmation, Proceedings, volume19 of LNCS","author":"J. Reynolds","year":"1974","unstructured":"Reynolds J.: Towards a theory of type structure. In: Robinet, B. (ed.) Colloque sur la Programmation, Proceedings, volume19 of LNCS, pp. 408\u2013423. Springer, Heidelberg (1974)"},{"key":"136_CR26","first-page":"513","volume-title":"Information Processing, Proceedings","author":"J. Reynolds","year":"1983","unstructured":"Reynolds J.: Types, abstraction and parametric polymorphism. In: Mason, R. (ed.) Information Processing, Proceedings, pp. 513\u2013523. Elsevier, Amsterdam (1983)"},{"key":"136_CR27","volume-title":"Denotational Semantics: A Methodology for Language Development","author":"D. Schmidt","year":"1986","unstructured":"Schmidt D.: Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, Boston (1986)"},{"key":"136_CR28","unstructured":"Seidel, D., Voigtl\u00e4nder, J.: Taming selective strictness. Technical report TUD-FI09-06, Technische Universit\u00e4t Dresden (2009). http:\/\/www.iai.uni-bonn.de\/jv\/TUD-FI09-06.pdf"},{"key":"136_CR29","first-page":"2916","volume-title":"Arbeitstagung Programmiersprachen, Proceedings, volume 154 of LNI","author":"D. Seidel","year":"2009","unstructured":"Seidel D., Voigtl\u00e4nder J.: Taming selective strictness. In: Dosch, W., Hanus, M. (eds) Arbeitstagung Programmiersprachen, Proceedings, volume 154 of LNI, pp. 2916\u20132930. Gesellschaft f\u00fcr Informatik, Bonn (2009)"},{"key":"136_CR30","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-3-642-12251-4_14","volume-title":"Functional and Logic Programming, Proceedings, volume 6009 of LNCS","author":"D. Seidel","year":"2010","unstructured":"Seidel D., Voigtl\u00e4nder J.: Automatically generating counterexamples to naive free theorems. In: Blume, M., Vidal, G. (eds) Functional and Logic Programming, Proceedings, volume 6009 of LNCS, pp. 175\u2013190. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-12251-4_14"},{"key":"136_CR31","first-page":"124","volume-title":"International Conference on Functional Programming, Proceedings, volume 37(9) of ACM SIGPLAN Not.","author":"J. Svenningsson","year":"2002","unstructured":"Svenningsson J.: Shortcut fusion for accumulating parameters & zip-like functions. In: Peyton Jones, S. (ed.) International Conference on Functional Programming, Proceedings, volume 37(9) of ACM SIGPLAN Not., pp. 124\u2013132. ACM, New York (2002). doi: 10.1145\/583852.581491"},{"key":"136_CR32","first-page":"29","volume-title":"Principles of Programming Languages, Proceedings, volume 43(1) of ACM SIGPLAN Not.","author":"J. Voigtl\u00e4nder","year":"2008","unstructured":"Voigtl\u00e4nder J.: Much ado about two: a pearl on parallel prefix computation. In: Wadler, P. (ed.) Principles of Programming Languages, Proceedings, volume 43(1) of ACM SIGPLAN Not., pp. 29\u201335. ACM, New York (2008). doi: 10.1145\/1328897.1328445"},{"key":"136_CR33","first-page":"13","volume-title":"Partial Evaluation and Semantics-Based Program Manipulation, Proceedings","author":"J. Voigtl\u00e4nder","year":"2008","unstructured":"Voigtl\u00e4nder J.: Proving correctness via free theorems: the case of the destroy\/build-rule. In: Gl\u00fcck, R., de Moor, O. (eds) Partial Evaluation and Semantics-Based Program Manipulation, Proceedings, pp. 13\u201320. ACM, New York (2008). doi: 10.1145\/1328408.1328412"},{"key":"136_CR34","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1007\/978-3-540-78969-7_13","volume-title":"Functional and Logic Programming, Proceedings, volume 4989 of LNCS","author":"J. Voigtl\u00e4nder","year":"2008","unstructured":"Voigtl\u00e4nder J.: Semantics and pragmatics of new shortcut fusion rules. In: Garrigue, J., Hermenegildo, M. (eds) Functional and Logic Programming, Proceedings, volume 4989 of LNCS, pp. 163\u2013179. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78969-7_13"},{"key":"136_CR35","first-page":"165","volume-title":"Principles of Programming Languages, Proceedings, volume 44(1) of ACM SIGPLAN Not.","author":"J. Voigtl\u00e4nder","year":"2009","unstructured":"Voigtl\u00e4nder J.: Bidirectionalization for free!. In: Pierce, B. (ed.) Principles of Programming Languages, Proceedings, volume 44(1) of ACM SIGPLAN Not., pp. 165\u2013176. ACM, New York (2009). doi: 10.1145\/1594834.1480904"},{"key":"136_CR36","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1145\/1596550.1596577","volume-title":"International Conference on Functional Programming, Proceedings, volume 44(9) of ACM SIGPLAN Not.","author":"J. Voigtl\u00e4nder","year":"2009","unstructured":"Voigtl\u00e4nder J.: Free theorems involving type constructor classes. In: Tolmach, A. (ed.) International Conference on Functional Programming, Proceedings, volume 44(9) of ACM SIGPLAN Not., pp. 173\u2013184. ACM, New York (2009). doi: 10.1145\/1631687.1596577"},{"key":"136_CR37","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1145\/1863543.1863571","volume-title":"International Conference on Functional Programming, Proceedings, volume 45(9) of ACM SIGPLAN Not.","author":"J. Voigtl\u00e4nder","year":"2010","unstructured":"Voigtl\u00e4nder J., Hu Z., Matsuda K., Wang M.: Combining syntactic and semantic bidirectionalization. In: Weirich, S. (ed.) International Conference on Functional Programming, Proceedings, volume 45(9) of ACM SIGPLAN Not., pp. 181\u2013192. ACM, New York (2010). doi: 10.1145\/1932681.1863571"},{"key":"136_CR38","first-page":"347","volume-title":"Functional Programming Languages and Computer Architecture, Proceedings","author":"P. Wadler","year":"1989","unstructured":"Wadler P.: Theorems for free!. In: MacQueen, D. (ed.) Functional Programming Languages and Computer Architecture, Proceedings, pp. 347\u2013359. ACM, New York (1989). doi: 10.1145\/99370.99404"},{"key":"136_CR39","doi-asserted-by":"crossref","unstructured":"Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: Principles of Programming Languages, Proceedings, pp. 60\u201376. ACM, New York (1989). doi: 10.1145\/75277.75283","DOI":"10.1145\/75277.75283"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-011-0136-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-011-0136-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-011-0136-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,5]],"date-time":"2025-03-05T02:55:08Z","timestamp":1741143308000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-011-0136-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,4,16]]},"references-count":39,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2011,5]]}},"alternative-id":["136"],"URL":"https:\/\/doi.org\/10.1007\/s00236-011-0136-9","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2011,4,16]]}}}