|
[Date Prev] [Date Next] [Thread Prev] [Thread Next] [Date Index] [Thread Index]
- From: Michael Greenberg <michael.m.greenberg@gmail.com>
- To: philly-lambda@googlegroups.com
- Subject: Re: Coq proof assistant
- Date: Tue, 1 Dec 2009 10:48:41 -0500
- Dkim-signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:x-beenthere:received:received:received :received:received:received-spf:received:mime-version:received :in-reply-to:references:date:message-id:subject:from:to:reply-to :precedence:mailing-list:list-id:list-post:list-help:list-archive :x-thread-url:x-message-url:list-unsubscribe:list-subscribe :content-type:content-transfer-encoding; bh=rfKw5nJZFTmMhjoABAgkCpdEaojYQ3CW7JD2Gf0J+8s=; b=MxWyLH5skVtKVkyOAxG+FsHpo1Px7T7zlpA1vlx+rCGyhypLJMJy+2sMLpM3lRyAOB L9D5oxeV2fpL2g7THiKedlp3FFwRdYLNpVoCAsnOBwclzRX75dXyET3e59jaBbJa3TFc MAZzdhGSosjEz/1RQvS2HdU4H9uP7z7cwf7W8=
- List-archive: <http://groups.google.com/group/philly-lambda?hl=>
- Mailing-list: list philly-lambda@googlegroups.com; contact philly-lambda+owners@googlegroups.com
- Reply-to: philly-lambda@googlegroups.com
On Tue, Dec 1, 2009 at 7:57 AM, pezman <mikehogan62@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
|
|