[TYPES] decidability of BCCCs?

[Ryan Wisnesky]

Hello,

I am trying to find a reference that states whether or not the free bi-cartesian closed category is decidable.  That is, I am wondering if beta-eta equality of the simply typed lambda calculus extended with strong 0,1,+,* types is decidable.  (In particular, I am interested in the full calculus, including the eliminator for 0, introduction for 1, and eta for all types).

So far, my search through the literature says that the answer to this question is "almost" or "maybe" :

- the STLC with strong 1,+,* types is decidable (omits 0, the empty type): http://www.cs.nott.ac.uk/~txa/publ/lics01.pdf

- the STLC with strong 0,1,+,* types has normal forms, but equivalent terms may have different such normal forms:http://www.cl.cam.ac.uk/~mpf23/papers/Types/tdpe.pdf

- work on mechanized proofs of correctness for deciding co-product equality may or may not include the "absurd" eliminator for the empty type: http://www.cis.upenn.edu/~sweirich/wmm/wmm07/programme/licata.pdf

I feel like the answer to this question is probably well-known, but I can't seem to find it in the literature.  Any help would be appreciated.  

Thanks,
Ryan