From vkoutav at ccs.neu.edu  Mon Oct  3 12:44:36 2011
From: vkoutav at ccs.neu.edu (Vasileios Koutavas)
Date: Mon, 3 Oct 2011 17:44:36 +0100
Subject: [PRL] cartoon about racket
Message-ID: <3B9DA41F-8D2C-49DD-8475-C7D0642084CA@ccs.neu.edu>

I could not resist sending this:

http://chzsomuchpun.files.wordpress.com/2011/08/fa5faef0-1c0c-41ba-aea0-2fc995f9bafe.jpg

--Vassilis




From dvanhorn at ccs.neu.edu  Thu Oct 13 16:11:29 2011
From: dvanhorn at ccs.neu.edu (David Van Horn)
Date: Thu, 13 Oct 2011 16:11:29 -0400
Subject: [PRL] Fwd: Re: [Programming] PL Seminar Next Week -- Jesse Tov
Message-ID: <4E9745F1.10709@ccs.neu.edu>

[ Harvard PL seminar are Wednesdays at 4pm. -- David ]

-------- Original Message --------
Subject: Re: [Programming] PL Seminar Next Week -- Jesse Tov
Date: Thu, 13 Oct 2011 13:47:24 -0400
From: Jesse A. Tov <tov at eecs.harvard.edu>
To: Programming at eecs.harvard.edu

Thanks to Gregory for the announcement.

I should add that because this is a practice conference talk, it will
be only 20 minutes. It won't be very polished, because I'm hoping to
improve it based on whatever feedback those in attendance can supply.
Any negative comments you can muster will be greatly appreciated.

Cheers,
Jesse

On Thu, Oct 13, 2011 at 12:08, Gregory Malecha
<gmalecha at eecs.harvard.edu> wrote:
> Jesse Tov will be talking at next week's programming language seminar. MD
> 323 @ 4:00pm
> A Theory of Substructural Types and Control
> Jesse A. Tov and Riccardo Pucella
> Exceptions are invaluable for structured error handling in high-level
> languages, but they are at odds with linear types. More generally,
> control effects may delete or duplicate portions of the stack, which,
> if we are not careful, can invalidate all substructural usage
> guarantees for values on the stack. We have developed a
> type-and-effect system that tracks control effects and ensures that
> values on the stack are never wrongly duplicated or dropped. We
> present the system first with abstract control effects and prove its
> soundness. We then give examples of three instantiations with
> particular control effects, including exceptions and delimited
> continuations, and show that they meet the soundness criteria for
> specific control effects.
> --
> gregory malecha
> http://www.people.fas.harvard.edu/~gmalecha/
>
> _______________________________________________
> Programming mailing list
> Programming at eecs.harvard.edu
> https://lists.eecs.harvard.edu/mailman/listinfo/programming
>
>
_______________________________________________
Programming mailing list
Programming at eecs.harvard.edu
https://lists.eecs.harvard.edu/mailman/listinfo/programming


From mwand1 at gmail.com  Fri Oct 14 10:59:03 2011
From: mwand1 at gmail.com (Mitch)
Date: Fri, 14 Oct 2011 14:59:03 +0000
Subject: [PRL] Certifying and reasoning on cost annotations of functional
	programs. (arXiv:...
Message-ID: <bcaec5215c877ce5b004af437f18@google.com>

Possibly of interest to somebody here. (Evaluation based on abstract
only).

Sent to you by Mitch via Google Reader: Certifying and reasoning on
cost annotations of functional programs. (arXiv:1110.2350v1 [cs.PL])
via cs.PL updates on arXiv.org by <a
href="http://arxiv.org/find/cs/1/au:+Amadio_R/0/1/0/all/0/1">Roberto M.
Amadio</a> (PPS), <a
href="http://arxiv.org/find/cs/1/au:+Regis_Gianas_Y/0/1/0/all/0/1">Yann
Regis-Gianas</a> (PPS, INRIA Paris - Rocquencourt) on 10/11/11

We present a so-called labelling method to insert cost annotations in a
higher-order functional program, to certify their correctness with
respect to a standard compilation chain to assembly code, and to reason
on them in a higher-order Hoare logic.

Things you can do from here:
- Subscribe to cs.PL updates on arXiv.org using Google Reader
- Get started using Google Reader to easily keep up with all your
favorite sites
-------------- next part --------------
HTML attachment scrubbed and removed

From tov at ccs.neu.edu  Sun Oct 16 18:58:30 2011
From: tov at ccs.neu.edu (Jesse A. Tov)
Date: Sun, 16 Oct 2011 18:58:30 -0400
Subject: [PRL] Fwd: Re: [Programming] PL Seminar Next Week -- Jesse Tov
In-Reply-To: <4E9745F1.10709@ccs.neu.edu>
References: <4E9745F1.10709@ccs.neu.edu>
Message-ID: <CABQ65r0dw7BMyPoPor5nAVLBtb5+3cNPiWs-RcTD-yz3-FmHsA@mail.gmail.com>

If anyone wants to come on Wednesday, I'll have room for four in my
car from NU to Harvard and back. I'm planning to leave at 3:15 and
we'll be back in time for the 6 PM meeting. Let me know if you'd like
a seat.

Cheers,
Jesse

On Thu, Oct 13, 2011 at 16:11, David Van Horn <dvanhorn at ccs.neu.edu> wrote:
> [ Harvard PL seminar are Wednesdays at 4pm. -- David ]
>
> -------- Original Message --------
> Subject: Re: [Programming] PL Seminar Next Week -- Jesse Tov
> Date: Thu, 13 Oct 2011 13:47:24 -0400
> From: Jesse A. Tov <tov at eecs.harvard.edu>
> To: Programming at eecs.harvard.edu
>
> Thanks to Gregory for the announcement.
>
> I should add that because this is a practice conference talk, it will
> be only 20 minutes. It won't be very polished, because I'm hoping to
> improve it based on whatever feedback those in attendance can supply.
> Any negative comments you can muster will be greatly appreciated.
>
> Cheers,
> Jesse
>
> On Thu, Oct 13, 2011 at 12:08, Gregory Malecha
> <gmalecha at eecs.harvard.edu> wrote:
>> Jesse Tov will be talking at next week's programming language seminar. MD
>> 323 @ 4:00pm
>> A Theory of Substructural Types and Control
>> Jesse A. Tov and Riccardo Pucella
>> Exceptions are invaluable for structured error handling in high-level
>> languages, but they are at odds with linear types. More generally,
>> control effects may delete or duplicate portions of the stack, which,
>> if we are not careful, can invalidate all substructural usage
>> guarantees for values on the stack. We have developed a
>> type-and-effect system that tracks control effects and ensures that
>> values on the stack are never wrongly duplicated or dropped. We
>> present the system first with abstract control effects and prove its
>> soundness. We then give examples of three instantiations with
>> particular control effects, including exceptions and delimited
>> continuations, and show that they meet the soundness criteria for
>> specific control effects.
>> --
>> gregory malecha
>> http://www.people.fas.harvard.edu/~gmalecha/
>>
>> _______________________________________________
>> Programming mailing list
>> Programming at eecs.harvard.edu
>> https://lists.eecs.harvard.edu/mailman/listinfo/programming
>>
>>
> _______________________________________________
> Programming mailing list
> Programming at eecs.harvard.edu
> https://lists.eecs.harvard.edu/mailman/listinfo/programming
>
> _______________________________________________
> PRL mailing list
> PRL at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/prl
>


From pete at ccs.neu.edu  Wed Oct 12 14:24:49 2011
From: pete at ccs.neu.edu (Pete Manolios)
Date: Wed, 12 Oct 2011 18:24:49 -0000
Subject: [PRL] Job opening at AFRL
Message-ID: <CADQ5nuzzoN4xQK7bDNFZ+JKhhTfX5y=jRiJ_vNpsf79CxaE_fw@mail.gmail.com>

There is a position available at AFRL for a Verification and
Validation Engineer.

The position will be located onsite at Wright-Patterson AFB, Dayton, Ohio.

If interested, here's how to get more information:

http://www.linquest.com/ -> Careers -> Job Openings -> Verification
and Validation Engineer (#1285)

-- 
Pete Manolios
Northeastern University
http://www.ccs.neu.edu/home/pete


From turon at ccs.neu.edu  Thu Oct 20 10:30:07 2011
From: turon at ccs.neu.edu (Aaron Turon)
Date: Thu, 20 Oct 2011 10:30:07 -0400
Subject: [PRL] Torture chamber tomorrow, 10/21, 1:30 WVH366
Message-ID: <CAGfQ5avc6oCT8SH9j2iCUj1zCNpOcrOgnvbAWoEW=w8VGncVCA@mail.gmail.com>

I'll be giving a practice OOPSLA talk tomorrow (Friday, 10/21) in
WVH366 at 1:30.  The talk length is 20 minutes.  Please come torture
me!

--

Scalable Join Patterns
(with Claudio Russo)

Coordination can destroy scalability in parallel programming. A
comprehensive library of synchronization primitives is therefore an
essential tool for exploiting parallelism. Unfortunately, such
primitives do not easily combine to yield scalable solutions to more
complex problems. We demonstrate that a concurrency library based on
Fournet and Gonthier's join calculus can provide declarative and
scalable coordination. By declarative, we mean that the programmer
needs only to write down the constraints of a coordination problem,
and the library will automatically derive a correct solution. By
scalable, we mean that the derived solutions deliver robust
performance both as the number of processors increases, and as the
complexity of the coordination problem grows. We validate our claims
empirically on seven coordination problems, comparing our generic
solution to specialized algorithms from the literature.


From wand at ccs.neu.edu  Mon Oct 24 19:26:20 2011
From: wand at ccs.neu.edu (Mitchell Wand)
Date: Mon, 24 Oct 2011 19:26:20 -0400
Subject: [PRL] Fwd: JMC R.I.P.
In-Reply-To: <4EA5D48C.60101@cs.stanford.edu>
References: <4EA5D48C.60101@cs.stanford.edu>
Message-ID: <CAJqwn-_ka0GQ--PUEp9EEE-GMvA9AEbmzQjaX3jTTGEehYw1CQ@mail.gmail.com>

---------- Forwarded message ----------
From: Les Earnest <les at cs.stanford.edu>
Date: Mon, Oct 24, 2011 at 5:11 PM
Subject: JMC R.I.P.
To:


I just learned that John McCarthy passed away in his sleep last night. I
understand that no funeral is planned but expect there will be a celebration
of his life sometime in the future.

   -Les Earnest
-------------- next part --------------
HTML attachment scrubbed and removed

From eli at barzilay.org  Tue Oct 25 16:51:22 2011
From: eli at barzilay.org (Eli Barzilay)
Date: Tue, 25 Oct 2011 16:51:22 -0400
Subject: [PRL] PL class
Message-ID: <CALO-gutgMUhp1gCuPK-r2Ehg8=GztCyM8P56dthBWcAx52L_OA@mail.gmail.com>

Is there anyone around who can do my PL class tomorrow?  (Stephen got
held up by the law...)  The subject is lazy evaluation.

-- 
          ((lambda (x) (x x)) (lambda (x) (x x)))          Eli Barzilay:
                  http://www.barzilay.org/                 Maze is Life!


From eli at barzilay.org  Tue Oct 25 22:20:34 2011
From: eli at barzilay.org (Eli Barzilay)
Date: Tue, 25 Oct 2011 22:20:34 -0400
Subject: [PRL] PL class
In-Reply-To: <CALO-gutgMUhp1gCuPK-r2Ehg8=GztCyM8P56dthBWcAx52L_OA@mail.gmail.com>
References: <CALO-gutgMUhp1gCuPK-r2Ehg8=GztCyM8P56dthBWcAx52L_OA@mail.gmail.com>
Message-ID: <CALO-gusu9b54R_Xs+-AqoVim237_qYrh3dVcRpHz5r7RaHL+_w@mail.gmail.com>

Anyone??

On Tuesday, October 25, 2011, Eli Barzilay <eli at barzilay.org> wrote:
> Is there anyone around who can do my PL class tomorrow?  (Stephen got
> held up by the law...)  The subject is lazy evaluation.
>
> --
>          ((lambda (x) (x x)) (lambda (x) (x x)))          Eli Barzilay:
>                  http://www.barzilay.org/                 Maze is Life!

-- 
          ((lambda (x) (x x)) (lambda (x) (x x)))          Eli Barzilay:
                  http://www.barzilay.org/                 Maze is Life!
-------------- next part --------------
HTML attachment scrubbed and removed

From cce at ccs.neu.edu  Mon Oct 31 20:44:01 2011
From: cce at ccs.neu.edu (Carl Eastlund)
Date: Mon, 31 Oct 2011 20:44:01 -0400
Subject: [PRL] Torture chamber this Wed. (11/2) at 10am
Message-ID: <CAEOPtY1Y86TKUL6e4TjERCdJFBqnfEPzT8UBFhkhP=DVoZ6YTA@mail.gmail.com>

I'll be practicing my 15-minute talk entitled "Dracula Reborn:
ML-style Modules, Racket Macros, and the ACL2 Theorem Prover", which I
will present at the ACL2 Workshop in Austin on Thursday.  The talk is
in room 366.

Carl Eastlund


From turon at ccs.neu.edu  Tue Nov  1 09:26:14 2011
From: turon at ccs.neu.edu (Aaron Turon)
Date: Tue, 1 Nov 2011 09:26:14 -0400
Subject: [PRL] SPLASH recap
Message-ID: <CAGfQ5ataZ6oEusaziG4h89Zb8eYUzkkuVfaQ7Xe0w-DNsDmCCw@mail.gmail.com>

On Wednesday at 11:45am, we'll hold a recap of the SPLASH
conferences/workshops in WVH366 (using the standard seminar slot).

Please join us for a discussion of the most memorable talks and events!


From cce at ccs.neu.edu  Tue Nov  1 18:52:39 2011
From: cce at ccs.neu.edu (Carl Eastlund)
Date: Tue, 1 Nov 2011 18:52:39 -0400
Subject: [PRL] CANCELLED: Torture chamber this Wed. (11/2) at 10am
Message-ID: <CAEOPtY2xArTb81JuvYNG6oOvBJGypC5Fdi8yS2BUgVR_PVYVYw@mail.gmail.com>

Much as I would like the feedback, my presentation isn't going to be
ready for a dress rehearsal in the morning.  Rather than waste
anyone's time on a half-baked dry-run, I will continue to work on my
own.

Carl Eastlund

On Mon, Oct 31, 2011 at 8:44 PM, Carl Eastlund <cce at ccs.neu.edu> wrote:
> I'll be practicing my 15-minute talk entitled "Dracula Reborn:
> ML-style Modules, Racket Macros, and the ACL2 Theorem Prover", which I
> will present at the ACL2 Workshop in Austin on Thursday. ?The talk is
> in room 366.
>
> Carl Eastlund


From matthias at ccs.neu.edu  Wed Nov  2 11:39:57 2011
From: matthias at ccs.neu.edu (Matthias Felleisen)
Date: Wed, 2 Nov 2011 11:39:57 -0400
Subject: [PRL] mark jones -- early warning
Message-ID: <FA4DF18F-BE30-491E-A8BA-A89694912971@ccs.neu.edu>


Next week we have Mark Jones (PSU) visiting. Due to an unfortunate mixup with the Darpa meeting, he will speak on THURSDAY. He can meet with people on WEDNESDAY and THURSDAY. Vincent is his host and responsible for the actual scheduling. He'll be in touch -- Matthias




From stamourv at ccs.neu.edu  Wed Nov  2 16:15:47 2011
From: stamourv at ccs.neu.edu (Vincent St-Amour)
Date: Wed, 02 Nov 2011 16:15:47 -0400
Subject: [PRL] Mark Jones's Visit
Message-ID: <8762j2e0wc.wl%stamourv@ccs.neu.edu>

As Matthias announced, Mark Jones will be visiting next week.

There are still meeting slots available on Wednesday, both before and
after lunch. If you're interested, please send me a list of times that
work for you.

Lunch on Thursday (after the talk) will be open to everyone.

If you have any questions, or are unsure, please ask me.

Vincent


From stamourv at ccs.neu.edu  Mon Nov  7 12:04:31 2011
From: stamourv at ccs.neu.edu (Vincent St-Amour)
Date: Mon, 07 Nov 2011 12:04:31 -0500
Subject: [PRL] Mark Jones's Schedule
Message-ID: <874nyfdfts.wl%stamourv@ccs.neu.edu>

Mark Jones will be visiting Wednesday and Thursday. Here's his meeting
schedule.

Please let me know if it doesn't work for you.

Vincent


Wednesday
10:00 - 11:00 : Breakfast
11:00 - 11:30 : Paul Stansifer
11:30 - 12:00 : Aaron Turon
12:00 - 12:30 : Christos Dimoulas
12:30 - 13:30 : Lunch
13:30 - 14:30 : Amal Ahmed and Jamie Perconti
14:30 - 15:30 : Jesse Tov
15:30 - 16:00 : Ian Johnson
16:00 - 16:30 : Stephen Chang
16:30 - 17:00 : Stevie Strickland
17:00 - 17:30 : Asumu Takikawa
17:30 - 18:00 : Dan King
18:00 - 18:30 : Carl Eastlund
19:00         : Dinner


Thursday
10:00 - 11:00 : Breakfast
11:00 - 12:30 : Talk
12:30 - 13:30 : Lunch (open to everyone)
13:30 - 14:00 : Olin Shivers
14:00 - 14:30 : Sam Tobin-Hochstadt
14:30 - 14:45 : Tony Garnock-Jones


From stamourv at ccs.neu.edu  Mon Nov  7 15:31:08 2011
From: stamourv at ccs.neu.edu (Vincent St-Amour)
Date: Mon, 07 Nov 2011 15:31:08 -0500
Subject: [PRL] Mark Jones's Schedule
In-Reply-To: <874nyfdfts.wl%stamourv@ccs.neu.edu>
References: <874nyfdfts.wl%stamourv@ccs.neu.edu>
Message-ID: <871utjd69f.wl%stamourv@ccs.neu.edu>

Here's a a revised schedule with more information about meals.

Vincent


Wednesday
10:00 - 11:00 : Breakfast
                (Vincent St-Amour, at the Colonnade)
11:00 - 11:30 : Paul Stansifer
11:30 - 12:00 : Aaron Turon
12:00 - 12:30 : Christos Dimoulas
12:30 - 13:30 : Lunch
                (Amal Ahmed, Carl Eastlund and Vincent St-Amour, at
		Betty's)
13:30 - 14:30 : Amal Ahmed and Jamie Perconti
14:30 - 15:30 : Jesse Tov
15:30 - 16:00 : Ian Johnson
16:00 - 16:30 : Stephen Chang
16:30 - 17:00 : Stevie Strickland
17:00 - 17:30 : Asumu Takikawa
17:30 - 18:00 : Dan King
18:00 - 18:30 : Carl Eastlund
19:00         : Dinner
                (Matthias Felleisen, Christos Dimoulas and Vincent
		St-Amour, at the Colonnade)

Thursday
9:30  - 11:00 : Breakfast
                (Sam Tobin-Hochstadt and Vincent St-Amour, at the
		Colonnade)
11:00 - 12:30 : Talk
12:30 - 13:30 : Lunch
                (open to everyone, at ph? and I)
13:30 - 14:00 : Olin Shivers
14:00 - 14:30 : Sam Tobin-Hochstadt
14:30 - 14:45 : Tony Garnock-Jones


From chrdimo at ccs.neu.edu  Wed Nov  9 10:29:51 2011
From: chrdimo at ccs.neu.edu (Christos Dimoulas)
Date: Wed, 09 Nov 2011 10:29:51 -0500
Subject: [PRL]  Grigore Rosu's Visit
Message-ID: <4EBA9C6F.8000900@ccs.neu.edu>

Hi everyone,

Grigore Rosu(http://fsl.cs.uiuc.edu/~grosu/) will be visiting next 
Wednesday.

If you're interested in a meeting with him, please send me a list of 
times that work for you. He will be at the department from 10:30 to 19:00.

Thanks.

.Christos


From matthias at ccs.neu.edu  Wed Nov  9 16:31:25 2011
From: matthias at ccs.neu.edu (Matthias Felleisen)
Date: Wed, 9 Nov 2011 16:31:25 -0500
Subject: [PRL] Fwd: [EAPLS] Faculty position(s) in programming languages
References: <20111109212401.11660.14104@svsoc4.win.tue.nl>
Message-ID: <0AA69129-A0B8-4084-8E1B-EB7BC634E0C8@ccs.neu.edu>



Begin forwarded message:

> From: eapls-noreply at eapls.org
> Date: November 9, 2011 4:24:01 PM EST
> To: matthias at ccs.neu.edu
> Subject: [EAPLS] Faculty position(s) in programming languages
> 
> 
> Faculty position(s) in programming languages
> 
> by Martin Erwig on November 9 |  View on site |  Share
> The School of EECS at Oregon State University has four openings for tenure track faculty. Researchers from the programming language community are specifically encouraged to apply.
> 
> Assistant/Associate/Full Professor tenure-track position in Computer Science 
> 
> The School of Electrical Engineering and Computer Science at Oregon State
> University invites applications for up to four tenure-track positions in
> Computer Science. We seek strong candidates with a commitment to quality
> teaching and with research strengths in the areas of programming languages,
> algorithms with a focus on optimization or probabilistic reasoning,
> systems-focused HCI, databases with a focus on very large data systems
> (excluding data mining), and computer security and privacy. Exceptionally
> strong candidates in other areas of computer science will also be considered.
> Applicants should demonstrate a strong commitment to collaboration with other
> research groups in the School of EECS, with other departments at Oregon State,
> and with other universities.
> 
> The School of EECS supports a culture of energetic collaboration, and the
> faculty are committed to excellence in both education and research. With 40
> tenure/tenure-track faculty, we enroll 185 Ph.D., 125 MS and 1200
> undergraduate students. OSU is recognized for its "very high research
> activity" by the Carnegie Foundation for the Advancement of Teaching. The
> School of EECS is housed in the Kelley Engineering Center, a green building
> designed to support collaboration among faculty and students across campus. 
> Corvallis is a college town renowned for its high quality of life.
> 
> For Full Consideration Date: 02-16-2012
> Closing Date: 06-30-2012
> 
> jobs.oregonstate.edu/applicants/Central?quickFind=59535
> 
> This message was sent by the EAPLS because you are a member. For more information about the EAPLS, visit our website.
> 
> To edit your EAPLS mailing list preferences please go to your profile.
> 

-------------- next part --------------
HTML attachment scrubbed and removed
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Mail Attachment.jpeg
Type: image/jpeg
Size: 8239 bytes
Desc: not available
Url : http://lists.ccs.neu.edu/pipermail/prl/attachments/20111109/e04cfd2a/attachment.jpeg 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Mail Attachment.png
Type: image/png
Size: 944 bytes
Desc: not available
Url : http://lists.ccs.neu.edu/pipermail/prl/attachments/20111109/e04cfd2a/attachment.png 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Mail Attachment.png
Type: image/png
Size: 940 bytes
Desc: not available
Url : http://lists.ccs.neu.edu/pipermail/prl/attachments/20111109/e04cfd2a/attachment-0001.png 

From chrdimo at ccs.neu.edu  Thu Nov 10 13:01:33 2011
From: chrdimo at ccs.neu.edu (Christos Dimoulas)
Date: Thu, 10 Nov 2011 13:01:33 -0500
Subject: [PRL] Grigore Rosu's visit -- early announcement
Message-ID: <4EBC117D.8040606@ccs.neu.edu>


Next week we have Grigore Rosu (UIUC) visiting.

Grigore will spend next Wednesday (November 16) at our lab. There are 
still some open slots for meetings. Let me know if you are interested.

Here is the info of the talk and a short bio of the speaker:

NEU Programming Languages Seminar presents

Grigore Rosu
Formal Systems Laboratory (FSL)
Department of Computer Science
University of Illinois at Urbana-Champaign

Wednesday, 11/16

11:45am - 1:30pm
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)


Title: K and Matching Logic

Abstract:: Would you like to wake up some morning, have a coffee, then 
design a non-trivial programming language, say with multidimensional 
arrays and array references, with functions and references to them, with 
blocks and local declarations, with input/output, with exceptions, with 
nondeterminism and concurrency with synchronization, and so on, and by 
evening to have a reasonably efficient interpreter, a state-space search 
tool and a model checker, as well as a deductive program verifier for 
your language, all correct-by-construction? Then you may be interested 
in K and Matching Logic, because that is what they are aiming for. K is 
a rewrite-based framework for defining formal operational semantics of 
programming languages. A K semantics can be executed, and thus tested, 
as if it was an interpreter for the defined language. This way, we can 
gain confidence in the correctness of our semantics. Then we can use 
precisely that semantics, unchanged, for program analysis and 
verification, without a need to give the language another, e.g., 
axiomatic or denotational or dynamic, semantics. Matching logic consists 
of a language-independent proof system that allows us to reason about 
programs in any language that is given a rewrite-based operational 
semantics.

Bio: Grigore Rosu is an associate professor in the Department of 
Computer Science at the University of Illinois at Urbana-Champaign 
(UIUC), where he leads the Formal Systems Laboratory (FSL). His research 
interests encompass both theoretical foundations and system development 
in the areas of formal methods, software engineering and programming 
languages. Before joining UIUC in 2002, he was a research scientist at 
NASA Ames. He obtained his Ph.D. at the University of California at San 
Diego in 2000 and his M.S. at the University of Bucharest, Romania, in 
1996. He was offered the CAREER award by the NSF and the outstanding 
junior award by the Computer Science Department at UIUC in 2005. He won 
an ACM SIGSOFT distinguished paper award at ASE 2008 and the best 
software science paper award at ETAPS 2002. He was ranked a UIUC 
excellent teacher in Spring 2008 and Fall 2004.



_______________________________________________
PRL mailing list
PRL at lists.ccs.neu.edu
https://lists.ccs.neu.edu/bin/listinfo/prl


From matthias at ccs.neu.edu  Thu Nov 10 13:25:50 2011
From: matthias at ccs.neu.edu (Matthias Felleisen)
Date: Thu, 10 Nov 2011 13:25:50 -0500
Subject: [PRL] Fwd: Programming Languages Mentoring Workshop (PLMW 2012)
References: <FAE21107-B743-4537-BBFA-C66464537447@cis.upenn.edu>
Message-ID: <F96FDF96-DCB1-44E8-98E1-CB55FBC54D97@ccs.neu.edu>



Begin forwarded message:

> From: Stephanie Weirich <sweirich at cis.upenn.edu>
> Date: November 10, 2011 1:21:01 PM EST
> To: Matthias Felleisen <matthias at ccs.neu.edu>
> Cc: Ronald Garcia <rxg at cs.ubc.ca>, Kathleen Fisher <kathleen.fisher at gmail.com>
> Subject: Programming Languages Mentoring Workshop (PLMW 2012)
> 
> Hi Matthias,
> 
> Kathleen Fisher, Ron Garcia and I are organizing a mentoring workshop
> at POPL this January. Can you forward this announcement to qualified students 
> (early graduate students and advanced undergrads) that are interested 
> in programming language research? 
> 
> We've been able to raise money to fund the travel of women and 
> underrepresented minorities to attend the workshop---however note that 
> the deadline for travel grant applications is Dec 2nd.
> 
> Thanks,
> Stephanie
> 
> ---------------------------------------------------------------------
> 
> CALL FOR PARTICIPATION
> 
> CRA-W/CDC and SIGPLAN Programming Languages Mentoring Workshop
> Philadelphia, PA (co-located with POPL 2012)
> Tuesday January 24, 2012
> http://www.seas.upenn.edu/~sweirich/plmw12/
> 
> We are pleased to invite students interested in programming languages
> research to the first PL mentoring workshop. The goal of this workshop
> is to introduce senior undergraduate and early graduate students to
> research topics in programming language theory as well as provide
> career mentoring advice to help them get through graduate school,
> land a great job, and succeed. We have recruited leaders from the
> programming language community to provide overviews of current
> research topics, and have organized panels of speakers to give
> students valuable advice about how to thrive in graduate school,
> search for a job, and cultivate habits and skills that will help them
> in research careers.
> 
> This workshop is part of the activities surrounding POPL, the
> Symposium on Principles of Programming Languages, and takes place the
> day before the main conference. One goal of the workshop is to make
> the POPL conference more accessible to newcomers and we hope that
> participants will stay through the entire conference.
> 
> Through the generous donation of our sponsors, we are able to provide
> travel scholarships to fund student participation. These travel
> scholarships will cover reasonable travel expenses (airfare, hotel and
> registration fees) for attendance at both the workshop and the POPL
> conference. Anyone may apply for a travel scholarship, but first
> priority will be given to women and under-represented minority
> applicants.
> 
> The workshop registration is open to all. Students with alternative
> sources of funding for their travel and registration fees are welcome.
> 
> APPLICATION for TRAVEL SUPPORT:
> The travel funding application can be accessed from the workshop web
> site. The deadline for full consideration of funding is December 2,
> 2011. Selected participants will be notified starting December 9th and
> will need to register for the workshop by December 24th.
> 
> ORGANIZERS:
> Stephanie Weirich, Kathleen Fisher and Ron Garcia
> 
> SPONSORS:
> The Computing Research Association's Committee on
> the Status of Women (CRA-W), the Coalition to Diversify Computing
> (CDC), and the ACM Special Interest Group on Programming Languages
> (SIGPLAN).



From chrdimo at ccs.neu.edu  Mon Nov 14 13:53:55 2011
From: chrdimo at ccs.neu.edu (Christos Dimoulas)
Date: Mon, 14 Nov 2011 13:53:55 -0500
Subject: [PRL] [Pl-seminar] Grigore Rosu's visit -- early announcement
In-Reply-To: <4EBC117D.8040606@ccs.neu.edu>
References: <4EBC117D.8040606@ccs.neu.edu>
Message-ID: <4EC163C3.4020800@ccs.neu.edu>


Here is a preliminary schedule for Grigore's visit.

Let me know if there are any conflicts or if someone requested for a 
meeting and his/her name does not show up.

Thanks.

Schedule November 16
--------------------
--------------------

09:15 -- 10:15 : Breakfast at Collonade (Christos Dimoulas)
10:30 -- 11:00 : David Van Horn
11:00 -- 11:30 : Amal Ahmed
11:45 -- 13:30 : Talk
13:30 -- 14:30 : Lunch (Jesse Tov, Amal Ahmed, Matthias Felleisen)
14:30 -- 15:00 : Pete Manolios
15:00 -- 15:30 : Matthias Felleisen
15:30 -- 16:00 : Stevie Strickland
16:00 -- 16:30 : Carl Eastlund
16:30 -- 17:00 : Thomas Wahl
17:00 -- 17:30 : Vincent St-Amour
17:30 -- 18:00 : Asumu Takikawa
18:00 -- 18:30 : Aaron Turon
18:30 -- 19:00 : Stephen Chang
19:00 --       : Dinner (David Van Horn, Thomas Wahl, Olin Shivers, 
Christos Dimoulas)



On 11/10/11 1:01 PM, Christos Dimoulas wrote:
> Next week we have Grigore Rosu (UIUC) visiting.
>
> Grigore will spend next Wednesday (November 16) at our lab. There are
> still some open slots for meetings. Let me know if you are interested.
>
> Here is the info of the talk and a short bio of the speaker:
>
> NEU Programming Languages Seminar presents
>
> Grigore Rosu
> Formal Systems Laboratory (FSL)
> Department of Computer Science
> University of Illinois at Urbana-Champaign
>
> Wednesday, 11/16
>
> 11:45am - 1:30pm
> Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)
>
>
> Title: K and Matching Logic
>
> Abstract:: Would you like to wake up some morning, have a coffee, then
> design a non-trivial programming language, say with multidimensional
> arrays and array references, with functions and references to them, with
> blocks and local declarations, with input/output, with exceptions, with
> nondeterminism and concurrency with synchronization, and so on, and by
> evening to have a reasonably efficient interpreter, a state-space search
> tool and a model checker, as well as a deductive program verifier for
> your language, all correct-by-construction? Then you may be interested
> in K and Matching Logic, because that is what they are aiming for. K is
> a rewrite-based framework for defining formal operational semantics of
> programming languages. A K semantics can be executed, and thus tested,
> as if it was an interpreter for the defined language. This way, we can
> gain confidence in the correctness of our semantics. Then we can use
> precisely that semantics, unchanged, for program analysis and
> verification, without a need to give the language another, e.g.,
> axiomatic or denotational or dynamic, semantics. Matching logic consists
> of a language-independent proof system that allows us to reason about
> programs in any language that is given a rewrite-based operational
> semantics.
>
> Bio: Grigore Rosu is an associate professor in the Department of
> Computer Science at the University of Illinois at Urbana-Champaign
> (UIUC), where he leads the Formal Systems Laboratory (FSL). His research
> interests encompass both theoretical foundations and system development
> in the areas of formal methods, software engineering and programming
> languages. Before joining UIUC in 2002, he was a research scientist at
> NASA Ames. He obtained his Ph.D. at the University of California at San
> Diego in 2000 and his M.S. at the University of Bucharest, Romania, in
> 1996. He was offered the CAREER award by the NSF and the outstanding
> junior award by the Computer Science Department at UIUC in 2005. He won
> an ACM SIGSOFT distinguished paper award at ASE 2008 and the best
> software science paper award at ETAPS 2002. He was ranked a UIUC
> excellent teacher in Spring 2008 and Fall 2004.
>
>
>
> _______________________________________________
> PRL mailing list
> PRL at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/prl
>
> _______________________________________________
> pl-seminar mailing list
> pl-seminar at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/pl-seminar



From chrdimo at ccs.neu.edu  Tue Nov 15 13:28:50 2011
From: chrdimo at ccs.neu.edu (Christos Dimoulas)
Date: Tue, 15 Nov 2011 13:28:50 -0500
Subject: [PRL] Schedule for Grigore Rosu's visit
Message-ID: <4EC2AF62.9010704@ccs.neu.edu>

Here is the schedule for Grigore's visit.

.CHristos

Schedule November 16
--------------------
--------------------

09:15 -- 10:15 : Breakfast at Colonade (Christos Dimoulas)
10:30 -- 11:00 : David Van Horn
11:00 -- 11:30 : Amal Ahmed
11:45 -- 13:30 : Talk
13:30 -- 14:30 : Lunch (Jesse Tov, Amal Ahmed, Matthias Felleisen)
14:30 -- 15:00 : Pete Manolios
15:00 -- 15:30 : Matthias Felleisen
15:30 -- 16:00 : Stevie Strickland
16:00 -- 16:30 : Carl Eastlund
16:30 -- 17:00 : Thomas Wahl
17:00 -- 17:30 : Vincent St-Amour
17:30 -- 18:00 : Asumu Takikawa
18:00 -- 18:30 : Aaron Turon
18:30 -- 19:00 : Stephen Chang
19:15 --           : Dinner (David Van Horn, Thomas Wahl, Olin Shivers, 
Christos Dimoulas)


From wand at ccs.neu.edu  Thu Nov 17 19:31:49 2011
From: wand at ccs.neu.edu (Mitchell Wand)
Date: Thu, 17 Nov 2011 19:31:49 -0500
Subject: [PRL] Fwd: TP Msg. #1136 Poster Perfect - How to Drive Home Your
 Science with a Visually Pleasing Poster.
In-Reply-To: <1760970963.191669.1321575590219.JavaMail.root@zm02.stanford.edu>
References: <1313062765.191548.1321575464046.JavaMail.root@zm02.stanford.edu>
	<1760970963.191669.1321575590219.JavaMail.root@zm02.stanford.edu>
Message-ID: <CAJqwn-89JuWOUF7mRPyrfEq=+vYZi8ovSzqmkq0K_xzNehnxYA@mail.gmail.com>

---------- Forwarded message ----------
From: Rick Reis <reis at stanford.edu>
Date: Thu, Nov 17, 2011 at 7:19 PM
Subject: TP Msg. #1136 Poster Perfect - How to Drive Home Your Science with
a Visually Pleasing Poster.
To: tomorrows-professor <tomorrows-professor at lists.stanford.edu>


Although occasionally there would be visually pleasing posters that
promoted less-than-stellar science, Purrington usually found that ?the
attractiveness of a poster is highly correlated with the quality of the
science,? he said. Graphic design and scientific inquiry require different
skills, but oddly enough, it appeared that ?the people who understood the
beauty of fonts had a sense of pitching their science,? he said.

-----------------------------------------------------------------------------------------------------------------
TOMORROW'S PROFESSOR(sm) eMAIL NEWSLETTER
http://cgi.stanford.edu/~dept-ctl/cgi-bin/tomprof/postings.php

Archives of all past postings can be found at:
http://cgi.stanford.edu/~dept-ctl/cgi-bin/tomprof/postings.php

Sponsored by
Stanford Center for Teaching and Learning
http://ctl.stanford.edu

Folks:

The posting below gives some great tips on preparing posters for
professional meetings, and not just for scientists. It is by Edyta
Zielinska and it appeared in the August 31, 2011 Careers issue of *The
Scientist*: Magazine of the Life Science [
http://www.the-scientist.com/toc/2011/03/]. ? Copyright 2011, The
Scientist, Inc. All rights reserved. Reprinted with permission.

Regards,

Rick Reis
reis at stanford.edu
UP NEXT: The Graduate Student Writer: Tips to Make the Writing Process Work
for You


Tomorrow's Research

------------------------------- 1,576 words ----------------------------

Poster Perfect - How to Drive Home Your Science with a Visually Pleasing
Poster

After many years of walking through poster sessions, Colin Purrington, a
professor of evolutionary biology at Swarthmore College, noticed a trend.
Usually, as he wandered the aisles looking for something to spark his
interest, he?d see a lot of badly designed posters that buried their
scientific messages. Although occasionally there would be visually pleasing
posters that promoted less-than-stellar science, Purrington usually found
that ?the attractiveness of a poster is highly correlated with the quality
of the science,? he said. Graphic design and scientific inquiry require
different skills, but oddly enough, it appeared that ?the people who
understood the beauty of fonts had a sense of pitching their science,? he
said.

Scientists have a lot of good reasons for making bad-looking posters.
Mentors often tell students to go into the hallway and make a poster like
the ones hanging there; posters present preliminary data, which is
sometimes collected up to the last moment before a conference, making
poster design and layout a last-minute affair. Finally, visual and graphic
design is a specialty unto itself, and one that researchers rarely study.

However, there are important reasons for making concise, well-presented,
and eye-catching posters. ?We have really big brains, and a big part of
that brain is dedicated to sight. If the poster doesn?t fit in some nice
visual sense, it just doesn?t work,? and viewers are likely to move on,
says Purrington, who has written an extensive online primer on scientific
poster-making.

*The Scientist* talked to researchers who have sharpened their scientific
pitches, as well as to graphic designers who understand the rationale
behind color, font, and layout choices. Here?s their advice for making a
better poster.

TIPS FOR DESIGN AND FORMATTING

Design pointers from the pros

* Shorten your text lines
Long lines of text are more difficult to read, which is why magazines and
newspapers always break up their text into narrower columns. If your poster
has a landscape orientation, consider breaking your text into four columns.

* Justify the right way: to the left
While justifying text on both the right and left (i.e., full justification)
makes for very neat-looking columns, designers are beginning to move away
from the practice, says Nichole Jonas, a graphics specialist at the Eunice
Kennedy Shriver National Institute of Child Health and Human Development.
It can cause distracting vertical ?rivers? of spaces down the page. Left
justifying text makes for an easier read.

* Consider your font
You don?t have to stick with just one. Adding a little variety, and even
downloading a font that isn?t available on PowerPoint, can make your poster
stand out. But never use more than two or three fonts, says Jonas. She
suggests using sans serif fonts like Helvetica or Gill Sans for the body
and a serif for the titles. (Other designers prefer serif fonts for the
body, as they ?can help guide the eye through the word,? said Jonas.)
?Anything but Comic Sans,? she says, as it tends to look amateurish.

* Don?t put conclusions on the floor
Even though it?s the most important part of the poster, the conclusion is
often placed ?at the bottom, [where] it?s at people?s feet,? says Graves.
She suggests placing it at top of the rightmost column?or, if you feel
daring, start the body of the poster with it.

* Bigger is better
?People have this weird love of small font,? says Purrington. ?They think
it looks professional and that large fonts are for children.? But that?s
not the case, he says. In low light conditions, or when scientists are
reading over other people?s shoulders, larger fonts are essential. LiLynn
Graves, graphic and web designer at the Cornell Center for Materials
Research at Cornell University, suggests a font size of 85pt for the title,
36?44 for the headers, and 24?34 for the body text.

* Dump PowerPoint?s color palette
Many people use PowerPoint to create their poster, but the program was
designed for projecting images in a darkened room. The deep blues and
fluorescent greens that look good in that setting often produce posters
that are too dark and difficult to read, says Graves. Stay away from
primary colors on primary colors (no reds on blues, or reds on yellows).
Instead, Jonas suggests a background in a muted color?one that is closer to
white on the color spectrum?for a more professional tone.

* Sundries
Check for readability at 6 feet; print out a small copy to better judge
your layout choices; use a ruler to make sure all columns are aligned;
stick with black as the text color.

How to make your data easy on the eyes

* Title with a message
Titles are the best way to quickly tell readers what they are supposed to
take away from your data. Always title your graphs, says Purrington.

* Make your findings obvious
Highlight the peak, trough, or other comparison of interest with an arrow
containing the value of that data point. It?s better than making a reader
work out the value from the axes.

* Include the method
While many posters do include a methods section, it is almost always useful
to include a simple description of how you got the data you?re presenting
near the graph, says biochemist Joseph Provost of Minnesota State
University Moorhead, a frequent judge of student posters. Without a simple
caption that describes the experimental method, ?it?s hard to understand
how an experiment was done,? he says.

* Temporarily dump your text
A good way to test to see whether your graphics are serving their intended
purpose: ?If you removed all the info besides the graphics, the poster
should still be pretty good,? says Purrington. ?Scientists are lazy, they
don?t read,? says marine biologist Nando Boero, from the Universit? del
Salento in Lecce, Italy. The graphs should tell the whole story, he says.

* Banish the legend
Legends or keys to multicolored line graphs give a viewer one more thing to
interpret. If possible, annotate your data with labels directly on the
image, says Purrington.

* Sundries
Use graphs rather than tables; avoid cluttered figures; arrange experiments
to tell a story, not in the order they were performed; include enough data
to defend your hypothesis; keep about a 50/50 ratio of graphics to text.


TIPS FOR CLEARER CONTENT

How to write a title

Bad: ?Mural architecture of planula larvae of a cniderian might be
suggestive of the central nervous system?

Good: ?The first brain?

Rationale: A poster is more of an advertisement for your work than a
definitive account, says Boero. There are some things you can?t get away
with when you?re writing a paper. But you can be on the cheeky side of
accurate in posters to capture the attention of a busy passerby.

Bad: ?The MES mess, a good buffer gone bad?

Good: ?How a common cell culture pH buffer interferes with transport
assays?

Rationale: It?s best to avoid acronyms and jargon when aiming for a general
audience. Scientists tend to wander through poster sessions. If you can nab
a researcher from another field, you may have won a future collaborator, or
someone who will offer a new perspective on your work, says Mark Wallert, a
researcher at Minnesota State University Moorhead and frequent poster
judge.

Sundries:
Never use ALL CAPS in titles; emphasize titles in one way: boldface,
italics, or underline, but never all three.

Improve your body

* Link images and text
Unlike journal articles, where tables and graphs are often located at a
distance from their description in the text, ?in a poster, the words must
be near the visual aid,? says Boero. ?You have that possibility, so use
it.?

* Cut your text
Once you?ve created your content, read it again to see how many words you
can cut, says Boero. Pretend you?re writing a telegram, and paying for
every word, he suggests.

* Make killer bullets
Limit bulleted lists to the conclusion section, if possible. There, lay out
4?5 summary statements that capture what your data means and its wider
implications.

* Answer your hypothesis
Make sure your conclusion is more than a restatement of your results. It
should directly address the hypothesis you lay out in the intro or
abstract.

The Checklist: What to do before you print

* Give it a test run
In his experience, Wallert says, ?you find [mistakes] when you?re standing
in front of your poster? at the conference. To save yourself the
embarrassment, project your poster on the wall of your lab and run through
your presentation, he suggests.

* Check your file size
Make sure you haven?t inserted a 500 MB image, or one that?s low
resolution. ?If a person has never done a poster, they?ll probably make one
of those mistakes,? says Purrington

* Are your axes labeled?
Oddly enough, missing axis labels are something that poster judges Wallert
and Provost see often.

* Check your message
Once you?ve made your poster look its best, give it one more read-through
to make sure that it presents the point of your research in the most
convincing light.

* Color check
Make sure the colors you?ve chosen are readable in low light. It?s hard to
predict where your poster will be placed, so make sure your choices work in
different settings.

* Check dimensions
Although this should really be the first thing you do, not the last, it?s a
good idea to make sure your poster conforms to the meeting?s size and
orientation specifications.

Resources

* Get feedback on your science
Post your poster on Faculty of 1000 (posters.f1000.com) to get feedback
from experts (F1000 is The Scientist?s sister company). More tips at
posters.f1000.com/postertips

* Buy software that does it for you
Check out Poster Genius, a program that formats your content into a clean
layout. You simply enter your text and figures, and it selects the right
font and tests for optimal readability under conference-hall conditions.
www.postergenius.com/cms/index.php

* Add technology
Add a QR (Quick Response) code, the multimedia bar code, for access to your
video or sound files (or a digital handout of your poster). Pros: you can
add those cool videos of your fluorescing C. elegans. Cons: they only work
for smart-phone owners. Download QR codes here:www.qrstuff.com or here
qrcode.kaywa.com

* Scientific Poster Design
A visual how-to for improving posters, with many examples:
www.cns.cornell.edu/documents/ScientificPosters.pdf

* Elements of Style
Graphic design elements as they apply to scientific posters:
Science.nichd.nih.gov/confluence/display/~jonasnic/Elements+of+Style

* Better Posters
Great blog with constantly updated resources for better poster-making:
betterposters.blogspot.com

* * * * * * *
NOTE: Anyone can SUBSCRIBE to the Tomorrows-Professor Mailing List by going
to:
https://mailman.stanford.edu/mailman/listinfo/tomorrows-professor

To UNSUBSCRIBE just reply to this posting with the word "unsubscribe" in
the top body of the text.



--++**==--++**==--++**==--++**==--++**==--++**==--++**==
tomorrows-professor mailing list
tomorrows-professor at lists.stanford.edu
https://mailman.stanford.edu/mailman/listinfo/tomorrows-professor
-------------- next part --------------
HTML attachment scrubbed and removed

From matthias at ccs.neu.edu  Fri Nov 18 09:20:41 2011
From: matthias at ccs.neu.edu (Matthias Felleisen)
Date: Fri, 18 Nov 2011 09:20:41 -0500
Subject: [PRL] Fwd: [TYPES/announce] MSRC Researcher and Postdoc positions
References: <45F6C1B611EEBE449F713744E6D0330F0F9A5A43@TK5EX14MBXC110.redmond.corp.microsoft.com>
Message-ID: <F36930B9-5946-4245-BC20-E542D38C5987@ccs.neu.edu>


If you're not on types, sign up 



Begin forwarded message:

> From: Matthew Parkinson <mattpark at microsoft.com>
> Date: November 18, 2011 8:20:54 AM EST
> To: "types-announce at lists.seas.upenn.edu" <types-announce at lists.seas.upenn.edu>
> Subject: [TYPES/announce] MSRC Researcher and Postdoc positions
> 
> [ The Types Forum (announcements only),
>     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
> 
> The following advertisement might be of interested to readers of the TYPES mailing list.
>  
> Matt
> ---
> Open Research Positions
>  
> We at MSR-Cambridge are seeking candidates from all areas of Computer  Science, including theoretical foundations, systems, networking,  programming languages, and machine learning. We are also interested  in candidates doing research at the frontiers of Computer Science  with other disciplines (such as finance, biology). We give higher  priority to the overall originality and promise of the candidate's  work than to the candidate's sub-area of specialization.
>  
> Deadline for applications for the Programming Principles and Tools group is 6th January 2012 for Researchers and 22nd February 2012 for Postdocs.
>  
> Further information can be found at
> http://research.microsoft.com/en-us/jobs/fulltime/researcher.aspx      
>  
> Applications are through
> http://research.microsoft.com/en-us/jobs/fulltime/apply_researcher.aspx  

-------------- next part --------------
HTML attachment scrubbed and removed

From samth at ccs.neu.edu  Sun Nov 20 09:43:13 2011
From: samth at ccs.neu.edu (Sam Tobin-Hochstadt)
Date: Sun, 20 Nov 2011 09:43:13 -0500
Subject: [PRL] Interesting information about Java's new function syntax,
 and approach to parallelism
Message-ID: <CAK=HD+aThaN2_77SwkJOT5FOkcVHiL=M6ef9DxrfXcGnjAczrA@mail.gmail.com>

This presentation
http://blogs.oracle.com/briangoetz/resource/devoxx-lang-lib-vm-co-evol.pdf
has a lot of neat stuff in it.

-- 
sam th
samth at ccs.neu.edu


From turon at ccs.neu.edu  Mon Nov 28 13:56:45 2011
From: turon at ccs.neu.edu (Aaron Turon)
Date: Mon, 28 Nov 2011 13:56:45 -0500
Subject: [PRL] Fwd: Whatever happened to partial evaluation?
Message-ID: <CAGfQ5atQyDAHBTKE0QwqtHhpeiC3GrVeZjQaj4hSx=Pt=RNCvQ@mail.gmail.com>

---------- Forwarded message ----------
From:?Alexey Radul <axch at mit.edu>
To:?prl at lists.ccs.neu.edu
Date:?Mon, 28 Nov 2011 10:54:11 -0500
Subject:?Whatever happened to partial evaluation?

Hello PRL,

A question for your collective wisdom:

What ever happened to partial evaluation? ?It seems like such a
promising compilation technique -- the ability to write embedded
interpreters with no performance cost could be called the holy grail
of the Lisp Way -- but research interest appears to have fallen off a
cliff at the turn of the century. ?partial-eval.org is dead. ?The
partial evaluation section on read-scheme.org just stops. ?I may be
misreading the paper titles and abstracts, but PEPM (the workshop on
Partial Evaluation and Program Manipulation) seems to have drifted off
to be pretty much just Program Manipulation.

My question is, what happened? ?Did the community decide that partial
evaluation is done, and it's up to industry to adopt it? ?If so, am I
right that industry largely did not? ?Also, is there any good summary
of the research consensus about the "right way" to do partial
evaluation, or the tradeoffs that it is up to industry to make?

If not, did the community decide that partial evaluation doesn't work
and give up? ?If they did, is there any summary anywhere of what the
insurmountable problem turned out to be? ?And what ways to surmount it
were attempted and why they didn't work? ?I have a hunch that the
killer is intermediate expression bulge of huge numbers of specialized
variants during compilation, but I would really appreciate reading a
cogent discussion of attempts to mitigate this problem and how well or
poorly they worked.

Alternately, is research activity still proceeding under a different
name? ?What are "supercompilation" and "distillation", and how are
they related?

The reason I ask is that my group is trying to get automatic
differentiation to be both first-class and efficient. ?(Why? ?Because
AD can generate gradients of machine learning models without manual
input -- if made practical, this could revolutionize machine
learning.) ?Efficient but not first-class, and in particular poorly
nestable, automatic differentiation can be had from the
source-to-source transformers at autodiff.org; first-class but
inefficient automatic differentiation can be had by operator
overloading. ?We were eying partially evaluating away all the
allocation overhead of operator overloading to get a first-class and
efficient implementation.

Does this sound like a plausible research agenda? ?What is the
canonical reference for how to implement a partial evaluator for this
kind of purpose? ?(Yes, I read Jones, Gomard, and Sestoft 1993
"Partial Evaluation and Program Generation"; is there anything more
modern?) ?Else, is there argumentation that partial evaluation will
not serve this purpose?

Thank you,
~Alexey Radul


From matthias at ccs.neu.edu  Mon Nov 28 14:37:53 2011
From: matthias at ccs.neu.edu (Matthias Felleisen)
Date: Mon, 28 Nov 2011 14:37:53 -0500
Subject: [PRL] Fwd: Whatever happened to partial evaluation?
In-Reply-To: <CAGfQ5atQyDAHBTKE0QwqtHhpeiC3GrVeZjQaj4hSx=Pt=RNCvQ@mail.gmail.com>
References: <CAGfQ5atQyDAHBTKE0QwqtHhpeiC3GrVeZjQaj4hSx=Pt=RNCvQ@mail.gmail.com>
Message-ID: <17F2AF31-0356-4D53-B7C0-A5CC3C396CEE@ccs.neu.edu>


On Nov 28, 2011, at 1:56 PM, Aaron Turon wrote:

> The reason I ask is that my group is trying to get automatic
> differentiation to be both first-class and efficient.  (Why?  Because
> AD can generate gradients of machine learning models without manual
> input -- if made practical, this could revolutionize machine
> learning.)  Efficient but not first-class, and in particular poorly
> nestable, automatic differentiation can be had from the
> source-to-source transformers at autodiff.org; first-class but
> inefficient automatic differentiation can be had by operator
> overloading. 


Hi Alexey, I cannot respond to your general question but I
would like to point to two people re your specific research
agenda. 

-- Jeff Siskind (Purdue) and collaborators worked on just this idea. 
See their POPL '07 papers in Nice, France. They work in Stalin Scheme, 
and they are definitely aware of partial evaluation. 

-- Mike Fagan (Rice) is the main author of a 90-ish award winning 
differentiation program (they also dealt with adjoins) for Fortran, 
ADIFOR. The first version of this program was also written in Scheme, 
and for all I know they still use Scheme. Mike is definitely familiar
with partial evaluation and such things. 

You may wish to ask these two people because they can evaluate your 
question in context. 

-- Matthias



From samth at ccs.neu.edu  Mon Nov 28 14:58:52 2011
From: samth at ccs.neu.edu (Sam Tobin-Hochstadt)
Date: Mon, 28 Nov 2011 14:58:52 -0500
Subject: [PRL] Fwd: Whatever happened to partial evaluation?
In-Reply-To: <CAGfQ5atQyDAHBTKE0QwqtHhpeiC3GrVeZjQaj4hSx=Pt=RNCvQ@mail.gmail.com>
References: <CAGfQ5atQyDAHBTKE0QwqtHhpeiC3GrVeZjQaj4hSx=Pt=RNCvQ@mail.gmail.com>
Message-ID: <CAK=HD+bUGT+0_+uX3H69LcGfncToBfq7SqzJoMReP3RLJcizbA@mail.gmail.com>

On Mon, Nov 28, 2011 at 1:56 PM, Aaron Turon <turon at ccs.neu.edu> wrote:
>
> Alternately, is research activity still proceeding under a different
> name?

Research on partial evaluation certainly continues.  At OOPSLA this
year, the best student paper was "Hybrid Partial Evaluation" by Shali
and Cook [1].

[1] http://www.cs.utexas.edu/~wcook/Civet/
-- 
sam th
samth at ccs.neu.edu


From wand at ccs.neu.edu  Wed Nov 30 09:50:10 2011
From: wand at ccs.neu.edu (Mitchell Wand)
Date: Wed, 30 Nov 2011 09:50:10 -0500
Subject: [PRL] Fwd: Bug bytes; Popping in on research; Caption contest
In-Reply-To: <1108868532495.1101418328690.14103.2.460855BC@scheduler>
References: <1108868532495.1101418328690.14103.2.460855BC@scheduler>
Message-ID: <CAJqwn-_SO0CjXzJoy+5NfPTr8zkeHtf5sAqx3rMGeyF-eFnVeA@mail.gmail.com>

In case (as is likely) your mail filter auto-discards the daily
"news at Northeastern", here is Pete, featured on the front page!  Way to go,
Pete!

--Mitch

---------- Forwarded message ----------
From: News at Northeastern <news at neu.edu>
Date: Wed, Nov 30, 2011 at 9:00 AM
Subject: Bug bytes; Popping in on research; Caption contest
To: wand at ccs.neu.edu


Having trouble viewing this email? Click here
<http://campaign.r20.constantcontact.com/render?llr=st7l9ybab&v=001J8BvtJGIt7tzi5FQll0q6AGDxCRZIPvj8dXkqGsLCFH8cUzIqsucPwhgHEw9W56IDEHQtdwDAM3moAkRDv1oe3eszMxtPG2oTTgt93Y2jvlXbB3DGDZy90yJ7SomI_H1ocSqCOQQwJ3EtXgCSMT2YLQTyo-V4ApdCOoZ3H-NKtvVdFJGz7XYeEHfQ9HWitVWgTuWO_ta4WQ%3D>
     [image: news at Northeastern]<http://r20.rs6.net/tn.jsp?llr=st7l9ybab&et=1108868532495&s=14103&e=001nxksV8eXIpG694uA_AtHjdD0h4aA4qjX7Ia6B3igqCGgk8Os8Daa19ofban12RvX6JnS99-CWw5r0ktOtg3Dp7Up0t1CbbSLYKZ4jDZkCrDPOcp-xd6_nlkbPECI0Ui2>
*November 30, 2011
<http://r20.rs6.net/tn.jsp?llr=st7l9ybab&et=1108868532495&s=14103&e=001nxksV8eXIpFGdqjvZ1NcDyrhS_kIysdqqeW3GuUwHlHeV_hDjOdEtUArHInTCtDgXK5jHCzu4FD1a3bacaaPcHTUsZ1Wcd1b2v0HvlalvP7JOZYpYLI_xiKWDQWS1FUq>
*
<http://r20.rs6.net/tn.jsp?llr=st7l9ybab&et=1108868532495&s=14103&e=001nxksV8eXIpH9zBp6K7st4dbOWape_pjq5zjaEWD4Hlk4apKDNAyLJ_wLQBmqw6x_tBxlSexOJW30LesClbJEg4wR6jCqNl_KepQcDJGWN7EC0H0WObjLr4aKjrdKoysj4qlmVOgocu34FvSHTkbbiCUv_vAxJyuW5XYSKK8am5XWrwkKZllRiHvhKKAI0pip>
  Digital pest control<http://r20.rs6.net/tn.jsp?llr=st7l9ybab&et=1108868532495&s=14103&e=001nxksV8eXIpH9zBp6K7st4dbOWape_pjq5zjaEWD4Hlk4apKDNAyLJ_wLQBmqw6x_tBxlSexOJW30LesClbJEg4wR6jCqNl_KepQcDJGWN7EC0H0WObjLr4aKjrdKoysj4qlmVOgocu34FvSHTkbbiCUv_vAxJyuW5XYSKK8am5XWrwkKZllRiHvhKKAI0pip>

Northeastern computer scientists will use a National Science Foundation
grant to design algorithms that will pinpoint bugs in software and hardware
systems. *>><http://r20.rs6.net/tn.jsp?llr=st7l9ybab&et=1108868532495&s=14103&e=001nxksV8eXIpH9zBp6K7st4dbOWape_pjq5zjaEWD4Hlk4apKDNAyLJ_wLQBmqw6x_tBxlSexOJW30LesClbJEg4wR6jCqNl_KepQcDJGWN7EC0H0WObjLr4aKjrdKoysj4qlmVOgocu34FvSHTkbbiCUv_vAxJyuW5XYSKK8am5XWrwkKZllRiHvhKKAI0pip>
*



<http://r20.rs6.net/tn.jsp?llr=st7l9ybab&et=1108868532495&s=14103&e=001nxksV8eXIpF_6hpK1UmpjiJXdQeoLOojqLYm7xaAYPiO8Hofdr2P70lSs-dxIBC8RtS808PPsYek38qnmc1VlHJfyfMUd11-58rJY8JKHI-yYnsy82RFqtnAnlWNG9SsUv0fFPGuRCJbJcHhfIlweLidP0hmDHb61qyLXD1rieDBTZBlfGXjWw==>
  3Qs: Shaping the election through the
media<http://r20.rs6.net/tn.jsp?llr=st7l9ybab&et=1108868532495&s=14103&e=001nxksV8eXIpF_6hpK1UmpjiJXdQeoLOojqLYm7xaAYPiO8Hofdr2P70lSs-dxIBC8RtS808PPsYek38qnmc1VlHJfyfMUd11-58rJY8JKHI-yYnsy82RFqtnAnlWNG9SsUv0fFPGuRCJbJcHhfIlweLidP0hmDHb61qyLXD1rieDBTZBlfGXjWw==>

Alan Schroeder, an associate professor of journalism in the College of
Arts, Media and Design, analyzes the role of the media in the 2012 GOP
primary election.
*>><http://r20.rs6.net/tn.jsp?llr=st7l9ybab&et=1108868532495&s=14103&e=001nxksV8eXIpF_6hpK1UmpjiJXdQeoLOojqLYm7xaAYPiO8Hofdr2P70lSs-dxIBC8RtS808PPsYek38qnmc1VlHJfyfMUd11-58rJY8JKHI-yYnsy82RFqtnAnlWNG9SsUv0fFPGuRCJbJcHhfIlweLidP0hmDHb61qyLXD1rieDBTZBlfGXjWw==>
*
  *Selected Events**
*
Today 12 p.m.
Free Cooking Demo<http://r20.rs6.net/tn.jsp?llr=st7l9ybab&et=1108868532495&s=14103&e=001nxksV8eXIpFspB-rziPXWoo8LUfdRhVZpctQU3ChhXCec-DNXIDwkzQ9VlvYaTUehc6jRJexdUV1CQIYvR0jjNnaExuSDDdk4tWfv3Chmk6uxd9ivBpgJBgGcHB691O8B3BVowhDXttQFEMf1LAJBFpL0n23DJwBEvtEoNi0ieZT5Kf21lVqeAceSF-2WfB9jXJ1DfHpXdJQ2vBASdPHww==>

Today 5 p.m.
An American Poet in the 21st
Century<http://r20.rs6.net/tn.jsp?llr=st7l9ybab&et=1108868532495&s=14103&e=001nxksV8eXIpGas92KypP395I2616m2PqC5SwWhMYc4wk7QQr8q_63qQ4tS7sGdFBIyM3Cn7UwWLiu5ImNcc5XuJpKBd7mV9L3gPiZdHn14loOGuX9spoNB9kXsVZoHE07b_jz78TPAvuaaz_tM8m1N8aTtuynC9NKcZR0npBjSJBP4MIv6umUOh-wuJ0vOW7rU-QwWNoNkFWQIAsmaNmWZA==>

Tomorrow 5 p.m.
Profiles in Innovation<http://r20.rs6.net/tn.jsp?llr=st7l9ybab&et=1108868532495&s=14103&e=001nxksV8eXIpG_hqY7RB-dE3SpMdq6UuZZQpcUmuf0ukhyRNzUgcFEH0lpe2DBD8KGrFnI9HjkeMfK4eldg1xFPvC_QKmRQ9EZh8lAJn_NKQswK5Ab8AvUyMRpvycibEyyZacF45V8NYkac-ynU3tTpcIXMJ98G3HC>

Full Event Calendar<http://r20.rs6.net/tn.jsp?llr=st7l9ybab&et=1108868532495&s=14103&e=001nxksV8eXIpEDcIyfHH71IQ9K7cYQfIIArvshiwUXKsvFMVsXSLFYISRrz-ZqL9EIn7nklN0DCtbjrsmlZWOoBfsVTO7smQutPVxTVE6VKkyefqpQFisovWjSn8PsBisId6i6Fr6Ig8M=>
        [image:
rss]<http://r20.rs6.net/tn.jsp?llr=st7l9ybab&et=1108868532495&s=14103&e=001nxksV8eXIpEosYx1madr-OHyiZF9dy57gNkrg2eqWczqGBRiLSpJOL-oy-IfSBEHSjxZXofE7WBirSZ1dHZkobVnCHjf6SIAzSIM1Pg6epyG-k3aAQb1O1eZiOmbsNe0Bjm8voYUriSb4sG3Zg--Dg==>
 [image: twitter]<http://r20.rs6.net/tn.jsp?llr=st7l9ybab&et=1108868532495&s=14103&e=001nxksV8eXIpHiL22FEWeLPg4uxLmK3yjlxjsJcQGFkRgLt8im9Q75QsUWR3WFP0TmgBGFywide-Vds75YXbCfl1owKSy5MrFryiINZpVzkjh3tCY6KWyQDYGsE66bgfC4DdXzKVrXa14=>
 [image: facebook]<http://r20.rs6.net/tn.jsp?llr=st7l9ybab&et=1108868532495&s=14103&e=001nxksV8eXIpENJRi09YvB3TYaRI0RQVhl7DjXPNA22HCVo_Dg5h0pPmA7fHRqCTAJ_n2YTbWNcfZao8pZ3ZrKVhay3OpfU3MbE3Bccx5-LRAgEuskCguciVORI1wkyF_spBURzluDlZU=>
 [image: youtube]<http://r20.rs6.net/tn.jsp?llr=st7l9ybab&et=1108868532495&s=14103&e=001nxksV8eXIpE4cPZtv56HeYncC-gi1KipvVzJ5VxNOQOo3vh15kx7ed4xZt4G9WvOxp6on4Z1gFq7XH0g2slR3lAnMcXGJcrT3Z2n9E5Dqenem2U2PKnr5iHVZc0itbA9>
<http://r20.rs6.net/tn.jsp?llr=st7l9ybab&et=1108868532495&s=14103&e=001nxksV8eXIpHtnJaVcTbZi3RGBKQQUZe0BTetspOMiq74yKogWNdt4-Tj9JgHzlU7CqKiSWripMJPYCi_FgqPmVuerJUc-km2gNwSyjy66qAksYLIXa-2yVU-b5U4Jqvk7ybQct9QbRSh2bI_xdEvNIKFa5qZib4i-Fl-_N75n47kDTjcgHzH-SW0DNXlzMNh>
  "Pop-up" meetings to highlight faculty
research<http://r20.rs6.net/tn.jsp?llr=st7l9ybab&et=1108868532495&s=14103&e=001nxksV8eXIpHtnJaVcTbZi3RGBKQQUZe0BTetspOMiq74yKogWNdt4-Tj9JgHzlU7CqKiSWripMJPYCi_FgqPmVuerJUc-km2gNwSyjy66qAksYLIXa-2yVU-b5U4Jqvk7ybQct9QbRSh2bI_xdEvNIKFa5qZib4i-Fl-_N75n47kDTjcgHzH-SW0DNXlzMNh>

New open house events will bring faculty and students together to explore
lab spaces and spark research collaborations, starting with the
Interdisciplinary Affective Science Laboratory on Dec. 5.
*>><http://r20.rs6.net/tn.jsp?llr=st7l9ybab&et=1108868532495&s=14103&e=001nxksV8eXIpHtnJaVcTbZi3RGBKQQUZe0BTetspOMiq74yKogWNdt4-Tj9JgHzlU7CqKiSWripMJPYCi_FgqPmVuerJUc-km2gNwSyjy66qAksYLIXa-2yVU-b5U4Jqvk7ybQct9QbRSh2bI_xdEvNIKFa5qZib4i-Fl-_N75n47kDTjcgHzH-SW0DNXlzMNh>
*
*Selected Media Coverage**
*

*Few changes expected with airline
bankruptcy<http://r20.rs6.net/tn.jsp?llr=st7l9ybab&et=1108868532495&s=14103&e=001nxksV8eXIpF1ljiDnV4kKDbHvuQ1Knb77sopTFjRoQS_xQ_cpd3fUpWNWOZfJ3iJ353WroNvcCtvYGzdjwnl5kdfH2swAjn8xgG9ivA1LZZ77r0m7UnEQuiamDA9cOzqMbZFvgtV0fmgayIVvZY1LcBg_uZaZXdwtkyXxIHNVJzu-6yQ5QxpLt8DMPYvwZJ3G11OxFIi8grVNMn-EA2uJAQv_TZhnXW_>
*
Boston Globe (November 30)

*Janet Echelman's world-wide webs at
Northeastern<http://r20.rs6.net/tn.jsp?llr=st7l9ybab&et=1108868532495&s=14103&e=001nxksV8eXIpHiL22FEWeLPjrBQk8Vz30EwfuZkNzKh7XVwqq2-GuIpFng6YSiRjNFxai41fbWX7GeDhkyOZEYUh91v-M-M1Xdgc0tUsD5X0VaU1xWF4qwgP-9GFPGFgxqLdbx80HVbEj3CkuZ2EkyIVo8QNMVift-JjHnctfV4venvfeXfIF3Yl9JR0fH9yek>
*
The Hub Review (November 29)

*Say it ain't so, Joe: US sector's pact with the drop-kick
devil<http://www.timeshighereducation.co.uk/story.asp?sectioncode=26&storycode=418204&c=1>
*
Times Higher Education (November 24)
  *Caption Contest*
<http://r20.rs6.net/tn.jsp?llr=st7l9ybab&et=1108868532495&s=14103&e=001nxksV8eXIpHRVGbqWdqdQeHS_JoAgx5WunXQH5zWAMPXw3B02VOon7nG78OHay-t_VxnLKVzVOiv9WBxsoggQdtlVScdlDIp7G-Xu4IrU8MGVCShkBiLJsBcQx382AGi1WDDlpVUmnn3ZwyZlZX0I0dFF-l-S0UaANtvY7qJE-bSCczuPwOUdukbOs3QecT1>
Send us your best caption!
*>><http://r20.rs6.net/tn.jsp?llr=st7l9ybab&et=1108868532495&s=14103&e=001nxksV8eXIpHRVGbqWdqdQeHS_JoAgx5WunXQH5zWAMPXw3B02VOon7nG78OHay-t_VxnLKVzVOiv9WBxsoggQdtlVScdlDIp7G-Xu4IrU8MGVCShkBiLJsBcQx382AGi1WDDlpVUmnn3ZwyZlZX0I0dFF-l-S0UaANtvY7qJE-bSCczuPwOUdukbOs3QecT1>
*
      *Published by Northeastern University Office Of Marketing &
Communications<http://r20.rs6.net/tn.jsp?llr=st7l9ybab&et=1108868532495&s=14103&e=001nxksV8eXIpGk1GyWywvkF2-9oZ2jBXfoc10Yj0GtvbnfqLpOk1ZNdrJmC94XUgBOcF2EkHfTL_7UahB44P_haI35aXwOXZxjCfSBAYQ8Pd24kDDxCKXh1Su7Id9QdJVnFO5Z9GTMk-8=>|
Unsubscribe<http://ui.constantcontact.com/d.jsp?p=un&m=1101418328690&ea=wand%40ccs.neu.edu&se=14103&t=1104385165753&lang=en&reason=F>|
Sign
up for Daily News<http://visitor.constantcontact.com/manage/optin/ea?v=001M6t4uPDAuUrRhfg5ZdtHxg%3D%3D>
*  Copyright ? 2011. All Rights Reserved.
           Forward
email<http://ui.constantcontact.com/sa/fwtf.jsp?llr=st7l9ybab&m=1101418328690&ea=wand%40ccs.neu.edu&a=1108868532495>

<http://visitor.constantcontact.com/do?p=un&mse=001M6t4uPDAuUoDW0BBqRUK9rR2voVLReTJ5mmzZ7OT-LQ%3D&t=001c1gVRPc_CBvu7M17TeXrFA%3D%3D&lang=001FCSs65SMrsI%3D&reason=001IqezpQbqEsU%3D&llr=st7l9ybab>
This email was sent to wand at ccs.neu.edu by news at neu.edu |
Update Profile/Email
Address<http://visitor.constantcontact.com/do?p=oo&mse=001M6t4uPDAuUoDW0BBqRUK9rR2voVLReTJ5mmzZ7OT-LQ%3D&t=001c1gVRPc_CBvu7M17TeXrFA%3D%3D&lang=001FCSs65SMrsI%3D&reason=001IqezpQbqEsU%3D&llr=st7l9ybab>
| Instant removal with
SafeUnsubscribe<http://visitor.constantcontact.com/do?p=un&mse=001M6t4uPDAuUoDW0BBqRUK9rR2voVLReTJ5mmzZ7OT-LQ%3D&t=001c1gVRPc_CBvu7M17TeXrFA%3D%3D&lang=001FCSs65SMrsI%3D&reason=001IqezpQbqEsU%3D&llr=st7l9ybab>?
| Privacy Policy <http://ui.constantcontact.com/roving/CCPrivacyPolicy.jsp>.
 News at Northeastern University | 716 Columbus Ave., Ste. 598 | Boston | MA |
02120
-------------- next part --------------
HTML attachment scrubbed and removed

From sstrickl at ccs.neu.edu  Wed Nov 30 10:52:06 2011
From: sstrickl at ccs.neu.edu (Stevie Strickland)
Date: Wed, 30 Nov 2011 10:52:06 -0500
Subject: [PRL] Scheduling for Gary T. Leavens's visit on 12/7
Message-ID: <EC4DAD19-39AC-4C22-8858-3F44925CBF9B@ccs.neu.edu>

Hi all,

Gary T. Leavens (http://www.cs.ucf.edu/~leavens/homepage.html) will be visiting us next Wednesday (12/7) to give a talk at the PL Seminar.  If you're interested in meeting with him, please let me know what times you're available that day.

Thanks,
Stevie

From sstrickl at ccs.neu.edu  Wed Nov 30 13:45:38 2011
From: sstrickl at ccs.neu.edu (Stevie Strickland)
Date: Wed, 30 Nov 2011 13:45:38 -0500
Subject: [PRL] 12/7: Gary T. Leavens, "JML's Rich,
	Inherited Specifications for Behavioral Subtypes"
Message-ID: <D10C41DF-9FF3-4109-B1E0-FB87472A2F65@ccs.neu.edu>

NEU Programming Languages Seminar presents

Gary T. Leavens
University of Central Florida

Wednesday, 12/7

11:45am - 1:30pm
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Title: JML's Rich, Inherited Specifications for Behavioral Subtypes

Abstract:

The Java Modeling Language (JML) is used to specify detailed designs for Java classes and interfaces. It has a particularly rich set of features for specifying methods. This talk describes those features, with particular emphasis on the features related to specification inheritance. It shows how specification inheritance in JML forces behavioral subtyping, through a discussion of semantics and examples. It also describes a notion of modular reasoning based on static type information, supertype abstraction, which is made valid in JML by methodological restrictions on invariants, history constraints, and initially clauses and by behavioral subtyping.

Bio:

Gary T. Leavens is a professor and interim chair of the department of EECS, Computer Science Division at the University of Central Florida (UCF). He joined UCF in August 2007, was associate chair from August 2008 to August 2010, and was appointed interim chair in September 2010. Previously he was a professor of computer science at Iowa State University in Ames, Iowa, where he started in January 1989. He received his Ph.D. from MIT in 1989. Before his graduate studies at MIT, he worked at Bell Telephone Laboratories in Denver Colorado as a member of technical staff.

Professor Leavens's research interests include programming and specification language design and semantics, program verification, and formal methods, with an emphasis on the object-oriented and aspect-oriented languages.  His best known work in the area of formal methods is related to the JML project, an international effort with many associated tools (see http://jmlspecs.org).  His work on specification languages embodies insights from his work on the theory of behavioral subtyping (with David Naumann, Don Pigozzi, and others). His best known work on language design and semantics is on aspect-oriented programming (joint with Curtis Clifton, James Noble, Hridesh Rajan, and Medhi Bagherzadeh) and multiple dispatch languages such as MultiJava. See http://www.eecs.ucf.edu/~leavens for more information on his research.

Thanks,
Stevie

From samth at ccs.neu.edu  Thu Dec  1 08:59:15 2011
From: samth at ccs.neu.edu (Sam Tobin-Hochstadt)
Date: Thu, 1 Dec 2011 08:59:15 -0500
Subject: [PRL] Fwd: [MIT-PL] PL Seminar on Monday: Hongwei Xi on the ATS
	language
In-Reply-To: <4ED782DD.6090802@csail.mit.edu>
References: <4ED782DD.6090802@csail.mit.edu>
Message-ID: <CAK=HD+bVWx-Eju09=eiQexcha0qUMpvdg2HiuZ5tPpQo58vdEw@mail.gmail.com>

This looks potentially interesting to many PRL folks.

---------- Forwarded message ----------
From: Adam Chlipala <adamc at csail.mit.edu>
Date: Thu, Dec 1, 2011 at 8:36 AM
Subject: [MIT-PL] PL Seminar on Monday: Hongwei Xi on the ATS language
To: pl at lists.csail.mit.edu


Date: December 5
Time: 4:00-5:30
Room: 32-D463 (Star)

Speaker: Hongwei Xi <http://www.cs.bu.edu/~hwxi/>, Boston University

Title: Views and Viewtypes in ATS

ATS is a statically typed general-purpose programming language. ?The
signatory feature of ATS is a programming paradigm named
programming-with-theorem-proving in which code for (run-time)
computation and code for proof construction can be written in a
syntactically intertwined manner. ?In ATS, there is direct support for
both dependent types and linear types. While the dependent types in
ATS, which are of a restricted form originated from the development of
Dependent ML (DML), are well-studied, the linear types in ATS are much
less well-known. ?In this talk, I will give an introduction to a
notion of linear types referred to as viewtypes in ATS, which combine
views (i.e., linear types for proofs) and types (for run-time values).
In addition, I will present several concrete examples to illustrate
certain practical uses of views and viewtypes.

_______________________________________________
Pl mailing list
Pl at lists.csail.mit.edu
https://lists.csail.mit.edu/mailman/listinfo/pl
http://projects.csail.mit.edu/pl


-- 
sam th
samth at ccs.neu.edu


From dvanhorn at ccs.neu.edu  Thu Dec  1 10:48:02 2011
From: dvanhorn at ccs.neu.edu (David Van Horn)
Date: Thu, 01 Dec 2011 10:48:02 -0500
Subject: [PRL] Fwd: [Programming] Fwd: [MIT-PL] PL Seminar on Monday:
 Hongwei Xi on the ATS language
In-Reply-To: <4ED78362.4090203@csail.mit.edu>
References: <4ED78362.4090203@csail.mit.edu>
Message-ID: <4ED7A1B2.3070803@ccs.neu.edu>



-------- Original Message --------
Subject: [Programming] Fwd: [MIT-PL] PL Seminar on Monday: Hongwei Xi on 
the ATS language
Date: Thu, 01 Dec 2011 08:38:42 -0500
From: Adam Chlipala <adamc at csail.mit.edu>
To: programming at eecs.harvard.edu

This talk might be of interest to some of you.

I'll also take this opportunity to point out that we have a PL Seminar
at MIT now. :)
      http://projects.csail.mit.edu/pl/#seminar
      https://lists.csail.mit.edu/mailman/listinfo/pl


-------------- next part --------------
An embedded message was scrubbed...
From: Adam Chlipala <adamc at csail.mit.edu>
Subject: [MIT-PL] PL Seminar on Monday: Hongwei Xi on the ATS language
Date: Thu, 01 Dec 2011 08:36:29 -0500
Size: 4044
Url: http://lists.ccs.neu.edu/pipermail/prl/attachments/20111201/fc99cfc6/attachment.eml 
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: Attached Message Part
Url: http://lists.ccs.neu.edu/pipermail/prl/attachments/20111201/fc99cfc6/attachment.txt 

From sstrickl at ccs.neu.edu  Fri Dec  2 13:12:37 2011
From: sstrickl at ccs.neu.edu (Stevie Strickland)
Date: Fri, 2 Dec 2011 13:12:37 -0500
Subject: [PRL] Second call for scheduling requests for Gary T. Leavens, 12/7
Message-ID: <46CE7199-733D-4190-B1BB-BAD7D58398DD@ccs.neu.edu>

Hi all,

We still have a couple of slots available to talk with Dr. Leavens (http://www.eecs.ucf.edu/~leavens/) next Wednesday (12/7).  If you're interested, please let me know what times you're available that day.

Thanks,
Stevie

From danking at ccs.neu.edu  Fri Dec  2 16:42:34 2011
From: danking at ccs.neu.edu (Daniel King)
Date: Fri, 2 Dec 2011 16:42:34 -0500
Subject: [PRL] Second call for scheduling requests for Gary T. Leavens,
	12/7
In-Reply-To: <46CE7199-733D-4190-B1BB-BAD7D58398DD@ccs.neu.edu>
References: <46CE7199-733D-4190-B1BB-BAD7D58398DD@ccs.neu.edu>
Message-ID: <CAEJz2tMAQhmS5ys-9GkAKWMTqtsK-ACt4gQpwkxL6OTCqXz78Q@mail.gmail.com>

On Fri, Dec 2, 2011 at 13:12, Stevie Strickland <sstrickl at ccs.neu.edu> wrote:
> Hi all,
>
> We still have a couple of slots available to talk with Dr. Leavens (http://www.eecs.ucf.edu/~leavens/) next Wednesday (12/7). ?If you're interested, please let me know what times you're available that day.

Me! Me! Me!

-- 
Dan King
College of Computer and Information Science
Northeastern University


From matthias at ccs.neu.edu  Fri Dec  2 18:30:30 2011
From: matthias at ccs.neu.edu (Matthias Felleisen)
Date: Fri, 2 Dec 2011 18:30:30 -0500
Subject: [PRL] Shriram in January
Message-ID: <6080C489-5FDF-44FF-98FD-3081A329CD13@ccs.neu.edu>


I have finally been able to pin down Shriram for a talk here. Mark your calendars for Jan 18. 

As many of you know he applies PL techniques to SE problems
(and does some PL too). I have asked him to present work that
is a bit outside of core PL to get an example of this kind of
work. The abstract is below; the work is sponsored by Cisco 
(and used there) and by Google. 

Shriram said he may bring along his co-authors, which would 
mean a chance to talk to three faculty members while you have
to listen to only one talk. It's a three-for, a real deal, a
steal, a free gift :-) Details when we get closer; I will 
arrange a schedule then. 

-- Matthias





                          Policy Analysis

                       Shriram Krishnamurthi
                          Brown University

Access-control policies control data dissemination in domains from
health-care to social networks.  Similar policies also govern various
aspects of firewalls and routers.

The subtle nature of these policies suggests this is a natural domain
to apply formal methods, while the separate authoring of policies in
domain-specific languages affords opportunities for powerful analysis.
It is, however, unclear that the straightforward application of
verification is appropriate or useful.  The talk will describe our
work on useful forms of input and output, the concrete tools we've
produced, and our increasing use of human cognitive aspects to drive
our next generation of research in this area.

                   http://www.margrave-tool.org/



From sstrickl at ccs.neu.edu  Tue Dec  6 00:26:10 2011
From: sstrickl at ccs.neu.edu (Stevie Strickland)
Date: Tue, 6 Dec 2011 00:26:10 -0500
Subject: [PRL] Current schedule for Gary T. Leavens's visit
Message-ID: <424BD286-19C0-4E32-A90A-57CD4F82964F@ccs.neu.edu>

Here's the current schedule I have for Dr. Leavens's visit on Wednesday.  Please let me know if you notice any issues so I can resolve them ASAP.

10:00 Karl Lieberherr
10:30 Christos Dimoulas
11:00 Dimitris Vardoulakis
11:20 Carl Eastlund
11:40 Setup for talk
11:45 Talk
13:30 Lunch (???, Christos, Carl)
14:30 Amal Ahmed
15:00 Pete Manolios
15:30 Sam Tobin-Hochstadt
16:00 Thomas Wahl
16:30 David Van Horn
17:00 Matthias Felleisen
17:30 Vincent St-Amour
17:45 Stephen Chang
18:00 Paul Stansifer
18:15 Asumu Takikawa

Thanks,
Stevie

From sstrickl at ccs.neu.edu  Tue Dec  6 13:19:13 2011
From: sstrickl at ccs.neu.edu (Stevie Strickland)
Date: Tue, 6 Dec 2011 13:19:13 -0500
Subject: [PRL] Updated schedule for Gary T. Leavens's visit, 12/7
Message-ID: <E54C116F-954A-4EE3-B901-2E9E13E28F2D@ccs.neu.edu>

The only important change is expanding the later slots to provide more time for those students meeting with him then.  If you have an earlier slot, you are unaffected.

10:00 Karl Lieberherr
10:30 Christos Dimoulas
11:00 Dimitris Vardoulakis
11:20 Carl Eastlund
11:40 Setup for talk
11:45 Talk
13:30 Lunch (Sam, Christos, Carl)
14:30 Amal Ahmed
15:00 Pete Manolios
15:30 Sam Tobin-Hochstadt
16:00 Thomas Wahl
16:30 David Van Horn
17:00 Matthias Felleisen
17:15 Vincent St-Amour
17:35 Stephen Chang
17:55 Paul Stansifer
18:15 Asumu Takikawa

Thanks,
Stevie

From wand at ccs.neu.edu  Wed Dec  7 21:22:50 2011
From: wand at ccs.neu.edu (Mitchell Wand)
Date: Wed, 7 Dec 2011 21:22:50 -0500
Subject: [PRL] Please don't use deadbolt as a doorstop
Message-ID: <CAJqwn-_MsSJXrHycFhadcFnej5Oz03oGPp0sVt8r=ec9e6cLQA@mail.gmail.com>

I didn't want to interrupt at today's talk, but please DO NOT use the
deadbolt in 366, or any other room, as a prop to keep the door open.

This damages the lock and pretty quickly results in a door that will
neither open nor close.

This has been a perennial problem in the classroom downstairs.

--Mitch
-------------- next part --------------
HTML attachment scrubbed and removed

From samth at ccs.neu.edu  Wed Dec  7 23:15:32 2011
From: samth at ccs.neu.edu (Sam Tobin-Hochstadt)
Date: Wed, 7 Dec 2011 23:15:32 -0500
Subject: [PRL] PL research meets linux kernel development
Message-ID: <CAK=HD+ZrOX5GTHq3dPcnxYhnk8DJXK+zwb0O7Qm8F+hQR9ML2A@mail.gmail.com>

http://lwn.net/SubscriberLink/470681/594406e5c400e524/

-- 
sam th
samth at ccs.neu.edu


From turon at ccs.neu.edu  Sun Dec 11 15:48:03 2011
From: turon at ccs.neu.edu (Aaron Turon)
Date: Sun, 11 Dec 2011 15:48:03 -0500
Subject: [PRL] Jean Yang's 12/14 visit
Message-ID: <CAGfQ5ashHP-QBF0JBGg-y4DngueLkC1Eq7RtU6J4VZsf5c=Q6A@mail.gmail.com>

On Wednesday (12/14), Jean Yang
(http://people.csail.mit.edu/jeanyang/) will be giving the final
seminar talk for the semester and visiting for the day.  She'd love to
meet with both students and faculty.  Please email me with your
constraints and I'll put together a schedule.

Thanks!

Aaron


From chrdimo at ccs.neu.edu  Tue Dec 13 00:55:55 2011
From: chrdimo at ccs.neu.edu (Christos Dimoulas)
Date: Tue, 13 Dec 2011 00:55:55 -0500
Subject: [PRL] Invitation to Bootstrap WOW!
Message-ID: <4EE6E8EB.20803@ccs.neu.edu>

Hi everyone,

My middle-school students at Orchard Gardens K-8 school completed 
Bootstrap and they are ready to show off their video games!

For this reason Citizens Schools organizes a public performance event at 
the school this Wednesday at 17:30.

It would be really great for the kids if any of you could attend, play 
with their video games and ask them questions.

These students do not get a lot of constructive stimuli from their 
environment and they could benefit a lot from interacting with people 
who have invested on education. In addition talking to people who know 
how to program and thus can ask meaningful questions could make them 
appreciate more their achievement.

The Orchard Gardens K-8 school is pretty close to the department and 
easily accessible with public transportation.
Here is the link from Google maps:
http://maps.google.com/maps?saddr=West+Village+H,+Boston,+Massachusetts+02115&daddr=Orchard+gardens+K8&hl=en&sll=42.33464,-71.08534&sspn=0.009612,0.01929&geocode=FasIhgIdVDfD-ynjpwflIXrjiTGC8ipL3J4SWA%3BFfPphQIdJHHD-ylVBg0WOXrjiTHzqUdfNntASw&vpsrc=0&dirflg=r&ttype=now&noexp=0&noal=0&sort=def&mra=ltm&t=m&z=15&start=2

Thank you very much!

.Christos

-------------- next part --------------
HTML attachment scrubbed and removed

From wand at ccs.neu.edu  Tue Dec 13 08:29:24 2011
From: wand at ccs.neu.edu (Mitchell Wand)
Date: Tue, 13 Dec 2011 08:29:24 -0500
Subject: [PRL] [1112.2396] Decorated proofs for computational effects: States
Message-ID: <CAJqwn-9hsSeYpSDa-q_XxpMQLHtTpS0kHfc+h=tn7WC0=4NRbA@mail.gmail.com>

No clue about content, but interesting abstract...  --MitchDecorated proofs
for computational effects: States
Jean-Guillaume Dumas <http://arxiv.org/find/cs/1/au:+Dumas_J/0/1/0/all/0/1>
 (LJK), Dominique Duval<http://arxiv.org/find/cs/1/au:+Duval_D/0/1/0/all/0/1>
 (LJK), Laurent Fousse<http://arxiv.org/find/cs/1/au:+Fousse_L/0/1/0/all/0/1>
 (LJK), Jean-Claude
Reynaud<http://arxiv.org/find/cs/1/au:+Reynaud_J/0/1/0/all/0/1>
 (RC)
(Submitted on 11 Dec 2011)

The syntax of an imperative language does not mention explicitly the state,
while its denotational semantics has to mention it. In this paper we show
that the equational proofs about an imperative language may hide the state,
in the same way as the syntax does.

Subjects:Programming Languages (cs.PL)Cite
as:arXiv:1112.2396v1<http://arxiv.org/abs/1112.2396v1>
 [cs.PL]

Link: http://arxiv.org/abs/1112.2396 (sent via Shareaholic)

----
-------------- next part --------------
HTML attachment scrubbed and removed

From wand at ccs.neu.edu  Thu Dec 22 11:45:10 2011
From: wand at ccs.neu.edu (Mitchell Wand)
Date: Thu, 22 Dec 2011 11:45:10 -0500
Subject: [PRL] Dependently Typed Programming based on Automated Theorem
 Proving | Lambda the Ultimate
Message-ID: <CAJqwn--iRAy2mTFUx9W=dwgUX3nXkgS4ith+wSu75KHEYoLHaA@mail.gmail.com>

Unread, fwiw.


> Mella is a minimalistic dependently typed programming language and
> interactive theorem prover implemented in Haskell. Its main purpose is to
> investigate the effective integration of automated theorem provers in a
> pure and simple setting. Such integrations are essential for supporting
> program development in dependently typed languages. We integrate the
> equational theorem prover Waldmeister and test it on more than 800 proof
> goals from the TPTP library. In contrast to previous approaches, the
> reconstruction of Waldmeister proofs within Mella is quite robust and does
> not generate a significant overhead to proof search. Mella thus yields a
> template for integrating more expressive theorem provers in more
> sophisticated languages.


http://lambda-the-ultimate.org/node/4423
-------------- next part --------------
HTML attachment scrubbed and removed

From wand at ccs.neu.edu  Thu Dec 22 20:03:42 2011
From: wand at ccs.neu.edu (Mitchell Wand)
Date: Thu, 22 Dec 2011 20:03:42 -0500
Subject: [PRL] [1112.5000] Lazy Pointer Analysis
Message-ID: <CAJqwn-9+-MDJSWtQxFUuJb+r6FgGEWTG25HbYDc41gssi9TxMg@mail.gmail.com>

Lazy Pointer Analysis
Uday P. Khedker <http://arxiv.org/find/cs/1/au:+Khedker_U/0/1/0/all/0/1>, Alan
Mycroft <http://arxiv.org/find/cs/1/au:+Mycroft_A/0/1/0/all/0/1>, Prashant
Singh Rawat <http://arxiv.org/find/cs/1/au:+Rawat_P/0/1/0/all/0/1>
(Submitted on 21 Dec 2011)

Flow- and context-sensitive pointer analysis is generally considered too
expensive for large programs; most tools relax one or both of the
requirements for scalability. We formulate a flow- and context-sensitive
points-to analysis that is lazy in the following sense: points-to
information is computed only for live pointers and its propagation is
sparse (restricted to live ranges of respective pointers). Further, our
analysis (a) uses strong liveness, effectively including dead code
elimination; (b) afterwards calculates must-points-to information from
may-points-to information instead of using a mutual fixed-point; and (c)
uses value-based termination of call strings during interprocedural
analysis (which reduces the number of call strings significantly).
A naive implementation of our analysis within GCC-4.6.0 gave analysis time
and size of points-to measurements for SPEC2006. Using liveness reduced the
amount of points-to information by an order of magnitude with no loss of
precision. For all programs under 30kLoC we found that the results were
much more precise than gcc's analysis. What comes as a pleasant surprise
however, is the fact that below this cross-over point, our naive
linked-list implementation is faster than a flow- and context-insensitive
analysis which is primarily used for efficiency. We speculate that lazy
flow- and context-sensitive analyses may be not only more precise, but also
more efficient, than current approaches.


http://arxiv.org/abs/1112.5000
-------------- next part --------------
HTML attachment scrubbed and removed

From wand at ccs.neu.edu  Thu Dec 22 20:04:46 2011
From: wand at ccs.neu.edu (Mitchell Wand)
Date: Thu, 22 Dec 2011 20:04:46 -0500
Subject: [PRL] [1112.4106] Dependent Types for JavaScript
Message-ID: <CAJqwn-_=xk0eXhPu_WzbSJ8pC2S6Sj=ktLVtHf_sJGT8r4CT5w@mail.gmail.com>

http://arxiv.org/abs/1112.4106

More from Jhala:

Dependent Types for JavaScript
Ravi Chugh <http://arxiv.org/find/cs/1/au:+Chugh_R/0/1/0/all/0/1>, Ranjit
Jhala <http://arxiv.org/find/cs/1/au:+Jhala_R/0/1/0/all/0/1>
(Submitted on 18 Dec 2011)

Dynamic languages like JavaScript, Python, and Ruby feature run-time
tag-tests, higher-order functions, extensible objects, and imperative
updates. In recent work on System D, we showed how to support many of these
features in a functional setting. In this work, we define a new calculus,
System !D (pronounced "D-ref"), that extends the previous one in two ways.
First, we add flow-sensitive heap types to reason about strong updates to
mutable variables. Second, we incorporate heap unrolling and uninterpreted
heap symbols to precisely reason about prototype-based objects. We
demonstrate that System !D is expressive by defining DJS, a large
JavaScript subset that translates to System !D for type checking. Through
several patterns advocated in the popular book JavaScript: The Good Parts,
we show that System !D is a practical typed intermediate language for
real-world, imperative dynamic languages with higher-order functions and
extensible, prototype-based objects.
-------------- next part --------------
HTML attachment scrubbed and removed

From dherman at ccs.neu.edu  Thu Dec 22 20:13:05 2011
From: dherman at ccs.neu.edu (David Herman)
Date: Thu, 22 Dec 2011 17:13:05 -0800
Subject: [PRL] [1112.4106] Dependent Types for JavaScript
In-Reply-To: <CAJqwn-_=xk0eXhPu_WzbSJ8pC2S6Sj=ktLVtHf_sJGT8r4CT5w@mail.gmail.com>
References: <CAJqwn-_=xk0eXhPu_WzbSJ8pC2S6Sj=ktLVtHf_sJGT8r4CT5w@mail.gmail.com>
Message-ID: <EE373C54-849E-49B8-B196-09BF039E81FB@ccs.neu.edu>

Ravi Chugh will be interning with us starting next month to work on types for JS. Hopefully Sam will be able to consult on the project from time to time, too.

Dave

On Dec 22, 2011, at 5:04 PM, Mitchell Wand wrote:

> http://arxiv.org/abs/1112.4106
> 
> More from Jhala:
> 
> Dependent Types for JavaScript
> 
> Ravi Chugh, Ranjit Jhala
> (Submitted on 18 Dec 2011)
> Dynamic languages like JavaScript, Python, and Ruby feature run-time tag-tests, higher-order functions, extensible objects, and imperative updates. In recent work on System D, we showed how to support many of these features in a functional setting. In this work, we define a new calculus, System !D (pronounced "D-ref"), that extends the previous one in two ways. First, we add flow-sensitive heap types to reason about strong updates to mutable variables. Second, we incorporate heap unrolling and uninterpreted heap symbols to precisely reason about prototype-based objects. We demonstrate that System !D is expressive by defining DJS, a large JavaScript subset that translates to System !D for type checking. Through several patterns advocated in the popular book JavaScript: The Good Parts, we show that System !D is a practical typed intermediate language for real-world, imperative dynamic languages with higher-order functions and extensible, prototype-based objects.
> _______________________________________________
> PRL mailing list
> PRL at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/prl

-------------- next part --------------
HTML attachment scrubbed and removed

From matthias at ccs.neu.edu  Thu Dec 22 22:52:55 2011
From: matthias at ccs.neu.edu (Matthias Felleisen)
Date: Thu, 22 Dec 2011 22:52:55 -0500
Subject: [PRL] [1112.4106] Dependent Types for JavaScript
In-Reply-To: <CAJqwn-_=xk0eXhPu_WzbSJ8pC2S6Sj=ktLVtHf_sJGT8r4CT5w@mail.gmail.com>
References: <CAJqwn-_=xk0eXhPu_WzbSJ8pC2S6Sj=ktLVtHf_sJGT8r4CT5w@mail.gmail.com>
Message-ID: <A8DC3859-7D61-47D8-90D3-E1484C991A6D@ccs.neu.edu>


He sure knows how to write marketing prose. 



On Dec 22, 2011, at 8:04 PM, Mitchell Wand wrote:

> http://arxiv.org/abs/1112.4106
> 
> More from Jhala:
> 
> Dependent Types for JavaScript
> 
> Ravi Chugh, Ranjit Jhala
> (Submitted on 18 Dec 2011)
> Dynamic languages like JavaScript, Python, and Ruby feature run-time tag-tests, higher-order functions, extensible objects, and imperative updates. In recent work on System D, we showed how to support many of these features in a functional setting. In this work, we define a new calculus, System !D (pronounced "D-ref"), that extends the previous one in two ways. First, we add flow-sensitive heap types to reason about strong updates to mutable variables. Second, we incorporate heap unrolling and uninterpreted heap symbols to precisely reason about prototype-based objects. We demonstrate that System !D is expressive by defining DJS, a large JavaScript subset that translates to System !D for type checking. Through several patterns advocated in the popular book JavaScript: The Good Parts, we show that System !D is a practical typed intermediate language for real-world, imperative dynamic languages with higher-order functions and extensible, prototype-based objects.
> _______________________________________________
> PRL mailing list
> PRL at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/prl

-------------- next part --------------
HTML attachment scrubbed and removed

From wand at ccs.neu.edu  Fri Dec 23 14:53:44 2011
From: wand at ccs.neu.edu (Mitchell Wand)
Date: Fri, 23 Dec 2011 14:53:44 -0500
Subject: [PRL] Found door to 308 propped open
Message-ID: <CAJqwn-9LaLvqNLmZ-K9s0Xjn7u9-6pzFMWiBX5fQBw4fWbqbgg@mail.gmail.com>

I just found the door to 308 propped open using the deadbolt.  This is a
bad thing.

1.  Things could get stolen
2.  The latches on these doors are delicate, and if they are propped open
using the deadbolt, pretty soon the entire latch stops working, and the
door can neither be closed nor opened.

Please don't do this.

--Mitch
-------------- next part --------------
HTML attachment scrubbed and removed

From mwand1 at gmail.com  Fri Dec 30 07:47:42 2011
From: mwand1 at gmail.com (Mitch)
Date: Fri, 30 Dec 2011 12:47:42 +0000
Subject: [PRL] Semantics and Algorithms for Parametric Monitoring.
 (arXiv:1112.5761v1 [cs.PL])
Message-ID: <20cf3071cfc686cd7704b54ea38b@google.com>

Possibly of interest?

Sent to you by Mitch via Google Reader: Semantics and Algorithms for
Parametric Monitoring. (arXiv:1112.5761v1 [cs.PL]) via cs.PL updates on
arXiv.org by <a
href="http://arxiv.org/find/cs/1/au:+Rosu_G/0/1/0/all/0/1">Grigore
Rosu</a>, <a
href="http://arxiv.org/find/cs/1/au:+Chen_F/0/1/0/all/0/1">Feng
Chen</a> on 12/29/11

Analysis of execution traces plays a fundamental role in many program
analysis approaches, such as runtime verification, testing, monitoring,
and specification mining. Execution traces are frequently parametric,
i.e., they contain events with parameter bindings. Each parametric
trace usually consists of many meaningful trace slices merged together,
each slice corresponding to one parameter binding. This gives a
semantics-based solution to parametric trace analysis. A
general-purpose parametric trace slicing technique is introduced, which
takes each event in the parametric trace and dispatches it to its
corresponding trace slices. This parametric trace slicing technique can
be used in combination with any conventional, non-parametric trace
analysis technique, by applying the later on each trace slice. As an
instance, a parametric property monitoring technique is then presented.
The presented parametric trace slicing and monitoring techniques have
been implemented and extensively evaluated. Measurements of runtime
overhead confirm that the generality of the discussed techniques does
not come at a performance expense when compared with existing
parametric trace monitoring systems.

Things you can do from here:
- Subscribe to cs.PL updates on arXiv.org using Google Reader
- Get started using Google Reader to easily keep up with all your
favorite sites
-------------- next part --------------
HTML attachment scrubbed and removed