Subject Reduction vs Intersection / Union Types in λμμ

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 ₃ (Kleene 1952), an variant of Gentzen’s system LK (Gentzen 1935).

Contributors

Steffen van Bakel

Conference

Publication date: September 2008

Publication date (Print): September 2008

Pages: 249-258

Affiliations

Department of Computing, Imperial College London

180 Queen’s Gate, London SW7 2BZ, UK

Article

DOI: 10.14236/ewic/VOCS2008.21

Copyright statement: © Steffen van Bakel. Published by BCS Learning and Development Ltd. Visions of Computer Science - BCS International Academic Conference

License:

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/

Conference name: Visions of Computer Science - BCS International Academic Conference

Conference acronym: VOCS

Conference number:

Conference location: Imperial College, London, UK

Conference date: 22 - 24 September 2008

Conference sponsor: Electronic Workshops in Computing (eWiC)

Conference theme: BCS International Academic Conference

Product

Product Information: 1477-9358BCS 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

Series title: Electronic Workshops in Computing