753
views
0
recommends
+1 Recommend
1 collections
    0
    shares

      Celebrating 65 years of The Computer Journal - free-to-read perspectives - bcs.org/tcj65

      scite_
       
      • Record: found
      • Abstract: found
      • Conference Proceedings: found
      Is Open Access

      Subject Reduction vs Intersection / Union Types in λμμ

      proceedings-article
      Visions of Computer Science - BCS International Academic Conference (VOCS)
      BCS International Academic Conference
      22 - 24 September 2008
      Bookmark

            Abstract

            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).

            Content

            Author and article information

            Contributors
            Conference
            September 2008
            September 2008
            : 249-258
            Affiliations
            [0001]Department of Computing, Imperial College London

            180 Queen’s Gate, London SW7 2BZ, UK
            Article
            10.14236/ewic/VOCS2008.21
            7c4b7769-4e10-4810-9109-033d7a70ab1b
            © 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
            VOCS
            Imperial College, London, UK
            22 - 24 September 2008
            Electronic Workshops in Computing (eWiC)
            BCS International Academic Conference
            History
            Product

            1477-9358 BCS Learning & Development

            Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/VOCS2008.21
            Self URI (journal page): https://ewic.bcs.org/
            Categories
            Electronic Workshops in Computing

            Applied computer science,Computer science,Security & Cryptology,Graphics & Multimedia design,General computer science,Human-computer-interaction

            Comments

            Comment on this article