{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T22:35:44Z","timestamp":1693866944828},"reference-count":49,"publisher":"Elsevier BV","issue":"1-3","license":[{"start":{"date-parts":[[2007,12,1]],"date-time":"2007-12-01T00:00:00Z","timestamp":1196467200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":2055,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2007,12]]},"DOI":"10.1016\/j.tcs.2007.09.014","type":"journal-article","created":{"date-parts":[[2007,9,22]],"date-time":"2007-09-22T11:23:31Z","timestamp":1190460211000},"page":"290-318","source":"Crossref","is-referenced-by-count":10,"title":["Selective strictness and parametricity in structural operational semantics, inequationally"],"prefix":"10.1016","volume":"388","author":[{"given":"Janis","family":"Voigtl\u00e4nder","sequence":"first","affiliation":[]},{"given":"Patricia","family":"Johann","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.tcs.2007.09.014_b1","series-title":"Haskell Workshop, Proceedings","first-page":"62","article-title":"Verifying Haskell programs using constructive type theory","author":"Abel","year":"2005"},{"key":"10.1016\/j.tcs.2007.09.014_b2","series-title":"European Symposium on Programming, Proceedings","first-page":"69","article-title":"Step-indexed syntactic logical relations for recursive and quantified types","volume":"vol. 3924","author":"Ahmed","year":"2006"},{"key":"10.1016\/j.tcs.2007.09.014_b3_1","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/0304-3975(90)90151-7","article-title":"Functorial polymorphism","volume":"70","author":"Bainbridge","year":"1990","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/j.tcs.2007.09.014_b3_2","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1016\/0304-3975(90)90055-M","article-title":"Functorial polymorphism","volume":"71","author":"Bainbridge","year":"1990","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/j.tcs.2007.09.014_b4","series-title":"Mathematical Foundations of Programming Semantics 2005, Proceedings","first-page":"191","article-title":"Parametric domain-theoretic models of polymorphic intuitionistic\/linear lambda calculus","volume":"vol. 155","author":"Birkedal","year":"2006"},{"key":"10.1016\/j.tcs.2007.09.014_b5","unstructured":"Clean Language Report 2.0. http:\/\/www.cs.ru.nl\/~clean\/CleanExtra\/report20\/index.html"},{"key":"10.1016\/j.tcs.2007.09.014_b6","series-title":"Principles of Programming Languages, Proceedings","first-page":"206","article-title":"Fast and loose reasoning is morally correct","author":"Danielsson","year":"2006"},{"key":"10.1016\/j.tcs.2007.09.014_b7","series-title":"Mathematics of Program Construction, Proceedings","first-page":"85","article-title":"Chasing bottoms \u2014 A case study in program verification in the presence of partial and infinite values","volume":"vol. 3125","author":"Danielsson","year":"2004"},{"key":"10.1016\/j.tcs.2007.09.014_b8","series-title":"Implementation and Application of Functional Languages 2005, Selected Papers","first-page":"37","article-title":"Proof tool support for explicit strictness","volume":"vol. 4015","author":"van Eekelen","year":"2006"},{"key":"10.1016\/j.tcs.2007.09.014_b9","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1016\/0304-3975(87)90109-5","article-title":"A syntactic theory of sequential control","volume":"52","author":"Felleisen","year":"1987","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/j.tcs.2007.09.014_b10","series-title":"Logic Colloquium \u201972\u201373, Proceedings","first-page":"22","article-title":"Equality between functionals","author":"Friedman","year":"1975"},{"key":"10.1016\/j.tcs.2007.09.014_b11","unstructured":"The Glasgow Haskell Compiler. http:\/\/www.haskell.org\/ghc"},{"key":"10.1016\/j.tcs.2007.09.014_b12","unstructured":"J.-Y. Girard, Interpr\u00e9tation functionelle et \u00e9limination des coupures dans l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieure, Ph.D. Thesis, Universit\u00e9 Paris VII, 1972"},{"key":"10.1016\/j.tcs.2007.09.014_b13","series-title":"International Conference on Functional Programming, Proceedings","first-page":"294","article-title":"Monadic augment and generalised short cut fusion","author":"Ghani","year":"2005"},{"key":"10.1016\/j.tcs.2007.09.014_b14","series-title":"Functional Programming Languages and Computer Architecture, Proceedings","first-page":"223","article-title":"A short cut to deforestation","author":"Gill","year":"1993"},{"key":"10.1016\/j.tcs.2007.09.014_b15","series-title":"Theoretical Aspects of Computer Software, Proceedings","first-page":"495","article-title":"Parametricity of extensionally collapsed term models of polymorphism and their categorical properties","volume":"vol. 526","author":"Hasegawa","year":"1991"},{"key":"10.1016\/j.tcs.2007.09.014_b16","doi-asserted-by":"crossref","first-page":"837","DOI":"10.1017\/S0956796805005666","article-title":"The logic of demand in Haskell","volume":"15","author":"Harrison","year":"2005","journal-title":"Journal of Functional Programming"},{"key":"10.1016\/j.tcs.2007.09.014_b17","unstructured":"The Haskell Mailing List Archive. http:\/\/www.mail-arch ive.com\/haskell@haskell.org"},{"key":"10.1016\/j.tcs.2007.09.014_b18","unstructured":"R. Harper, C. Stone, An interpretation of Standard ML in type theory, Technical Report CMU-CS-97-147, Carnegie Mellon University, 1997"},{"key":"10.1016\/j.tcs.2007.09.014_b19","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1023\/A:1022982420888","article-title":"A generalization of short-cut fusion and its correctness proof","volume":"15","author":"Johann","year":"2002","journal-title":"Higher-order and Symbolic Computation"},{"key":"10.1016\/j.tcs.2007.09.014_b20","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1017\/S0956796802004409","article-title":"Short cut fusion is correct","volume":"13","author":"Johann","year":"2003","journal-title":"Journal of Functional Programming"},{"key":"10.1016\/j.tcs.2007.09.014_b21","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1017\/S0960129504004578","article-title":"On proving the correctness of program transformations based on free theorems for higher-order polymorphic calculi","volume":"15","author":"Johann","year":"2005","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.1016\/j.tcs.2007.09.014_b22","series-title":"Principles of Programming Languages, Proceedings","first-page":"99","article-title":"Free theorems in the presence of seq","author":"Johann","year":"2004"},{"key":"10.1016\/j.tcs.2007.09.014_b23","first-page":"63","article-title":"The impact of seq on free theorems-based program transformations","volume":"69","author":"Johann","year":"2006","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/j.tcs.2007.09.014_b24","doi-asserted-by":"crossref","unstructured":"S.B. Lassen, Relational reasoning about functions and nondeterminism, Ph.D. Thesis, University of Aarhus, 1998","DOI":"10.7146\/brics.v4i24.18950"},{"key":"10.1016\/j.tcs.2007.09.014_b25","series-title":"Principles of Programming Languages, Proceedings","first-page":"88","article-title":"Polymorphic type inference","author":"Leivant","year":"1983"},{"key":"10.1016\/j.tcs.2007.09.014_b26","series-title":"European Symposium on Programming, Proceedings","first-page":"204","article-title":"Parametricity and unboxing with unpointed types","author":"Launchbury","year":"1996"},{"key":"10.1016\/j.tcs.2007.09.014_b27","series-title":"International Colloquium on Automata, Languages and Programming, Proceedings","first-page":"372","article-title":"Interpreting polymorphic FPC into domain theoretic models of parametric polymorphism","volume":"vol. 4052","author":"M\u00f8gelberg","year":"2006"},{"key":"10.1016\/j.tcs.2007.09.014_b28","doi-asserted-by":"crossref","first-page":"470","DOI":"10.1145\/44501.45065","article-title":"Abstract types have existential type","volume":"10","author":"Mitchell","year":"1988","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/j.tcs.2007.09.014_b29","series-title":"Haskell 98 Language and Libraries: The Revised Report","year":"2003"},{"key":"10.1016\/j.tcs.2007.09.014_b30","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1017\/S0960129500003066","article-title":"Parametric polymorphism and operational equivalence","volume":"10","author":"Pitts","year":"2000","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.1016\/j.tcs.2007.09.014_b31","series-title":"Advanced Topics in Types and Programming Languages","first-page":"245","article-title":"Typed operational reasoning","author":"Pitts","year":"2005"},{"key":"10.1016\/j.tcs.2007.09.014_b32","unstructured":"G.D. Plotkin, Lambda-definability and logical relations, Memorandum SAI-RM-4, University of Edinburgh, 1973"},{"key":"10.1016\/j.tcs.2007.09.014_b33","first-page":"17","article-title":"A structural approach to operational semantics","volume":"60\u201361","author":"Plotkin","year":"2004","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"10.1016\/j.tcs.2007.09.014_b34","series-title":"Principles of Programming Languages, Proceedings","first-page":"49","article-title":"Bridging the gulf: A common intermediate language for ML and Haskell","author":"Peyton Jones","year":"1998"},{"key":"10.1016\/j.tcs.2007.09.014_b35","series-title":"Colloque sur la Programmation, Proceedings","first-page":"408","article-title":"Towards a theory of type structure","author":"Reynolds","year":"1974"},{"key":"10.1016\/j.tcs.2007.09.014_b36","series-title":"Information Processing, Proceedings","first-page":"513","article-title":"Types, abstraction and parametric polymorphism","author":"Reynolds","year":"1983"},{"key":"10.1016\/j.tcs.2007.09.014_b37","series-title":"European Symposium on Programming, Proceedings","first-page":"38","article-title":"Haskell is not not ML","volume":"vol. 3924","author":"Rudiak-Gould","year":"2006"},{"key":"10.1016\/j.tcs.2007.09.014_b38","series-title":"Logic in Computer Science, Proceedings","first-page":"364","article-title":"Reflexive graphs and parametric polymorphism","author":"Robinson","year":"1994"},{"key":"10.1016\/j.tcs.2007.09.014_b39","unstructured":"G. Rosolini, A. Simpson, Using synthetic domain theory to prove operational properties of a polymorphic programming language based on strictness 2004 (manuscript)"},{"key":"10.1016\/j.tcs.2007.09.014_b40","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/S0019-9958(85)80001-2","article-title":"Logical relations and the typed lambda-calculus","volume":"65","author":"Statman","year":"1985","journal-title":"Information and Control"},{"key":"10.1016\/j.tcs.2007.09.014_b41","series-title":"International Conference on Functional Programming, Proceedings","first-page":"124","article-title":"Shortcut fusion for accumulating parameters & zip-like functions","author":"Svenningsson","year":"2002"},{"key":"10.1016\/j.tcs.2007.09.014_b42","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1017\/S0956796897002967","article-title":"Algorithm + Strategy = Parallelism","volume":"8","author":"Trinder","year":"1998","journal-title":"Journal of Functional Programming"},{"key":"10.1016\/j.tcs.2007.09.014_b43","series-title":"Functional Programming Languages and Computer Architecture, Proceedings","first-page":"306","article-title":"Shortcut deforestation in calculational form","author":"Takano","year":"1995"},{"key":"10.1016\/j.tcs.2007.09.014_b44","unstructured":"J. Voigtl\u00e4nder, P. Johann, Selective strictness and parametricity in structural operational semantics, Technical Report TUD-FI06-02, Technische Universit\u00e4t Dresden, 2006"},{"key":"10.1016\/j.tcs.2007.09.014_b45","series-title":"International Conference on Functional Programming, Proceedings","first-page":"14","article-title":"Concatenate, reverse and map vanish for free","author":"Voigtl\u00e4nder","year":"2002"},{"key":"10.1016\/j.tcs.2007.09.014_b46","series-title":"International Conference on Functional Programming, Proceedings","first-page":"251","article-title":"Boxy types: Inference for higher-rank types and impredicativity","author":"Vytiniotis","year":"2006"},{"key":"10.1016\/j.tcs.2007.09.014_b47","series-title":"Functional Programming Languages and Computer Architecture, Proceedings","first-page":"347","article-title":"Theorems for free!","author":"Wadler","year":"1989"},{"key":"10.1016\/j.tcs.2007.09.014_b48","series-title":"Principles of Programming Languages, Proceedings","first-page":"60","article-title":"How to make ad-hoc polymorphism less ad hoc","author":"Wadler","year":"1989"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397507006871?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397507006871?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T06:58:34Z","timestamp":1556866714000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397507006871"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,12]]},"references-count":49,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2007,12]]}},"alternative-id":["S0304397507006871"],"URL":"https:\/\/doi.org\/10.1016\/j.tcs.2007.09.014","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2007,12]]}}}