|
[Date Prev] [Date Next] [Thread Prev] [Thread Next] [Date Index] [Thread Index]
Hmm, something about this doesn't sound "gut feel"-ish, but then
again, I'm not in the sales and marketing department.
On Dec 1, 10:48 am, Michael Greenberg <michael.m.greenb...@gmail.com>
wrote:
> On Tue, Dec 1, 2009 at 7:57 AM, pezman <mikehoga...@gmail.com> wrote:
> > @MG -- I was wondering if there is any material under development that
> > goes deeper into TAPL stuff or other PL topics that might be of
> > general interest? I'd love to get the gut feel for the more advanced
> > topics in TAPL (System F, F-omega etc.) and topics in intensional type
> > systems etc. etc. It might be fun to beta-test some stuff like that
> > (otoh, we might be unqualified test subjects).
>
> The POPL tutorial (http://www.cis.upenn.edu/~plclub/popl08-tutorial/)
> covers Fsub. (The approach to variables taken in our book is
> inadequate for System F and beyond---locally nameless is the way to
> go.)
>
> Developing soundness proofs for more complicated calculi in Coq is
> called, by some, "research". Have a look at recent work by Jianzhou
> Zhao and Steve Zdancewic (more Penn PL!) for some interesting
> examples.
>
> Cheers,
> Michael
|
|