Steffen van Bakel's list of publications
List of Publications of Steffen van Bakel Department of Computing Imperial College London 2021 2020 Recent Work 2019 2018 2017 2016 2015 2014 2013 2012 2011 2010 2009 2008 2007 2006 2005 2004 2003 2002 2001 2000 1999 1998 1997 1996 1995 1994 1993 1992 My Google Scholar profile, Scopus profile, entry in DBLP, Research Gate profile, and Imperial College page. Other sites to meet lots of nice and interesting people are Researchers in Rewriting, and Researchers in Intersection Types and Related Systems (maintained by Joe Wells). Recent Work. D. Davies, S. van Bakel, and N. Wu. Candid: A Dependently Typed Programming Language with Control Operators for Classical Logic. S. van Bakel. Exception Handling with and without Classical Logic. S. van Bakel and M.G. Vigliotti. A fully-abstract output-based semantics of λμ in the π-calculus. 2019 (C) 42% S. van Bakel. Exception Handling and Classical Logic. In: Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming, Porto, Portugal, October 7-9, 2019. ACM New York, NY, USA, article 21. A full version with all proofs can be found here. 2018 (J) 0.855 S. van Bakel. Characterisation of Normalisation Properties for λμ using Strict Negated Intersection Types. ACM Transactions on Computational Logic, Volume 19(1): 3:1-3:47, February 2018 (Article No. 3). (J) 0.569 S. van Bakel, F. Barbanera, U. de'Liguoro. Intersection Types for the λμ-Calculus. Logical Methods in Computer Science 14(1) (2018). 2017 (J) 0.636 F. Barbanera, S. van Bakel, U. de'Liguoro. Orchestrated Session Compliance. Journal of Logical and Algebraic Methods in Programming, 86(1): 30-76 (2017) 2016 (W) S. van Bakel. Characterisation of Approximation and (Head) Normalisation for λμ using Strict Intersection Types. 8th International Workshop on Intersection Types and Related Systems (ITRS'16). EPTCS volume 242, 2016. Ulrich Kohlenbach, Steffen van Bakel, Stefano Berardi Proceedings Sixth International Workshop on Classical Logic and Computation (CL&C 2016), Porto, Portugal, 23th June 2016. EPTCS 213, 2016. 2015 (W) F. Barbanera, S. van Bakel, U. de'Liguoro. Orchestrated compliance for session-based client/server interactions. Proceedings of 8th Interaction and Concurrency Experience (ICE 2015), June 5, 2015, Grenoble, France, EPTCS 189, pp. 21-36. (U) S. van Bakel, L. Cardelli and M.G. Vigliotti. Classical Cut-elimination in the π-calculus. 2014 (B) S. van Bakel and M.G. Vigliotti. Classical π. In M. Abadi, P. Gardner, A.D. Gordon, and R. Mardare, editors, Essays for the Luca Cardelli Fest, number MSR-TR-2014-104. Microsoft Research, September 2014. (W) S. van Bakel and M.G. Vigliotti. A fully-abstract semantics of λμ in the π-calculus. In: Fifth International Workshop on Classical Logic and Computation (CL&C'14), Vienna, Austria, July 2014. EPTCS volume 164, pp 33-47, 2014. (J) 0.697 R.N.S. Rowe and S.J. van Bakel. Semantic Types and Approximation for Featherweight Java. Theoretical Computer Science, 517:34-74, 2014. (U) S. van Bakel and M.G. Vigliotti. An Implicative Logic based encoding of the λ-calculus into the π-calculus. 2013 (B) S.J. van Bakel and R.N.S. Rowe. Functional Type Assignment for Featherweight Java. In: The Beauty of Functional Code, Essays Dedicated to Rinus Plasmeijer on the Occasion of His 61st Birthday. Volume 8106 of Lecture Notes in Computer Science, pages 27-46, Springer-Verlag, 2013. (W) S. van Bakel, F. Barbanera, U. de'Liguoro. Characterisation of Strongly Normalising λμ-Terms. In: 6th International Workshop on Intersection Types and Related Systems (ITRS'12), Dubrovnik, Croatia, June 29th, 2012. EPTCS volume 121, pp 1-17, 2013. (J) 0.646 S. van Bakel, S. Berardi, and U. Berger. Classical Logic and Computation (CLAC 2010) - Preface. Annals of Pure and Applied Logic 164: 589-590, 2013 2012 (J) 0.522 S. van Bakel. Completeness and Soundness results for X with Intersection and Union Types. Fundamenta Informaticae, 121:1-41, 2012. DOI:10.3233/FI-2012-770. (A version with more examples and more detailed proofs can be found here.) (C) 48% S. van Bakel and M.G. Vigliotti. An Output-Based Semantics of Λμ with Explicit Substitution in the π-calculus - Extended Abstract. In: Theoretical Computer Science - 7th IFIP TC 1/WG 2.2 International Conference, TCS 2012, 26-28 September 2012, Amsterdam, The Netherlands. Volume 7604 of Lecture Notes in Computer Science, pages 372--387. Springer-Verlag, 2012. (U) S. van Bakel and J. Raghunandan. An optimised term graph rewriting engine for X - Measuring the cost of α-conversion. 2011 (W) S. van Bakel, F. Barbanera, U. de'Liguoro. A Domain Logic Approach to Models of λμ and Related Calculi. In: Domains X Workshop 2011, Deptartment of Computer Science, Swansea, Wales, UK, 5 - 7 September 2011. (C) 34% R.N.S. Rowe and S. van Bakel. Approximation Semantics and Expressive Predicate Assignment for Object-Oriented Programming. In: Proceedings of 10th International Conference on Typed Lambda Calculi and Applications (TLCA'11), Novi Sad, Serbia, June 1-3, 2011. Volume 6690 of Lecture Notes in Computer Science, pages 229-244, Springer-Verlag, 2011. (C) 34% S. van Bakel, F. Barbanera, U. de'Liguoro. A Filter Model for the λμ-Calculus - (Extended Abstract). In: Proceedings of 10th International Conference on Typed Lambda Calculi and Applications (TLCA'11), Novi Sad, Serbia, June 1-3, 2011. Volume 6690 of Lecture Notes in Computer Science, pages 213-228, Springer-Verlag, 2011. (J) 7.806 S. van Bakel. Strict Intersection Types for the Lambda Calculus. ACM Computing Surveys, 43(3) article 20, April 2011. (U) S. van Bakel and M.G. Vigliotti. An output-based semantics of λ in π. 2010 (W) S. van Bakel, S. Berardi, and U. Berger. Proceedings Third International Workshop on Classical Logic and Computation CL&C 2010. EPTCS 47, 2010. (W) S. van Bakel. Sound and Complete Typing for λμ. In: 5th International Workshop on Intersection Types and Related Systems (ITRS'10), Edinburgh, Scotland, July 2010. EPTCS volume 45, pp 31-44. (J) 0.646 S. van Bakel, S. Berardi, and U. Berger. Classical Logic and Computation (2008) - Preface. Annals of Pure and Applied Logic 161: 1313-1314, 2010. (J) 0.646 S. van Bakel. Completeness and partial soundness results for intersection and union typing for Lambdabar-mu-mutilde. Annals of Pure and Applied Logic 161, pp 1400-1430, 2010. Steffen van Bakel, Stefano Berardi, Ulrich Berger Proceedings Third International Workshop on Classical Logic and Computation (CL&C 2010), Brno, Czech Republic, 21-22 August, 2010. 2009 (C) 29% S. van Bakel and M.G. Vigliotti. A logical interpretation of the λ-calculus into the π-calculus, preserving spine reduction and types. In: 20th International Conference on Concurrency Theory (CONCUR'09), Bologna, Italy, September 2009. Volume 5710 of Lecture Notes in Computer Science, pages 84-98. Springer-Verlag, 2009. (W) S. van Bakel and R. Rowe. Semantic Predicate Types and Approximation for Class-based Object Oriented Programming. In: 11th Workshop on Formal Techniques for Java-like Programs (FTfJP'09), Genova, Italy, July 6 2009. 2008 (J) 0.646 S. van Bakel and S. Berardi. Classical Logic and Computation (2006) - Preface. Annals of Pure and Applied Logic 153: 1-3, 2008. (J) 0.474 S. van Bakel and P. Lescanne. Computation with classical sequents. Mathematical Structures in Computer Science, 18:555-609, 2008 (J) 0.838 S. van Bakel. The Heart of Intersection Type Assignment - Normalisation proofs revisited. Theoretical Computer Science, 398(1-3):82-94, 2008. (J) 0.600 S. van Bakel and U. de'Liguoro. Logical equivalence for subtyping and recursive types. Theory of Computing Systems, 42(3):306-348, 2008. (C) 43% S. van Bakel. Subject Reduction vs Intersection / Union Types for lambda-bar-mu-mu-tilde (Extended abstract). In: Visions of Computer Science, BCS International Academic Conference, London, pages 249-258, 2008. (W) S. van Bakel, L. Cardelli and M.G. Vigliotti. From X to π: Representing Classical Sequent Calculus in Pi-calculus. In: International Workshop on Classical Logic and Computation (CL&C'08), Reykjavik, Iceland, July 2008. (W) S. van Bakel. Reduction in X does not agree with Intersection and Union Types. In: 4th International Workshop on Intersection Types and Related Systems (ITRS'08), Turin, Italy, March 2008. (W) S. van Bakel, I. Kahn, M.G. Vigliotti, and J.K. Heath. Modelling intracellular fate of FGF receptors with BioAmbients. In: Sixth Workshop on Quantitative Aspects of Programming Languages (QAPL'08), Budapest, Hungary, March 2008. ENTCS 220, pp. 181-197. 2007 (W) 75% S. van Bakel and M.G. Vigliotti. Note on a simple type system for non-interference. In: Nordic Workshop on Programming Theory (NWPT'07), Oslo, October 10-12, 2007. (B) S. van Bakel. Classical Sequents and Computation: an overview. In: Reflections on Type Theory, Lambda Calculus, and the Mind, Essays Dedicated to Henk Barendregt on the Occasion of his 60th Birthday. Radboud University, 2007. 2006 (C) 24% A. Summers and S. van Bakel. Approaches to Polymorphism in Classical Sequent Calculus. In: Programming Languages and Systems: Proceedings of 15th European Symposium on Programming (ESOP'06), Vienna, Austria. Volume 3924 of Lecture Notes in Computer Science, pages 84-99. Springer-Verlag, 2006. (U) P. Audebaud and S. van Bakel. Understanding X with λμ. (Full version), 2006. (W) S. van Bakel and J. Raghunandan. Explicit Alpha Conversion and Garbage Collection for X. International Workshop on Term Graph Rewriting (TermGraph'06), Vienna, Austria, March 2006. 2005 (C) 35% S. van Bakel, S. Lengrand and P. Lescanne. The language X: Circuits, Computations and Classical Logic. Proceedings of Ninth Italian Conference on Theoretical Computer Science (ICTCS'05), Siena, Italy, Volume 3701 of Lecture Notes in Computer Science, pages 81-96, 2005. (C) 35% S. van Bakel and U. de'Liguoro. Subtyping object and recursive types logically (Extended Abstract). Proceedings of Ninth Italian Conference on Theoretical Computer Science (ICTCS'05), Siena, Italy, Volume 3701 of Lecture Notes in Computer Science, pages 66-80, 2005. (U) S. van Bakel. Rank 2 Types for Term Graph Rewriting. 2005. (U) S. van Bakel, J. Raghunandan, and A. Summers. Term Graphs, Alpha Conversion and Principal Types for X, 2005. 2004 (J) 0.825 S. Lengrand, P. Lescanne, D. Dougherty, M. Dezani-Ciancaglini and S. van Bakel. Intersection types for explicit substitutions. Information and Computation, 189(1):17-42, 2004. (J) S. van Bakel. Cut-Elimination in the Strict Intersection Type Assignment System is Strongly Normalising. Notre Dame Journal of Formal Logic, Volume 45, Number 1, 2004. (W) S. van Bakel and J. Raghunandan. Implementing X. International Workshop on Term Graph Rewriting (TermGraph'04), Rome, Italy, October 2004; ENTCS, volume 127(5). (W) S. van Bakel. Intersection and Union Types for X. 3rd International Workshop on Intersection Types and Related Systems (ITRS'04), Turku, Finland, July 2004; ENTCS, volume 136. 2003 (J) 0.838 S. van Bakel and M. Fernández. Normalization, Approximation, and Semantics for Combinator Systems. Theoretical Computer Science, 290:975-1019, 2003. (C) 42% S. van Bakel and U. de'Liguoro. Logical Semantics for the First Order Varsigma Calculus. Proceedings of Eighth Italian Conference on Theoretical Computer Science (ICTCS'03), Bertinoro, Italy, Volume 2841 of Lecture Notes in Computer Science, pages 202-215, 2003. 2002 (J) 0.838 S. van Bakel, F. Barbanera, M. Dezani-Ciancaglini, and F.J. de Vries. Intersection Types for λ-Trees. Theoretical Computer Science, 272 (Theories of Types and Proofs 1997):3-40, 2002. (C) ?% C. Braghin, A. Cortesi, R. Focardi, and S. van Bakel. Boundary Inference for Enforcing Security Policies in Mobile Ambients. Proceedings of 2nd IFIP International Conference on Theoretical Computer Science (TCS'02), Montreal, Canada, pages 383-395, 2002. (W) S. van Bakel. Preface. 2nd International Workshop on Intersection Types and Related Systems (ITRS'02), Copenhagen, Denmark, July 2002; ENTCS, volume 70.1. (W) S. van Bakel. Strongly Normalising Cut-Elimination with Strict Intersection Types. 2nd International Workshop on Intersection Types and Related Systems (ITRS'02), Copenhagen, Denmark, July 2002; ENTCS, volume 70.1. (W) S. van Bakel. Rank 2 Type Assignment for Applicative Term Graph Rewriting. Workshop Types in Programming (TIP'02), Dagstuhl, Germany, July 2002; ENTCS, Volume 75. (C) 43% S. van Bakel, M. Dezani-Ciancaglini. Characterising Strong Normalisation for Explicit Substitutions. Proceedings of LATIN'02, Cancun, Mexico, Volume 2286 of Lecture Notes in Computer Science, pages 356-370, Springer-Verlag, 2002. 2001 (U) S. van Bakel, F. Barbanera, and M. Fernández. Polymorphic Intersection Type Assignment for Rewrite Systems with Abstraction and β-rule. Technical Report 2001/01, Department of Computer Science, Imperial College London. 2000 (C) ?% S. van Bakel, F. Barbanera, and M. Fernández. Polymorphic Intersection Type Assignment for Rewrite Systems with Abstraction and β-rule. In: Types for Proofs and Programs. International Workshop, TYPES'99. Lokeberg, Sweden, Sected Papers. Volume 1956 of Lecture Notes in Computer Science, pages 41-60, Springer-Verlag, 2000. (U) S. van Bakel, M. Dezani-Ciancaglini, U. de'Liguoro, Y. Motohama. The Minimal Relevant Logic and the Call-by-Value Lambda Calculus. 2000. Technical report TR-ARP-05-2000, Australian National University. 1997 (J) 0.646 S. van Bakel, L. Liquori, R. Ronchi della Rocca, and P. Urzyczyn. Comparing Cubes of Typed and Type Assignment Systems. Annals of Pure and Applied Logic, 86(3):267-303, 1997. (J) 0.825 S. van Bakel and M. Fernández. Normalization Results for Typeable Rewrite Systems. Information and Computation, 133(2):73-116, 1997. 1996 (U) S. van Bakel, F Barbanera and M. Fernández. Normalisation and Approximation results for typeable Term Rewriting Systems (with abstraction and β-rule) - Summary. (J) 0.522 S. van Bakel. Rank 2 Intersection Type Assignment in Term Rewriting Systems. Fundamenta Informaticae, 26(2):141-166, 1996. (C) 36% S. van Bakel, F. Barbanera, and M. Fernández. Rewrite Systems with Abstraction and β-rule: Types, Approximants and Normalization. In: Programming Languages and Systems - Proceedings of 6th European Symposium on Programming (ESOP'96), Linkoping, Sweden. Volume 1058 of Lecture Notes in Computer Science, pages 387-403. Springer-Verlag, 1996. (C) 58% S. van Bakel and M. Fernández. Approximation and Normalization Results for Typeable Term Rewriting Systems. In: Second International Workshop on Higher Order Algebra, Logic and Term Rewriting (HOA'95), Paderborn, Germany. Selected Papers. Volume 1074 of Lecture Notes in Computer Science, pages 17-36. Springer-Verlag, 1996. 1995 (J) 0.838 S. van Bakel. Intersection Type Assignment Systems. Theoretical Computer Science, 151(2):385-435, 1995. (C) 32% S. van Bakel and M. Fernández. (Head-)Normalization of Typeable Rewrite Systems. In: 6th International Conference on Rewriting Techniques and Applications (RTA'95), Kaiserslautern, Germany. Volume 914 of Lecture Notes in Computer Science, pages 279-293. Springer-Verlag, 1995. 1994 (C) ?% S. van Bakel, L. Liquori, R. Ronchi della Rocca, and P. Urzyczyn. Comparing Cubes. In: Third International Symposium on Logical Foundations of Computer Science (LFCS'94), St. Petersburg, Russia. Volume 813 of Lecture Notes in Computer Science, pages 353-365. Springer-Verlag, 1994. (C) 48% S. van Bakel and M. Fernández. Strong Normalization of Typeable Rewrite Systems. In: First International Workshop on Higher Order Algebra, Logic and Term Rewriting (HOA'93), Amsterdam, the Netherlands. Selected Papers. Volume 816 of Lecture Notes in Computer Science, pages 20-39. Springer-Verlag, 1994. 1993 (PhD) S. van Bakel. Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems. Department of Computer Science, University of Nijmegen, 1993. (J) 0.789 S. van Bakel. Principal type schemes for the Strict Type Assignment System. Journal of Logic and Computation, 3(6):643-670, 1993. (C) 28% S. van Bakel. Essential Intersection Type Assignment. In: 13th Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS'93), Bombay, India. Volume 761 of Lecture Notes in Computer Science, pages 13-23, Springer-Verlag, 1993. (C) 57% S. van Bakel. Partial Intersection Type Assignment in Applicative Term Rewriting Systems. In: International Conference on Typed Lambda Calculi and Applications (TLCA'93), Utrecht, the Netherlands. Volume 664 of Lecture Notes in Computer Science, pages 29-44, Springer-Verlag, 1993. (B) S. van Bakel, S. Smetsers, and S. Brock. Partial Type Assignment in Left Linear Applicative Term Rewriting Systems. In: Term Graph Rewriting. Theory and Practice, pages 15-30. Wiley, 1993. (B) S. van Bakel. Partiële Typetoekenning in Linkslineaire applicatieve Termherschrijfsystemen. In: Zin dat het heeft; een liber amicorum voor Jan van Bakel, pages 35-54. Coppen, 1993. (B) S. van Bakel. Chapter Six: Type assignment systems. In Rinus Plasmeijer, Marko van Eekelen, Functional Programming and Parallel Graph Rewriting. Addison-Wesley, 1993. 1992 (J) 0.838 S. van Bakel. Complete restrictions of the Intersection Type Discipline. Theoretical Computer Science, 102:135-163, 1992. A version of this paper with a corrected proof for the property "All strongly normalisable terms are typeable" can be found here. (C) 45% S. van Bakel, S. Smetsers, and S. Brock. Partial Type Assignment in Left Linear Applicative Term Rewriting Systems. In: 17th Colloquim on Trees in Algebra and Programming (CAAP'92), Rennes, France. Volume 581 of Lecture Notes in Computer Science, pages 300-321, Springer-Verlag, 1992. I had a bit of time on my hands, so decided to try something out: I scanned in an old paper (Pottinger's 1980 paper "A Type Assignment for the Strongly Normalizable λ-terms" that appeared in "To H. B. Curry, Essays in Combinatory Logic, Lambda-Calculus and Formalism" and is rather famous for being the first in stating that you can characterise strong normalisation using intersection types); you can find the scanned document here. I then converted that to text, and moved it to latex (only changing some notation, the content is unchanged), the result of which you can find here. (Last updated: May 14, 2019).
