Jumbo Lambda Calculus

Two new papers by Paul Blain Levy, "Jumbo Lambda Calculus" and the extended version "Jumbo Connectives in Type Theory and Logic", are available on his web page. Part of the 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.

(From the types list.)

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

First Link

I think you meant to point us here: http://www.cs.bham.ac.uk/~pbl/papers/.

Whoops...

Of course you're right... It's fixed now. Thanks!

Functions in jumbo lambda-calculus

Observation: the functions in jumbo lambda-calculus are similar to the case-lambda construct of Chez Scheme and PLT Scheme. That is, you've got a multi-way function that chooses a body according to some criterion. But instead of matching on arities, as in case-lambda, the choice is made via a tag passed as an argument.