{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,31]],"date-time":"2022-12-31T22:25:58Z","timestamp":1672525558300},"reference-count":33,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.45.3","type":"journal-article","created":{"date-parts":[[2011,1,21]],"date-time":"2011-01-21T00:50:17Z","timestamp":1295571017000},"page":"31-44","source":"Crossref","is-referenced-by-count":4,"title":["Sound and Complete Typing for lambda-mu"],"prefix":"10.4204","volume":"45","author":[{"given":"Steffen","family":"van Bakel","sequence":"first","affiliation":[{"name":"Imperial College London"}]}],"member":"2720","published-online":{"date-parts":[[2011,1,22]]},"reference":[{"key":"Ariola-Herbelin'03","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"871","DOI":"10.1007\/3-540-45061-0_68","article-title":"Minimal Classical Logic and Control Operators","volume-title":"Proceedings of Automata, Languages and Programming, 30th International Colloquium, ICALP'03, 2003","volume":"2719","author":"Z.M. Ariola","year":"2003"},{"issue":"1","key":"Bakel-TCS'92","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0304-3975(92)90297-S","article-title":"Complete restrictions of the Intersection Type Discipline","volume":"102","author":"S. van Bakel","year":"1992","journal-title":"Theoretical Computer Science"},{"key":"Bakel-APAL'10","doi-asserted-by":"crossref","first-page":"1400","DOI":"10.1016\/j.apal.2010.04.010","article-title":"Completeness and Partial Soundness Results for Intersection & Union Typing for `l`m\"767E\u03bc","volume":"161","author":"S. van Bakel","year":"2010","journal-title":"Annals of Pure and Applied Logic"},{"key":"Bakel-FI'10","volume-title":"Completeness and Soundness results for X with Intersection and Union Types","author":"S. van Bakel","year":"2010"},{"issue":"3","key":"Bakel-deLiguoro-TOCS'08","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1007\/s00224-007-9079-5","article-title":"Logical equivalence for subtyping object and recursive types","volume":"42","author":"S. van Bakel","year":"2008","journal-title":"Theory of Computing Systems"},{"issue":"133","key":"Bakel-Fernandez-IaC'97","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1006\/inco.1996.2617","article-title":"Normalization Results for Typeable Rewrite Systems","volume":"2","author":"S. van Bakel","year":"1997","journal-title":"Information and Computation"},{"key":"vBLL-ICTCS'05","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/11560586_8","article-title":"The language X: Circuits, Computations and Classical Logic","volume-title":"Proceedings of Ninth Italian Conference on Theoretical Computer Science (ICTCS'05)","volume":"3701","author":"S. van Bakel","year":"2005"},{"key":"Bakel-Lescanne-MSCS'08","doi-asserted-by":"crossref","first-page":"555","DOI":"10.1017\/S0960129508006762","article-title":"Computation with Classical Sequents","volume":"18","author":"S. van Bakel","year":"2008","journal-title":"Mathematical Structures in Computer Science"},{"key":"Barbanera-Dezani-Liguoro-IaC'95","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1006\/inco.1995.1086","article-title":"Intersection and Union Types: Syntax and Semantics","volume":"119(2)","author":"F. Barbanera","year":"1995","journal-title":"Information and Computation"},{"key":"Barendregt'84","volume-title":"The Lambda Calculus: its Syntax and Semantics","author":"H. Barendregt","year":"1984"},{"issue":"4","key":"BCD'83","doi-asserted-by":"crossref","first-page":"931","DOI":"10.2307\/2273659","article-title":"A filter lambda model and the completeness of type assignment","volume":"48","author":"H. Barendregt","year":"1983","journal-title":"Journal of Symbolic Logic"},{"issue":"1","key":"Church'36","doi-asserted-by":"crossref","first-page":"40","DOI":"10.2307\/2269326","article-title":"A Note on the Entscheidungsproblem","volume":"1","author":"A. Church","year":"1936","journal-title":"Journal of Symbolic Logic"},{"key":"Coppo-Dezani'78","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1007\/BF02011875","article-title":"A New Type Assignment for Lambda-Terms","volume":"19","author":"M. Coppo","year":"1978","journal-title":"Archive f\u00fcr Mathematischer Logic und Grundlagenforschung"},{"key":"Curien-Herbelin'00","series-title":"ACM Sigplan Notices","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/351240.351262","article-title":"The Duality of Computation","volume-title":"Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming (ICFP'00)","volume":"35.9","author":"P.-L. Curien","year":"2000"},{"key":"Curry-Feys'58","volume-title":"Combinatory Logic","volume":"1","author":"H.B. Curry","year":"1958"},{"issue":"4","key":"Davies-Pfenning'01","first-page":"511","article-title":"A judgmental reconstruction of modal logic","volume":"11","author":"R. Davies","year":"2001","journal-title":"Mathematical Structures in Computer Science"},{"key":"DGL-ITRS'04","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"228","article-title":"Intersection and Union Types in the `l`m\"767E\u03bc-calculus","volume-title":"Electronic Proceedings of 2nd International Workshop Intersection Types and Related Systems (ITRS'04)","volume":"136","author":"D. Dougherty","year":"2004"},{"key":"DGL-CDR'08","doi-asserted-by":"crossref","DOI":"10.1016\/j.tcs.2008.01.022","article-title":"Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage","volume":"398","author":"D. Dougherty","year":"2008","journal-title":"Theoretical Computer Science"},{"key":"Dunfield-Pfenning'03","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/3-540-36576-1_16","article-title":"Type Assignment for Intersections and Unions in Call-by-Value Languages","volume-title":"Proceedings of 6th International Conference on Foundations of Software Science and Computational Structures (FOSSACS'03)","author":"J. Dunfield","year":"2003"},{"key":"Gentzen'35","article-title":"Investigations into logical deduction","volume-title":"The Collected Papers of Gerhard Gentzen","author":"G. Gentzen","year":"1935"},{"key":"deGroote'94","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/3-540-58216-9_27","article-title":"On the relation between the \u03bb\u03bc-calculus and the syntactic theory of sequential control","volume-title":"Proceedings of 5th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'94)","volume":"822","author":"Ph. de Groote","year":"1994"},{"key":"Harper-Lillibridge'91","volume-title":"ML with callcc is unsound","author":"B. Harper","year":"1991"},{"key":"Herbelin'05","volume-title":"C'est maintenant qu'on calcule: au c\u0153ur de la dualit\u00e9","author":"H. Herbelin","year":"2005"},{"key":"Hindley'97","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511608865","volume-title":"Basic Simple Type Theory","author":"J.R. Hindley","year":"1997"},{"key":"Lengrand'03","series-title":"Electronic Notes in Theoretical Computer Science","article-title":"Call-by-value, call-by-name, and strong normalization for the classical sequent calculus","volume-title":"3rd Workshop on Reduction Strategies in Rewriting and Programming (WRS 2003)","volume":"86","author":"S. Lengrand","year":"2003"},{"key":"Maffeis'05","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/j.entcs.2005.06.012","article-title":"Sequence Types for the pi-calculus","volume":"136","author":"S. Maffeis","year":"2005","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"Milner-et.al'97","volume-title":"The Definition of Standard ML","author":"R. Milner","year":"1990"},{"key":"Ong-Stewart'97","first-page":"215","article-title":"A Curry-Howard foundation for functional computation with control","volume-title":"Proceedings of the 24th Annual ACM Symposium on Principles Of Programming Languages","author":"C.-H. L. Ong","year":"1997"},{"key":"Parigot'92","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1007\/BFb0013061","article-title":"An algorithmic interpretation of classical natural deduction","volume-title":"Proceedings of 3rd International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'92)","volume":"624","author":"M. Parigot","year":"1992"},{"key":"Parigot-Brno'93","first-page":"263","article-title":"Classical Proofs as Programs","volume-title":"Kurt G\u00f6del Colloquium","author":"M. Parigot","year":"1993"},{"key":"Parigot'93","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1109\/LICS.1993.287602","article-title":"Strong Normalization for Second Order Classical Natural Deduction","volume-title":"Proceedings of Eighth Annual IEEE Symposium on Logic in Computer Science, 19-23 June 1993","author":"M. Parigot","year":"1993"},{"key":"Pierce-PhD'91","volume-title":"Programming with Intersection Types and Bounded Polymorphism","author":"B.C. Pierce","year":"1991"},{"issue":"4","key":"Wright'95","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1007\/BF01018828","article-title":"Simple imperative polymorphism","volume":"8","author":"A.K. Wright","year":"1995","journal-title":"Lisp and Symbolic Computation"}],"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2017,6,19]],"date-time":"2017-06-19T14:42:33Z","timestamp":1497883353000},"score":1,"resource":{"primary":{"URL":"http:\/\/arxiv.org\/abs\/1101.4425v1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,1,22]]},"references-count":33,"URL":"https:\/\/doi.org\/10.4204\/eptcs.45.3","relation":{},"ISSN":["2075-2180"],"issn-type":[{"value":"2075-2180","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,1,22]]}}}