From dvanhorn at ccs.neu.edu Wed Jan 4 13:23:05 2012 From: dvanhorn at ccs.neu.edu (David Van Horn) Date: Wed, 04 Jan 2012 13:23:05 -0500 Subject: [PRL] What is it like to have an understanding of very advanced X? Message-ID: <4F049909.8060906@ccs.neu.edu> This seems applicable beyond just math: http://www.quora.com/What-is-it-like-to-have-an-understanding-of-very-advanced-mathematics David From dherman at ccs.neu.edu Wed Jan 4 21:00:27 2012 From: dherman at ccs.neu.edu (David Herman) Date: Thu, 5 Jan 2012 03:00:27 +0100 Subject: [PRL] What is it like to have an understanding of very advanced X? In-Reply-To: <4F049909.8060906@ccs.neu.edu> References: <4F049909.8060906@ccs.neu.edu> Message-ID: On Jan 4, 2012, at 7:23 PM, David Van Horn wrote: > This seems applicable beyond just math: > > http://www.quora.com/What-is-it-like-to-have-an-understanding-of-very-advanced-mathematics Awesome! And the anonymous respondent also linked to this very nice blog post from Terry Tao, which I'd not seen before: http://terrytao.wordpress.com/career-advice/there%E2%80%99s-more-to-mathematics-than-rigour-and-proofs/ Dave From clements at brinckerhoff.org Wed Jan 4 21:10:43 2012 From: clements at brinckerhoff.org (John Clements) Date: Wed, 4 Jan 2012 18:10:43 -0800 Subject: [PRL] What is it like to have an understanding of very advanced X? In-Reply-To: References: <4F049909.8060906@ccs.neu.edu> Message-ID: <9827A4EB-5BB5-4F56-8830-DC3FE7DE81DA@brinckerhoff.org> On Jan 4, 2012, at 6:00 PM, David Herman wrote: > On Jan 4, 2012, at 7:23 PM, David Van Horn wrote: > >> This seems applicable beyond just math: >> >> http://www.quora.com/What-is-it-like-to-have-an-understanding-of-very-advanced-mathematics > > Awesome! +1. John -------------- next part -------------- A non-text attachment was scrubbed... Name: smime.p7s Type: application/pkcs7-signature Size: 4624 bytes Desc: not available Url : http://lists.ccs.neu.edu/pipermail/prl/attachments/20120104/f8392fcc/attachment.bin From mwand1 at gmail.com Mon Jan 9 07:04:27 2012 From: mwand1 at gmail.com (Mitch) Date: Mon, 09 Jan 2012 12:04:27 +0000 Subject: [PRL] Abstracting Runtime Heaps for Program Understanding. (arXiv:1201.1327v1 [cs.... Message-ID: <20cf30780ad0475b3704b6173397@google.com> Sent to you by Mitch via Google Reader: Abstracting Runtime Heaps for Program Understanding. (arXiv:1201.1327v1 [cs.PL]) via cs.PL updates on arXiv.org by Mark Marron, Cesar Sanchez, Zhendong Su, Manuel Fahndrich on 1/8/12 Modern programming environments provide extensive support for inspecting, analyzing, and testing programs based on the algorithmic structure of a program. Unfortunately, support for inspecting and understanding runtime data structures during execution is typically much more limited. This paper provides a general purpose technique for abstracting and summarizing entire runtime heaps. We describe the abstract heap model and the associated algorithms for transforming a concrete heap dump into the corresponding abstract model as well as algorithms for merging, comparing, and computing changes between abstract models. The abstract model is designed to emphasize high-level concepts about heap-based data structures, such as shape and size, as well as relationships between heap structures, such as sharing and connectivity. We demonstrate the utility and computational tractability of the abstract heap model by building a memory profiler. We then use this tool to check for, pinpoint, and correct sources of memory bloat from a suite of programs from DaCapo. 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 wand at ccs.neu.edu Tue Jan 10 10:41:46 2012 From: wand at ccs.neu.edu (Mitchell Wand) Date: Tue, 10 Jan 2012 10:41:46 -0500 Subject: [PRL] Fwd: [MIT-PL] 1/20: Ben Livshits on multi-execution In-Reply-To: References: Message-ID: ---------- Forwarded message ---------- From: Jean Yang Date: Tue, Jan 10, 2012 at 10:29 AM Subject: [MIT-PL] 1/20: Ben Livshits on multi-execution To: pl at lists.csail.mit.edu Cc: Sally Lee Hi all, Next Friday we will have the pleasure of hearing Ben Livshits from Microsoft Research speak about his work on multi-execution. Hope to see you there. Jean --- Title: Multi-execution as an alternative to symbolic execution Time: 2:30-3:30pm; refreshments at 2:15 Location: 32-G882 (8th floor reading room) This talk will cover out recent work that explores multi-execution techniques as an alternative to both static analysis and symbolic execution. Our primary application is detection or malware-hosting pages on the web. In recent years, attacks that exploit vulnerabilities in browsers and their associated plugins have increased significantly. These attacks are often written in JavaScript and literally millions of URLs contain such malicious content. While static and runtime methods for malware detection been proposed in the literature, both on the client side, for just-in-time in-browser detection, as well as offline, crawler-based malware discovery, these approaches encounter the same fundamental limitation. Web-based malware tends to be environment-specific, targeting a particular browser, often attacking specific versions of installed plugins. This targeting occurs because the malware exploits vulnerabilities in specific plugins and fail otherwise. As a result, a fundamental limitation for detecting a piece of malware is that malware is triggered infrequently, only showing itself when the right environment is present. In fact, we observe that using current fingerprinting techniques, just about any piece of existing malware may be made virtually undetectable with the current generation of malware scanners. We propose Rozzle, a JavaScript multi-execution virtual machine, as a way to explore multiple execution paths within a single execution so that environment-specific malware will reveal itself. Using large-scale experiments, we show that Rozzle increases the detection rate for offline runtime detection by almost seven times. In addition, Rozzle triples the effectiveness of online runtime detection. We show that Rozzle incurs virtually no runtime overhead and allows us to replace multiple VMs running different browser configurations with a single Rozzle-enabled browser, reducing the hardware requirements, network bandwidth, and power consumption. --- Biography: Ben Livshits is a researcher at Microsoft Research in Redmond, WA and an affiliate professor at the University of Washington. Originally from St. Petersburg, Russia, he received a bachelor's degree in Computer Science and Math from Cornell University in 1999, and his M.S. and Ph.D. in Computer Science from Stanford University in 2002 and 2006, respectively. Dr. Livshits' research interests include application of sophisticated static and dynamic analysis techniques to finding errors in programs. Ben has published papers at PLDI, POPL, Oakland Security, Usenix Security, CCS, SOSP, ICSE, FSE, and many other venues. He is known for his work in software reliability and especially tools to improve software security, with a primary focus on approaches to finding buffer overruns in C programs and a variety of security vulnerabilities (cross-site scripting, SQL injections, etc.) in Web-based applications. He is the author of several dozen academic papers and patents. Lately he has been focusing on how Web 2.0 application and browser reliability, performance, and security can be improved through a combination of static and runtime techniques. Ben generally does not speak of himself in the third person. http://research.microsoft.com/~livshits/ -- Jean Yang http://people.csail.mit.edu/jeanyang _______________________________________________ Pl mailing list Pl at lists.csail.mit.edu https://lists.csail.mit.edu/mailman/listinfo/pl http://projects.csail.mit.edu/pl -------------- next part -------------- HTML attachment scrubbed and removed From turon at ccs.neu.edu Wed Jan 11 11:22:37 2012 From: turon at ccs.neu.edu (Aaron Turon) Date: Wed, 11 Jan 2012 11:22:37 -0500 Subject: [PRL] Derek Dreyer's visit Message-ID: Derek Dreyer (http://www.mpi-sws.org/~dreyer/research.html) will be visiting next week, and giving a talk on Thu 1/19. I am proposing to hold the talk at: ** Thu 1/19, 1:30-3pm ** Please let me know ASAP if this time will not work for you. Derek will also have some (limited) time for meetings while he's here. If you'd like to meet with him on Thursday or Friday, please email me and I will arrange the details. I will give preference to those whose research is most closely related to Derek's. Cheers, Aaron From matthias at ccs.neu.edu Wed Jan 11 11:39:45 2012 From: matthias at ccs.neu.edu (Matthias Felleisen) Date: Wed, 11 Jan 2012 11:39:45 -0500 Subject: [PRL] shriram and dan/kathi Message-ID: Next Wednesday (1/18) we will have Shriram, Dan Dougherty and Kathi Fisler visiting the lab. Shriram will speak but DD and KF will also be available for 1-1 meetings. After discussing this with Shriram in detail, SK will be available separately from DD/KF who come as a pair. If you would like to meet with either SK and/or DD/KF, please let me know which times you cannot meet with them. Right now, I am counting on meetings from 2:30 through 6:30pm. I will try to allocate time slots in the morning, if there is enough demand. Abstract appeared on pl-seminar and is appended below. -- Matthias --------------------------------------------------------------------- Policy Analysis, an Application of Programming Language Technology 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. --------------------------------------------------------------------- From stamourv at ccs.neu.edu Thu Jan 12 17:32:08 2012 From: stamourv at ccs.neu.edu (Vincent St-Amour) Date: Thu, 12 Jan 2012 17:32:08 -0500 Subject: [PRL] Torture Chamber: Monday, 2:00 PM, WVH 366 Message-ID: <87boq8zh5j.wl%stamourv@ccs.neu.edu> I will be holding a torture chamber for my upcoming PADL talk, "Typing the Numeric Tower" This will be on Monday at 2:00 in 366. Vincent From stamourv at ccs.neu.edu Mon Jan 16 12:17:37 2012 From: stamourv at ccs.neu.edu (Vincent St-Amour) Date: Mon, 16 Jan 2012 12:17:37 -0500 Subject: [PRL] Torture Chamber: Monday, 2:00 PM, WVH 366 In-Reply-To: <87boq8zh5j.wl%stamourv@ccs.neu.edu> References: <87boq8zh5j.wl%stamourv@ccs.neu.edu> Message-ID: <8739bfzhvy.wl%stamourv@ccs.neu.edu> Just a reminder. I'm holding a torture chamber today at 2. Vincent At Thu, 12 Jan 2012 17:32:08 -0500, Vincent St-Amour wrote: > > I will be holding a torture chamber for my upcoming PADL talk, "Typing > the Numeric Tower" > > This will be on Monday at 2:00 in 366. > > Vincent > > _______________________________________________ > PRL mailing list > PRL at lists.ccs.neu.edu > https://lists.ccs.neu.edu/bin/listinfo/prl From dherman at ccs.neu.edu Mon Jan 16 19:25:06 2012 From: dherman at ccs.neu.edu (David Herman) Date: Mon, 16 Jan 2012 16:25:06 -0800 Subject: [PRL] sound familiar? Message-ID: http://programmingzen.com/2012/01/16/on-the-usability-of-codecademy/ Dave From matthias at ccs.neu.edu Wed Jan 18 08:32:58 2012 From: matthias at ccs.neu.edu (Matthias Felleisen) Date: Wed, 18 Jan 2012 08:32:58 -0500 Subject: [PRL] reminder: Policy Analysis, an Application of Programming Language Technology Message-ID: <14FF3F54-D646-4DAD-9B10-48F24D22F875@ccs.neu.edu> Today's NUPRL Colloquium: --------------------------------------------------------------------- Policy Analysis, an Application of Programming Language Technology 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. --------------------------------------------------------------------- Time: 11:45am, Place: WVH 366 From sstrickl at ccs.neu.edu Thu Jan 19 08:33:11 2012 From: sstrickl at ccs.neu.edu (Stevie Strickland) Date: Thu, 19 Jan 2012 08:33:11 -0500 Subject: [PRL] Door to 308 was propped open when I arrived Message-ID: When I came into 308 this morning, the door had been propped open with the doorstop. Kudos for not propping it open with the deadbolt, but since no one's come back to the lab 20 minutes later, I assume that it's been left open all night. While I appreciate that it's annoying sometimes to pull out your keycard, please don't leave the lab open, even temporarily, if there's no one else around. Also, if you're leaving the lab and notice that the door's propped open with no one inside, please close it even if you're not the person who opened it. Thanks, Stevie From sstrickl at ccs.neu.edu Thu Jan 19 10:51:20 2012 From: sstrickl at ccs.neu.edu (Stevie Strickland) Date: Thu, 19 Jan 2012 10:51:20 -0500 Subject: [PRL] Fwd: Door to 308 was propped open when I arrived References: <4365BA2D-482A-4D51-8484-6876D959CBF1@gmail.com> Message-ID: Begin forwarded message: > From: Ahmed Abdelmeged > Subject: Re: [PRL] Door to 308 was propped open when I arrived > Date: January 19, 2012 10:44:06 AM EST > To: Stevie Strickland > > Stevie, > I turned off the lights yesterday myself. At that time the door was locked. I think that the person who did that must have come later at night. Probably one of the janitors. This hypothesis is further supported by that janitors are unlikely to read emails on this list. Consequently, they are likely to keep doing what the audience of PRL would consider wrong. > > Plz forward to prl. > > -- Ahmed > > On 2012-01-19, at 8:33 AM, Stevie Strickland wrote: > >> When I came into 308 this morning, the door had been propped open with the doorstop. Kudos for not propping it open with the deadbolt, but since no one's come back to the lab 20 minutes later, I assume that it's been left open all night. While I appreciate that it's annoying sometimes to pull out your keycard, please don't leave the lab open, even temporarily, if there's no one else around. Also, if you're leaving the lab and notice that the door's propped open with no one inside, please close it even if you're not the person who opened it. >> >> Thanks, >> Stevie >> _______________________________________________ >> PRL mailing list >> PRL at lists.ccs.neu.edu >> https://lists.ccs.neu.edu/bin/listinfo/prl >> From mwand1 at gmail.com Mon Jan 23 06:58:42 2012 From: mwand1 at gmail.com (Mitch) Date: Mon, 23 Jan 2012 11:58:42 +0000 Subject: [PRL] Secondary use of data in EHR systems. (arXiv:1201.4262v1 [cs.PL]) Message-ID: <20cf3071cfc67fac9604b730c0a2@google.com> Hmm, AOP, security, analysis, continuations, interesting authors. Sent to you by Mitch via Google Reader: Secondary use of data in EHR systems. (arXiv:1201.4262v1 [cs.PL]) via cs.PL updates on arXiv.org by Fan Yang, Chris Hankin, Flemming Nielson, Hanne Riis Nielson on 1/22/12 We show how to use aspect-oriented programming to separate security and trust issues from the logical design of mobile, distributed systems. The main challenge is how to enforce various types of security policies, in particular predictive access control policies - policies based on the future behavior of a program. A novel feature of our approach is that advice is able to analyze the future use of data. We consider a number of different security policies, concerning both primary and secondary use of data, some of which can only be enforced by analysis of process continuations. 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 mwand1 at gmail.com Tue Jan 31 07:58:25 2012 From: mwand1 at gmail.com (Mitch) Date: Tue, 31 Jan 2012 12:58:25 +0000 Subject: [PRL] On the realizability of contracts in dishonest systems. (arXiv:1201.6188v1 [... Message-ID: <20cf307d06a4ceb43a04b7d284ad@google.com> Sent to you by Mitch via Google Reader: On the realizability of contracts in dishonest systems. (arXiv:1201.6188v1 [cs.PL]) via cs.PL updates on arXiv.org by Massimo Bartoletti, Emilio Tuosto, Roberto Zunino on 1/30/12 We develop a theory of contracting systems, where behavioural contracts may be violated by dishonest participants after they have been agreed upon - unlike in traditional approaches based on behavioural types. We consider the contracts of \cite{CastagnaPadovaniGesbert09toplas}, and we embed them in a calculus that allows distributed participants to advertise contracts, reach agreements, query the fulfilment of contracts, and realise them (or choose not to). Our contract theory makes explicit who is culpable at each step of a computation. A participant is honest in a given context S when she is not culpable in each possible interaction with S. Our main result is a sufficient criterion for classifying a participant as honest in all possible contexts. 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 matthias at ccs.neu.edu Tue Jan 31 08:16:47 2012 From: matthias at ccs.neu.edu (Matthias Felleisen) Date: Tue, 31 Jan 2012 08:16:47 -0500 Subject: [PRL] On the realizability of contracts in dishonest systems. (arXiv:1201.6188v1 [... In-Reply-To: <20cf307d06a4ceb43a04b7d284ad@google.com> References: <20cf307d06a4ceb43a04b7d284ad@google.com> Message-ID: <0B2322A2-C339-4D76-862D-6F72191018C4@ccs.neu.edu> Their notion of 'behavioral contract' is about [non-functional] protocol specifications, quite different from the behavioral contracts of Eiffel and friends. On Jan 31, 2012, at 7:58 AM, Mitch wrote: > > > Sent to you by Mitch via Google Reader: > > > On the realizability of contracts in dishonest systems. (arXiv:1201.6188v1 [cs.PL]) > via cs.PL updates on arXiv.org by Massimo Bartoletti, Emilio Tuosto, Roberto Zunino on 1/30/12 > We develop a theory of contracting systems, where behavioural contracts may be violated by dishonest participants after they have been agreed upon - unlike in traditional approaches based on behavioural types. We consider the contracts of \cite{CastagnaPadovaniGesbert09toplas}, and we embed them in a calculus that allows distributed participants to advertise contracts, reach agreements, query the fulfilment of contracts, and realise them (or choose not to). > > Our contract theory makes explicit who is culpable at each step of a computation. A participant is honest in a given context S when she is not culpable in each possible interaction with S. Our main result is a sufficient criterion for classifying a participant as honest in all possible contexts. > > > > > 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 > > > _______________________________________________ > 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 turon at ccs.neu.edu Tue Jan 31 11:46:37 2012 From: turon at ccs.neu.edu (Aaron Turon) Date: Tue, 31 Jan 2012 11:46:37 -0500 Subject: [PRL] POPL recap: Wednesday Message-ID: A heads-up: we are planning to hold a POPL recap session tomorrow (Wednesday). The exact schedule is TBD, but will most likely be during the standard 1145 seminar slot. I'll send out another email as soon as I know for sure. From dougorleans at gmail.com Tue Jan 31 12:39:28 2012 From: dougorleans at gmail.com (Doug Orleans) Date: Tue, 31 Jan 2012 12:39:28 -0500 Subject: [PRL] Palindromic programs Message-ID: This morning I wondered what the longest (ignoring whitespace) palindromic Racket program was. Obviously any palindromic integer is a program, but that's not too interesting. There's also "(quote etouq)" but I couldn't think of a good way to extend that. Then I came up with this: (letrec ((letrec letrec) (certel certel)) certel) This can be extended indefinitely: (letrec ((letrec letrec) (gateman stressed) (nametag desserts) (stressed gateman) (desserts nametag) (certel certel)) certel) These just return #, though. Is there a palindromic program that actually does something interesting? --Doug P.S. Here's a palindromic quine in C: http://www.derf.net/palindromes/old.palindrome.html#CODE From will at ccs.neu.edu Tue Jan 31 15:17:56 2012 From: will at ccs.neu.edu (will at ccs.neu.edu) Date: Tue, 31 Jan 2012 15:17:56 -0500 (EST) Subject: [PRL] Palindromic programs In-Reply-To: <7994539.260101328040660721.JavaMail.root@zimbra> Message-ID: <27041124.260341328041076290.JavaMail.root@zimbra> Doug Orleans wrote: > These just return #, though. Is there a palindromic > program that actually does something interesting? Possibly. Here's an idea that should be generalizable: ((lambda (lambda adbmal x) adbmal) (+) (+) (lambda (x lambda adbmal) adbmal)) Will From turon at ccs.neu.edu Tue Jan 31 15:40:23 2012 From: turon at ccs.neu.edu (Aaron Turon) Date: Tue, 31 Jan 2012 15:40:23 -0500 Subject: [PRL] POPL recap: ** NOW THURSDAY ** Message-ID: Unfortunately, it was not possible to move around class schedules to do the recap on Wednesday. Instead, we will hold in on: Thursday, Feb 2, WVH366 from 1:45-3pm (the same as Derek's talk) Please join us for what should be a very fun recap session! On Tue, Jan 31, 2012 at 11:46 AM, Aaron Turon wrote: > A heads-up: we are planning to hold a POPL recap session tomorrow > (Wednesday). ?The exact schedule is TBD, but will most likely be > during the standard 1145 seminar slot. ?I'll send out another email as > soon as I know for sure. From dougorleans at gmail.com Tue Jan 31 16:48:35 2012 From: dougorleans at gmail.com (Doug Orleans) Date: Tue, 31 Jan 2012 16:48:35 -0500 Subject: [PRL] Palindromic programs In-Reply-To: <27041124.260341328041076290.JavaMail.root@zimbra> References: <7994539.260101328040660721.JavaMail.root@zimbra> <27041124.260341328041076290.JavaMail.root@zimbra> Message-ID: On Tue, Jan 31, 2012 at 3:17 PM, wrote: > Doug Orleans wrote: >> These just return #, though. ?Is there a palindromic >> program that actually does something interesting? > > Possibly. ?Here's an idea that should be generalizable: > > ((lambda (lambda adbmal x) adbmal) > ?(+) > ?(+) > ?(lambda (x lambda adbmal) adbmal)) Very nice! I just realized we're fudging the definition of 'palindrome' to allow parenthesis reversal... --Doug From turon at ccs.neu.edu Sun Feb 5 22:23:32 2012 From: turon at ccs.neu.edu (Aaron Turon) Date: Sun, 5 Feb 2012 22:23:32 -0500 Subject: [PRL] Mike Dodds's visit Message-ID: Mike Dodds (http://www.cl.cam.ac.uk/~md466/) will be visiting the lab this week, on Tuesday 2/7. Mike has done work on manual and automatic verification of concurrent programs and data structures, and has also worked on automatic parallelization. He'll be giving a talk on some very neat work called "deny-guarantee reasoning" -- the announcement should go early tomorrow. Please let me know if you'd like to meet with Mike on Tuesday. He'll be in the lab for the full day. Thanks, Aaron From samth at ccs.neu.edu Sun Feb 5 22:26:09 2012 From: samth at ccs.neu.edu (Sam Tobin-Hochstadt) Date: Sun, 5 Feb 2012 22:26:09 -0500 Subject: [PRL] Mike Dodds's visit In-Reply-To: References: Message-ID: I'd love to meet with Mike. On Sun, Feb 5, 2012 at 10:23 PM, Aaron Turon wrote: > Mike Dodds (http://www.cl.cam.ac.uk/~md466/) will be visiting the lab > this week, on Tuesday 2/7. ?Mike has done work on manual and automatic > verification of concurrent programs and data structures, and has also > worked on automatic parallelization. ?He'll be giving a talk on some > very neat work called "deny-guarantee reasoning" -- the announcement > should go early tomorrow. > > Please let me know if you'd like to meet with Mike on Tuesday. ?He'll > be in the lab for the full day. > > Thanks, > > Aaron > > _______________________________________________ > PRL mailing list > PRL at lists.ccs.neu.edu > https://lists.ccs.neu.edu/bin/listinfo/prl -- sam th samth at ccs.neu.edu From turon at ccs.neu.edu Wed Feb 8 17:50:11 2012 From: turon at ccs.neu.edu (Aaron Turon) Date: Wed, 8 Feb 2012 17:50:11 -0500 Subject: [PRL] Matthew Fluet on Friday 2/10 Message-ID: Matthew Fluet (http://www.cs.rit.edu/~mtf/) will be here on Friday, 2/10 for Jesse's defense. He'll have some time (not tons) for meeting with students or faculty during the rest of the day. If you're interested, please let me know and give me your scheduling constraints. From asumu at ccs.neu.edu Sat Feb 18 10:58:14 2012 From: asumu at ccs.neu.edu (Asumu Takikawa) Date: Sat, 18 Feb 2012 10:58:14 -0500 Subject: [PRL] Julia: new language for scientific computing Message-ID: <20120218155814.GZ11124@howl.undo.it> http://julialang.org/blog/2012/02/why-we-created-julia/ Heavily inspired by Lisp, but aimed at scientific computation. It has macros for a non-sexpression syntax (no real hygiene though). Cheers, Asumu From dimvar at ccs.neu.edu Sat Feb 18 13:03:03 2012 From: dimvar at ccs.neu.edu (Dimitris Vardoulakis) Date: Sat, 18 Feb 2012 13:03:03 -0500 Subject: [PRL] Julia: new language for scientific computing In-Reply-To: <20120218155814.GZ11124@howl.undo.it> References: <20120218155814.GZ11124@howl.undo.it> Message-ID: Looks pretty neat, thanks for sharing! I really like how they allow you to name the cores and decide where to send data to. The gradual type system also looks interesting (I couldn't seem to find any discussion of type checking or type inference in the manual though). On Sat, Feb 18, 2012 at 10:58 AM, Asumu Takikawa wrote: > http://julialang.org/blog/2012/02/why-we-created-julia/ > > Heavily inspired by Lisp, but aimed at scientific computation. It has > macros for a non-sexpression syntax (no real hygiene though). > > Cheers, > Asumu > > _______________________________________________ > PRL mailing list > PRL at lists.ccs.neu.edu > https://lists.ccs.neu.edu/bin/listinfo/prl -- Dimitris From mwand1 at gmail.com Sat Feb 25 09:02:47 2012 From: mwand1 at gmail.com (Mitch) Date: Sat, 25 Feb 2012 14:02:47 +0000 Subject: [PRL] An Exercise in Invariant-based Programming with Interactive and Automatic Th... Message-ID: fwiw... Sent to you by Mitch via Google Reader: An Exercise in Invariant-based Programming with Interactive and Automatic Theorem Prover Support. (arXiv:1202.4829v1 [cs.LO]) via cs.PL updates on arXiv.org by Ralph-Johan Back (?bo Akademi University), Johannes Eriksson (?bo Akademi University) on 2/22/12 Invariant-Based Programming (IBP) is a diagram-based correct-by-construction programming methodology in which the program is structured around the invariants, which are additionally formulated before the actual code. Socos is a program construction and verification environment built specifically to support IBP. The front-end to Socos is a graphical diagram editor, allowing the programmer to construct invariant-based programs and check their correctness. The back-end component of Socos, the program checker, computes the verification conditions of the program and tries to prove them automatically. It uses the theorem prover PVS and the SMT solver Yices to discharge as many of the verification conditions as possible without user interaction. In this paper, we first describe the Socos environment from a user and systems level perspective; we then exemplify the IBP workflow by building a verified implementation of heapsort in Socos. The case study highlights the role of both automatic and interactive theorem proving in three sequential stages of the IBP workflow: developing the background theory, formulating the program specification and invariants, and proving the correctness of the final implementation. 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 mwand1 at gmail.com Sat Feb 25 09:06:49 2012 From: mwand1 at gmail.com (Mitch) Date: Sat, 25 Feb 2012 14:06:49 +0000 Subject: [PRL] Automated Generation of User Guidance by Combining Computation and Deduction... Message-ID: <20cf307f34926ea1f704b9ca635e@google.com> FYI: I post these if the abstract suggests there's even some vague connection to something we're interested in. Feel free to hit "delete". Sent to you by Mitch via Google Reader: Automated Generation of User Guidance by Combining Computation and Deduction. (arXiv:1202.4832v1 [cs.LO]) via cs.PL updates on arXiv.org by Walther Neuper on 2/22/12 Herewith, a fairly old concept is published for the first time and named "Lucas Interpretation". This has been implemented in a prototype, which has been proved useful in educational practice and has gained academic relevance with an emerging generation of educational mathematics assistants (EMA) based on Computer Theorem Proving (CTP). Automated Theorem Proving (ATP), i.e. deduction, is the most reliable technology used to check user input. However ATP is inherently weak in automatically generating solutions for arbitrary problems in applied mathematics. This weakness is crucial for EMAs: when ATP checks user input as incorrect and the learner gets stuck then the system should be able to suggest possible next steps. The key idea of Lucas Interpretation is to compute the steps of a calculation following a program written in a novel CTP-based programming language, i.e. computation provides the next steps. User guidance is generated by combining deduction and computation: the latter is performed by a specific language interpreter, which works like a debugger and hands over control to the learner at breakpoints, i.e. tactics generating the steps of calculation. The interpreter also builds up logical contexts providing ATP with the data required for checking user input, thus combining computation and deduction. The paper describes the concepts underlying Lucas Interpretation so that open questions can adequately be addressed, and prerequisites for further work are provided. 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 wand at ccs.neu.edu Sat Feb 25 13:08:16 2012 From: wand at ccs.neu.edu (Mitchell Wand) Date: Sat, 25 Feb 2012 13:08:16 -0500 Subject: [PRL] Fwd: Google is Hiring PhDs! In-Reply-To: <20120224075959.D902B5C00E8@hpza9.eem.corp.google.com> References: <20120224075959.D902B5C00E8@hpza9.eem.corp.google.com> Message-ID: Down with the old Borg, up with the new Borg! ---------- Forwarded message ---------- From: Zoanna Jones Date: Fri, Feb 24, 2012 at 2:59 AM Subject: Google is Hiring PhDs! To: wand at ccs.neu.edu *Hello Mitchell, Google strongly believes that PhDs play a pivotal role in tackling global problems by asking the questions and building the tools that create or improve products which help make sense of all the world's information. We?re always looking for the best and the brightest PhD students to fill our technical roles, and we often rely on university faculty to let us know who the top students are in their programs. As a valued member of the Northeastern community, we'd like to ask for your help in identifying top students who are looking for full-time or internship positions this year. If you are interested in referring a PhD student at your university for a position at Google, please complete this form. Members of the Google University Programs team will regularly review these submissions, and follow up with interviews for eligible candidates. To learn more about the challenges that PhDs at Google are tackling, please visit research.google.com. I?ve also included an email announcement below my signature that you can forward on to your PhD students that highlights the current roles we?re recruiting for. If you have questions, or would like to follow up on the status of a previously referred student, please don't hesitate to reach out! Thanks, Zoanna -------------------------------- Are you graduating in 2012? Still looking for a full-time opportunity? Google is looking for the best and brightest computer science students from Northeastern! Interested in joining the company Fortune & CNN ranked the #1 place to work? Check out and apply for our full-time PhD opportunities at http://www.google.com/jobs/students/tech/phd/. There are many opportunities for PhDsat Google to make immediate impact and work on real problems. Google strives to provide an environment of on-going learning where advanced technical development and innovation are the priorities. Our engineers are also encouraged to make contributions to the computer science community through a variety of professional development activities, such as attending conferences, publishing papers , open source, and more. Check out more on our Research at Google page . Not graduating this year? We are also hiring PhD interns for summer 2012. Apply directly to the PhD internship posting - Software Engineering Intern, PhD, Summer - North America Locations. We?ll be reviewing applications on a rolling basis. Stay in touch with new programs and announcements by following us on our Google Students +Page !* -------------- next part -------------- HTML attachment scrubbed and removed From wand at ccs.neu.edu Thu Mar 1 10:02:12 2012 From: wand at ccs.neu.edu (Mitchell Wand) Date: Thu, 1 Mar 2012 10:02:12 -0500 Subject: [PRL] Pitching: The first 8 words - Global Business Hub - Boston.com Message-ID: Probably good advice for other kinds of talks, too.. http://www.boston.com/business/blogs/global-business-hub/2012/02/the_first_8_wor.html?p1=Well_MostPop_Emailed5 -------------- next part -------------- HTML attachment scrubbed and removed From chrdimo at ccs.neu.edu Tue Mar 13 10:01:52 2012 From: chrdimo at ccs.neu.edu (Christos Dimoulas) Date: Tue, 13 Mar 2012 10:01:52 -0400 Subject: [PRL] ESOP Torture chamber Thursday March 15 13:00-14:00 @ 366 Message-ID: <4F5F5350.2070202@ccs.neu.edu> Hi everyone, I am planning to have a torture chamber for my upcoming ESOP talk this Thursday from 13:00 to 14:00 at 366. I would be grateful if you could attend and give me your feedback. Thank you. .Christos From chrdimo at ccs.neu.edu Wed Mar 14 17:14:26 2012 From: chrdimo at ccs.neu.edu (Christos Dimoulas) Date: Wed, 14 Mar 2012 17:14:26 -0400 Subject: [PRL] *** NEW TIME *** ESOP Torture chamber Thursday March 15 13:45-15:00 @ 366 In-Reply-To: <4F5F5350.2070202@ccs.neu.edu> References: <4F5F5350.2070202@ccs.neu.edu> Message-ID: <4F610A32.6090802@ccs.neu.edu> We will have to move the talk a little bit later to avoid a conflict with Sam's class. The new time is 13:45. I have the room until 15:00. Thanks. On 3/13/12 10:01 AM, Christos Dimoulas wrote: > Hi everyone, > > I am planning to have a torture chamber for my upcoming ESOP talk this > Thursday from 13:00 to 14:00 at 366. > > I would be grateful if you could attend and give me your feedback. > > Thank you. > > .Christos > > > _______________________________________________ > PRL mailing list > PRL at lists.ccs.neu.edu > https://lists.ccs.neu.edu/bin/listinfo/prl From stchang at ccs.neu.edu Mon Mar 19 14:36:37 2012 From: stchang at ccs.neu.edu (Stephen Chang) Date: Mon, 19 Mar 2012 14:36:37 -0400 Subject: [PRL] ESOP Torture chamber Wed March 21 4pm @ 366 Message-ID: Hi everyone, I'm having a torture chamber for my upcoming ESOP talk this Wednesday, March 21st, at 4pm in 366. I would appreciate any feedback. Steve From stchang at ccs.neu.edu Wed Mar 21 14:41:17 2012 From: stchang at ccs.neu.edu (Stephen Chang) Date: Wed, 21 Mar 2012 14:41:17 -0400 Subject: [PRL] ESOP Torture chamber Wed March 21 4pm @ 366 In-Reply-To: References: Message-ID: Just a reminder that I'll be holding a torture chamber today at 4pm in 366. I would be grateful for any feedback. On Mon, Mar 19, 2012 at 2:36 PM, Stephen Chang wrote: > Hi everyone, > > I'm having a torture chamber for my upcoming ESOP talk this Wednesday, > March 21st, at 4pm in 366. > > I would appreciate any feedback. > > Steve From dvanhorn at ccs.neu.edu Thu Mar 22 10:47:27 2012 From: dvanhorn at ccs.neu.edu (David Van Horn) Date: Thu, 22 Mar 2012 10:47:27 -0400 Subject: [PRL] Fwd: [NJ-pls] IBM Programming Languages Day In-Reply-To: <20120322142315.GA28268@mantle.bostoncoop.net> References: <20120322142315.GA28268@mantle.bostoncoop.net> Message-ID: <4F6B3B7F.2070103@ccs.neu.edu> -------- Original Message -------- Subject: [NJ-pls] IBM Programming Languages Day Date: Thu, 22 Mar 2012 23:23:15 +0900 From: Chung-chieh Shan To: nj-pls at lists.seas.upenn.edu ----- Forwarded message from Julian Dolby ----- Programming Languages Day 2012 The 2012 Programming Languages Day will be held at the IBM Thomas J. Watson Research Center on Friday, June 29, 2012. The day will be held in cooperation with the New Jersey and New England Programming Languages and Systems Seminars. The main goal of the event is to increase awareness of each other's work, and to encourage interaction and collaboration. The Programming Languages Day features a keynote presentation and approximately 5 regular presentations. Dr. Shriram Krishnamurthi of Brown University will deliver the keynote presentation this year. If you would like to present your work, please send a title and abstract to dolby at us.ibm.com by May 1, 2012. Tutorials or joint presentations are welcome. We also solicit input on topics or particular presentations that would be of interest to attendees. Notification of accepted abstracts will be sent approximately by May 30, 2012. You are welcome from 9AM onwards, and the keynote presentation will start at 10AM sharp. We expect the program to run until 4PM. The Programming Languages day will be held in room GN-F15 in the Hawthorne-1 building in Hawthorne, New York. If you plan to attend the Programming Languages Day, please register by sending an e-mail with your name, affiliation, and contact information to dolby at us.ibm.com so that we can plan for lunch and refreshments to be available. Program committee: Patrick Cousot, ?cole Normale Sup?rieure and New York University Julian Dolby, IBM Thomas J. Watson Research Center John Field, Google Martin Rinard, Massachusetts Institute of Technology Information on Programming Languages Day is available at: http://researcher.ibm.com/project/3198 -------------- next part -------------- A non-text attachment was scrubbed... Name: signature.asc Type: application/pgp-signature Size: 190 bytes Desc: not available Url : http://lists.ccs.neu.edu/pipermail/prl/attachments/20120322/e3c0b179/attachment.pgp -------------- next part -------------- An embedded and charset-unspecified text was scrubbed... Name: Attached Message Part Url: http://lists.ccs.neu.edu/pipermail/prl/attachments/20120322/e3c0b179/attachment.txt From wand at ccs.neu.edu Tue Mar 27 08:01:57 2012 From: wand at ccs.neu.edu (Mitchell Wand) Date: Tue, 27 Mar 2012 08:01:57 -0400 Subject: [PRL] A Picture of Language - NYTimes.com Message-ID: The origin of sentence diagramming. http://opinionator.blogs.nytimes.com/2012/03/26/a-picture-of-language/ -------------- next part -------------- HTML attachment scrubbed and removed From clements at brinckerhoff.org Tue Mar 27 14:16:18 2012 From: clements at brinckerhoff.org (John Clements) Date: Tue, 27 Mar 2012 11:16:18 -0700 Subject: [PRL] A Picture of Language - NYTimes.com In-Reply-To: References: Message-ID: On Mar 27, 2012, at 5:01 AM, Mitchell Wand wrote: > The origin of sentence diagramming. Related question: should first-year programming students be able to "diagram" their code? Specifically, should they be able to identify all nested expressions? John -------------- next part -------------- A non-text attachment was scrubbed... Name: smime.p7s Type: application/pkcs7-signature Size: 4800 bytes Desc: not available Url : http://lists.ccs.neu.edu/pipermail/prl/attachments/20120327/f244ba9c/attachment.bin From matthias at ccs.neu.edu Tue Mar 27 16:26:06 2012 From: matthias at ccs.neu.edu (Matthias Felleisen) Date: Tue, 27 Mar 2012 16:26:06 -0400 Subject: [PRL] A Picture of Language - NYTimes.com In-Reply-To: References: Message-ID: On Mar 27, 2012, at 2:16 PM, John Clements wrote: > > On Mar 27, 2012, at 5:01 AM, Mitchell Wand wrote: > >> The origin of sentence diagramming. > > Related question: should first-year programming students be able to "diagram" their code? Specifically, should they be able to identify all nested expressions? My first programming course required (1) reading and understanding the Algol 60 report grammar and (2) being able to 'parse' an Algol program (if you have seen the back of the Pascal report, you know what I mean). Evaluation problems were done by example -- no real rules.