{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T23:10:51Z","timestamp":1773097851992,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540626886","type":"print"},{"value":"9783540684381","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-62688-3_27","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:48:50Z","timestamp":1330278530000},"page":"30-45","source":"Crossref","is-referenced-by-count":4,"title":["Minimum information code in a pure functional language with data types"],"prefix":"10.1007","author":[{"given":"S.","family":"Berardi","sequence":"first","affiliation":[]},{"given":"L.","family":"Boerio","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"3_CR1","unstructured":"H. Barendregt, The Lambda Calculus its Syntax and Semantics, Studies in Logic and the Foundation of Mathematics, North-Holland, 1984"},{"key":"3_CR2","volume-title":"Ph. D. Thesis","author":"P. N. Benton","year":"1992","unstructured":"P. N. Benton, Strictness Analysis of Lazy Functional Programs, Ph. D. Thesis, University of Cambridge, Pembroke College, 1992, Cambridge."},{"key":"3_CR3","unstructured":"S. Berardi, Extensional Equality for Simply Typed \u03bb-calculi, Technical Report, Turin University, 1993 (available via ftp at ftp.di.unito.it)."},{"key":"3_CR4","unstructured":"S. Berardi, Pruning Simply Typed \u03bb-terms, to appear in Journal of Logic and Computation."},{"key":"3_CR5","series-title":"LNCS 902","first-page":"63","volume-title":"Proceedings of TLCA '95","author":"S. Berardi","year":"1995","unstructured":"S. Berardi, L. Boerio, Using Subtyping in Program Optimization, Proceedings of TLCA '95, Eds, M. Dezani and G. Plotkin, Edinburgh, April 1995, LNCS 902, pp. 63\u201377, Springer-Verlag."},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"S. Berardi, L. Boerio, Removing Redundant Code in a Pure Functional Language with Data Types, Technical Report, Turin University, 1996 (available via ftp at ftp.di.unito.it).","DOI":"10.1007\/3-540-62688-3_27"},{"key":"3_CR7","series-title":"LNCS 788","first-page":"120","volume-title":"Proceedings of ESOP '94","author":"L. Boerio","year":"1994","unstructured":"L. Boerio, Extending Pruning Techniques to Polymorphic Second Order \u03bb-Calculus, Proceedings of ESOP '94, Edinburgh, April 1994, LNCS 788, D. Sannella (ed.), Springer-Verlag, pp. 120\u2013134."},{"key":"3_CR8","volume-title":"Ph. D. Thesis in Computer Science","author":"L. Boerio","year":"1995","unstructured":"L. Boerio, Optimizing Programs Extracted from Proofs, Ph. D. Thesis in Computer Science, University of Turin, February 1995, Turin (available via ftp at ftp.di.unito.it)."},{"key":"3_CR9","volume-title":"Ph. D. Thesis","author":"J. Y. Girard","year":"1971","unstructured":"J. Y. Girard, Interpretation Fonctionelle et Elimination des Coupures dans l'Aritmetique d'Ordre Superieur, Ph. D. Thesis, Universit\u00e9 Paris VII, 1971, Paris."},{"key":"3_CR10","volume-title":"LNCS 78","author":"M. J. C. Gordon","year":"1979","unstructured":"M. J. C. Gordon, R. Milner, C. P. Wadsworth, Edinburgh LCF, LNCS 78, Springer-Verlag, 1979."},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"L.S. Hunt, D. Sands, Binding Time Analysis: A New PERspective, Proceedings of the ACM Symposium on Partial Evaluation and Semantics-based Program Manipulation, 1991.","DOI":"10.1145\/115865.115881"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"J. C. Mitchell, Type Systems for Programming Languages, In: J. van Leeuwen ed., Handbook of Theoretical Computer Science, Elsevier Science Publ., 1990, 366\u2013458.","DOI":"10.1016\/B978-0-444-88074-1.50013-5"},{"key":"3_CR13","first-page":"89","volume-title":"Extracting F\u03c9's, Programs from Proofs in the Calculus of Constructions","author":"C. Paulin-Mohring","year":"1989","unstructured":"C. Paulin-Mohring, Extracting F \u03c9's, Programs from Proofs in the Calculus of Constructions, In: Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, Association for Computing Machinery publisher, 11\u201313 January 1989, pp. 89\u2013104."},{"key":"3_CR14","unstructured":"J. C. Reynolds, Towards a Theory of Type Structure, in Colloque sur la Programmation, LNCS 19, Springer-Verlag, 1974."}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-62688-3_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:13:59Z","timestamp":1605629639000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-62688-3_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540626886","9783540684381"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-62688-3_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997]]}}}