[TYPES/announce] jumbo lambda-calculus

[Paul B Levy]

---------- Forwarded message ----------
Date: Thu, 11 May 2006 12:23:19 +0100 (BST)
From: Paul B Levy <pbl at acws-0092.cs.bham.ac.uk>
To: types-announce at list.seas.upenn.edu
Subject: jumbo lambda-calculus


Dear all,

A manuscript "Jumbo connectives in type theory and logic" is available on 
my webpage

http://www.cs.bham.ac.uk/~pbl/papers/

The first part (on jumbo lambda-calculus) is being presented at ICALP in 
July.

Comments are very welcome.

Abstract
--------

We make an argument that, for any study involving computational effects 
such as divergence or continuations, the traditional syntax of simply 
typed lambda-calculus cannot be regarded as canonical, because standard 
arguments for canonicity rely on isomorphisms that may not exist in an 
effectful setting.  To remedy this, we define a ``jumbo lambda-calculus'' 
that fuses the traditional connectives together into more general ones, 
so-called ``jumbo connectives''.  We provide two pieces of evidence for 
our thesis that the jumbo formulation is advantageous.

Firstly, we show that the jumbo lambda-calculus provides a ``complete'' 
range of connectives, in the sense of including every possible connective 
that, within the beta-eta theory, possesses a reversible rule.   

Secondly, in the presence of effects, we see that there is no 
decomposition of jumbo connectives into non-jumbo ones that is valid in 
both call-by-value and call-by-name.

Finally, we apply the concept of jumbo connectives to systems with 
isorecursive types (Jumbo FPC) and multiple conclusions (Jumbo LK).

At each stage, we see that various connectives proposed in the literature 
are special cases of the jumbo connectives.