lillibridge, strong termination, exceptions

Subject: lillibridge, strong termination, exceptions
From: Johan Ovlinger (
Date: Mon Feb 04 2002 - 23:49:48 EST

It's all Matthias's fault (betcha never heard that before)!

Anyway, He mentioned Mark Lillibridge, whose Thesis I read many moons
ago (and was very jealous). So on a lark I checked out his homepage at
dig^h^h^h compaq SRC (birthplace of Modula-3, coincidentally (?)).

The following abstract (from his pubs) is pertinent to our discussion
about strong normalisation this afternoon:

  More precisely, we prove that a natural extension of the
  simply-typed lambda calculus with unchecked exceptions is strictly
  more powerful than all known sound extensions of Girard's F-omega (a
  superset of the simply-typed lambda calculus) with call/cc.

  This result is established by showing that the first language is
  Turing complete while the later languages permit only a subset of
  the recursive functions to be written.

This suprised me. Adding exceptions to the STLC makes it turing
complete! If only I didn't have a thesis proposal to write...

This archive was generated by hypermail 2b28 : Mon Feb 04 2002 - 23:49:50 EST