+1 Recommend
1 collections
      • Record: found
      • Abstract: found
      • Conference Proceedings: found
      Is Open Access

      Subject Reduction vs Intersection / Union Types in λμμ

      Visions of Computer Science - BCS International Academic Conference (VOCS)

      BCS International Academic Conference

      22 - 24 September 2008

      Read this article at

          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.


          The role of Classical Logic in computer science is changing drastically over the last few years. Given the direct relation between the Lambda Calculus (Barendregt 1984) and intuitionistic logic, for many years it was believed that only the constructive logics had any real computational content, and only after Griffi n’s discovery of the relation between double-negation elimination (Griffi n 1990) and Felleisen’s control operators (Felleisen, Friedman, Kohlbecker, and Duba 1987) did the research community become aware of the computational advantages of Classical Logic. Since then, many researchers have focussed on different calculi, trying to exploit the Curry-Howard isomorphism for various classical logics, both in sequent style and in natural deduction, for computer science: amongst many, we mention (Parigot 1992; Ong and Stewart 1997; Curien and Herbelin 2000; Urban 2000; Wadler 2003). In this paper we contribute to that line of research by studying the λμμ-calculus (Curien and Herbelin 2000), which enjoys a Curry-Howard isomorphism for implicative G 3 (Kleene 1952), an variant of Gentzen’s system LK (Gentzen 1935).

          Related collections

          Most cited references 2

          • Record: found
          • Abstract: not found
          • Article: not found

          A syntactic theory of sequential control

            • Record: found
            • Abstract: not found
            • Book Chapter: not found

            Strong Normalization of the Dual Classical Sequent Calculus


              Author and article information

              September 2008
              September 2008
              : 249-258
              Department of Computing, Imperial College London

              180 Queen’s Gate, London SW7 2BZ, UK
              © Steffen van Bakel. Published by BCS Learning and Development Ltd. Visions of Computer Science - BCS International Academic Conference

              This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

              Visions of Computer Science - BCS International Academic Conference
              Imperial College, London, UK
              22 - 24 September 2008
              Electronic Workshops in Computing (eWiC)
              BCS International Academic Conference
              Product Information: 1477-9358BCS Learning & Development
              Self URI (journal page): https://ewic.bcs.org/
              Electronic Workshops in Computing


              Comment on this article