The Coq mailing list

[Tadeusz Litak <tadeusz.litak AT gmail.com>]

Dear all,

I have a question about $SUBJECT$.

I have a hard time trying to find out whether there are some "canonical" Coq formalizations of, let's say, Parigot's 
\lambda\mu-calculus or related formalisms and their basic metatheory.

In particular, I always thought that formalization of, e.g, normalization proofs which go via the CPS route would make a 
nice student project. I have a student right now willing to spend some time on this. But I would like to avoid 
reinventing the wheel, and I had the suspicion that there may be more than a few formalization efforts already 
available. Still, casual search does not produce all that much. Such calculi do not seem covered, for example, by what I 
can find in the Iron Lambda repository. Am I missing some obvious references?


Best regards,
t.