Sequent calculus and ANF

[Frank Pfenning]

Hi Dan,

  as mentioned in the conclusion of Ohori's paper, it does not tell the
whole story.  There is also a connection between A-normal form, Moggi's
monadic meta-language, and lax logic.  This goes back to work by
[Benton, Biermann, and de Paiva'98], [Kobayashi'97] and, of
course, [Moggi'88,'89,'91].  You can read about that in:

Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal
logic. Mathematical Structures in Computer Science, 11:511-540,
2001. http://www.cs.cmu.edu/~fp/papers/mscs00.pdf

  - Frank

> Ahh thanks to Matthias Blume for point me to the work by Ohori
> 
> Atsushi Ohori. A Curry-Howard isomorphism for compilation and program 
> execution. Proc. TLCA Conference, Springer LNCS 1581, 258-179, April 1999.
> 
>    http://www.jaist.ac.jp/~ohori/research/anormal.pdf