Skip to content

Postdoc opportunities at UPenn, Harvard, and Northeastern

Saturday, August 28, 2010

Applications are invited for postdoc positions in the areas of programming languages, formal verification, operating systems, and hardware design at the University of Pennsylvania, Harvard University, and Northeastern University.

The hosting project, SAFE (Semantically Aware Foundation Environment), is part of CRASH, a larger DARPA-funded effort to design new computer systems that are highly resistant to cyber-attack, can adapt after a successful attack in order to continue rendering useful services, can learn from previous attacks how to guard against and cope with future attacks, and can repair themselves after attacks have succeeded. It offers a rare opportunity to rethink the hardware / OS / software stack from a completely clean slate, with no legacy constraints whatsoever.

Specifically, we aim to build a suite of modern operating system services that embodies and supports fundamental security principles—including separation of privilege, least privilege, and mutual suspicion—down to its very bones, without compromising performance. Achieving this goal demands an integrated effort focusing on (1) processor architectures, (2) operating systems, (3) formal methods, and (4) programming languages and compilers — coupled with a co-design methodology in which all critical system layers are designed together, with a ruthless insistence on simplicity, security, and verifiability at every level.

The ideal candidate will have a Ph.D. in Computer Science, a combination of strong theoretical and practical interests, and expertise in two or more of the following areas: programming languages, security, formal verification, operating systems, and hardware design. The position is for one year in the first instance, with possible renewal up to four years. Starting date is negotiable. Applications from women and members of other under-represented groups are particularly welcome.

To apply, please send a CV, research statement, and the names of three people who can be asked for letters of reference to Benjamin Pierce (bcpierce@cis.upenn.edu). Inquiries can be directed to any of the PIs:

Andre Dehon (Penn)
Greg Morrisett (Harvard)
Benjamin Pierce (Penn)
Olin Shivers (Northeastern)
Jonathan Smith (Penn)

Filed in Announce | Comments (0)

Doctor JS

Thursday, August 26, 2010

Tell the Doctor about it.

Doctor JS is a genius. He’ll analyze your JavaScript code, complete with: polymorphism, prototypes, exceptions, and callbacks.

DoctorJS is a static analysis tool developed by my PRL lab neighbor, Dimitris Vardoulakis. It’s an implementation of Vardoulakis and Olin Shivers‘ CFA2—a context-free approach to control flow analysis.

Brendan Eich, CTO of Mozilla and creator of JS, recently blogged about DoctorJS (Static Analysis FTW) and called static analysis one of the best “researchy” investments Mozilla has made over the past few years.

Filed in CFA, JavaScript | Comments (0)

Abstracting Abstract Machines: Storing and stacking continuations

Monday, July 26, 2010

We’ve been working on two techniques for systematically deriving abstract interpretations approximating canonical machines for higher-order languages. The first allocates continuations in a bounded store to achieve a finite state-space. We demonstrate the generality of this approach by transforming classical abstract machines into abstract interpreters.

Abstracting Abstract Machines.
David Van Horn and Matthew Might.
The 15th ACM SIGPLAN International Conference on Functional Programming (ICFP’10), Baltimore, Maryland, September, 2010.

We describe a derivational approach to abstract interpretation that yields novel and transparently sound static analyses when applied to well-established abstract machines. To demonstrate the technique and support our claim, we transform the CEK machine of Felleisen and Friedman, a lazy variant of Krivine’s machine, and the stack-inspecting CM machine of Clements and Felleisen into abstract interpretations of themselves. The resulting analyses bound temporal ordering of program events; predict return-flow and stack-inspection behavior; and approximate the flow and evaluation of by-need parameters. For all of these machines, we find that a series of well-known concrete machine refactorings, plus a technique we call store-allocated continuations, leads to machines that abstract into static analyses simply by bounding their stores. We demonstrate that the technique scales up uniformly to allow static analysis of realistic language features, including tail calls, conditionals, side effects, exceptions, first-class continuations, and even garbage collection.

The second technique keeps continuations on the stack to achieve a push-down model of abstract interpretation. The resulting abstract interpreter always matches calls and returns, achieving a higher level of precision by never conflating call and return pairs. Although this technique produces abstract interpreters with infinite state-spaces, we demonstrate how basic static analysis questions remain decidable by casting them as language inclusion problems answered by push-down automata.

Pushdown Control-Flow Analysis of Higher-Order Programs.
Christopher Earl, Matthew Might, and David Van Horn.
The 2010 Workshop on Scheme and Functional Programming (SFP 2010), Montréal, Québec, Canada, August, 2010.

Context-free approaches to static analysis gain precision over classical approaches by perfectly matching returns to call sites—a property that eliminates spurious interprocedural paths. Vardoulakis and Shivers’s recent formulation of CFA2 showed that it is possible (if expensive) to apply context-free methods to higher-order languages and gain the same boost in precision achieved over first-order programs.

To this young body of work on context-free analysis of higher-order programs, we contribute a pushdown control-flow analysis framework, which we derive as an abstract interpretation of a CESK machine with an unbounded stack. One instantiation of this framework marks the first polyvariant pushdown analysis of higher-order programs; another marks the first polynomial-time analysis. In the end, we arrive at a framework for control-flow analysis that can efficiently compute pushdown generalizations of classical control-flow analyses.

There are also slides (PDF) covering both techniques from a talk given at the Harvard PL seminar.

Filed in Announce, CFA | Comments (0)

IBM PL Day

Wednesday, June 9, 2010

IBM Programming Languages Day

July 29, 2010, Hawthorne NY

The eleventh annual Programming Languages Day will be held at the IBM Thomas J. Watson Research Center on Thursday, July 29, 2010. 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. (Continued)

Filed in Announce | Comments (0)

Plotkin given SIGPLAN achievement award

Wednesday, June 9, 2010

Gordon Plotkin was awarded the SIGPLAN achievement award at this year’s PLDI.

Professor Gordon D. Plotkin has made fundamental advances in almost every area of the theory of programming languages. His contributions have helped to establish the mathematical foundations on which the scientific study of programming languages are based. His 1975 paper “Call-by-name, Call-by-value, and the λ-calculus” exposed the relationship between the reduction semantics of the λ-calculus and its operational semantics, as defined by Landin’s SECD machine. In the process, he defined what it meant for a calculus and a semantics to correspond: this launched the study of operational semantics as it is now understood. (Continued)

Filed in Announce | Comments (0)

Photos from TFP 2010

Tuesday, June 8, 2010

Some photos from TFP 2010, Norman, Oklahoma.

Filed in Photos | Comments (0)

Robin Milner: The Elegant Pragmatist

Tuesday, June 8, 2010

Turing award winner and programming language trailblazer, Robin Milner, who recently passed away, has a cover story in the latest Communications of the ACM.

A man of modest background and quiet brilliance, Milner made ground-breaking contributions to the fields of verification, programming languages, and concurrency. He was born in 1934 near Plymouth, England, and won scholarships to Eton—where he developed an enduring love of math as well as a prodigious work ethic—and King’s College, Cambridge. It was during his time at Cambridge that Milner was introduced to programming, though the subject didn’t interest him initially. “I regarded programming as really rather inelegant,” he recalled in an interview in 2001 with Martin Berger, a professor at the University of Sussex. “So I resolved that I would never go near a computer in my life.”

Filed in Uncategorized | Comments (0)

What’s the Racket?

Monday, June 7, 2010

Racket, the system formerly known as PLT Scheme, has just been released.

PLT is happy to announce the release of Racket, available from

http://racket-lang.org/

With Racket, you can script command shells and web servers; you can quickly prototype animations and complex GUIs; regexps and threads are here to serve you. To organize your systems, you can mix and match classes, modules or components. Best of all, you start without writing down types. If you later wish to turn your script into a program, equip your Racket modules with explicit type declarations as you wish. And Racket doesn’t just come as a typed variant; you can also write your modules in a purely functional and lazy dialect.

Racket comes in so many flavors because Racket is much more than a standard scripting language or a plain programming language. Racket supports language extensibility to an unequaled degree. A Racket programmer knows that making up a new language is as easy as writing a new library.

To help you start quickly, Racket includes batteries in all shapes and sizes, most importantly, extensive documentation and all kinds of libraries.

Racket occupies a unique position between research and practice. It inherits many major ideas from language research, among them type safety (when the type system says that x is a number, then at runtime it always is a number) and memory safety (when some memory is reclaimed by the garbage collector it is impossible to still have a reference to it). At the same time, user demand governs rigid adherence to purely theoretical principles.

Racket, formerly PLT Scheme, is a product of over 15 years of development. Although Racket starts with a mature software base and an established user community, its new name reflects our view that this is just the beginning of Racket’s evolution.

Filed in Announce, Scheme | Comments (0)

Fun with Unicode and delimited continuations

Thursday, June 3, 2010

Doug Orleans’ cute program to compute roots of quadratic equations:

(define (± x y)
  (shift k (values (k (+ x y)) (k (- x y)))))

(define (quadratic-formula-roots a b c)
  (reset (/ (± (- b) (√ (- (² b) (* 4 a c))))
	    (* 2 a))))
Filed in Poetry, Scheme | Comments (0)

Evaluating Call By Need on the Control Stack

Tuesday, May 18, 2010

New paper from Stephen Chang, David Van Horn, and Matthias Felleisen, appearing at Trends in Functional Programming 2010: Evaluating Call By Need on the Control Stack.

Abstract:

Ariola and Felleisen’s call-by-need λ-calculus replaces a variable occurrence with its value at the last possible moment. To support this gradual notion of substitution, function applications—once established—are never discharged. In this paper we show how to translate this notion of reduction into an abstract machine that resolves variable references via the control stack. In particular, the machine uses the static address of a variable occurrence to extract its current value from the dynamic control stack.

PDF

Filed in Announce, Lazy | Comments (0)

google

google

asus