weaselhat

POPL 2010 has been a blast, with lots of great papers and conversation. I presented Contracts Made Manifest at 10:30am today, and the follow-up discussions contained enough ideas for years of research. (So stay tuned!)

Filed by Michael Greenberg on 2010-01-22 at 10:22am under Presentations, Programming Languages
1 Comment

We’ve sent off the final version of Contracts Made Manifest. There have been quite a few improvements since submission, the most important of which is captured by Figure 1 from our paper:

Our submission only addressed lax λ_C, where we had an inexact translation φ into λ_H and an exact translation ψ out of λ_H. We show a dual situation for picky λ_C, where φ is exact and ψ is inexact. Intuitively, languages farther to the right on the “axis of blame” are pickier. Translating from right to left preserves behavior exactly, but left-to-right translations generate terms that can blame more than their pre-images. (There are examples in the paper.) I should note that lax and picky λ_C seem to be the extremes of the axis of blame: I don’t see a natural way to be laxer than lax λ_C or pickier than picky λ_C.

We also show that restricting these calculi to first-order dependency leaves them exactly equivalent; before, we could only show an exact equivalence by eliminating all dependency.

Filed by Michael Greenberg on 2009-11-03 at 12:03pm under Papers, Programming Languages
No Comments

We can’t install software into the /usr tree at my office, so I end up having local installs of lots of software. Some things, like GODI, play well with this. I had some trouble finding the right way to get LLVM’s Ocaml bindings to work, so I figured I’d share the wealth. The following instructions will put an install into the directory $PREFIX/llvm-install.

Here are the steps; they’re followed by a plain English explanation.

cd $PREFIX
svn co http://llvm.org/svn/llvm-project/llvm/trunk llvm
wget http://llvm.org/releases/2.5/llvm-gcc4.2-2.5-x86-linux-RHEL4.tar.gz
tar xzf llvm-gcc4.2-2.5-x86-linux-RHEL4.tar.gz
mkdir llvm-objects llvm-install
cd llvm-objects
../llvm/configure --with-llvmgccdir=$PREFIX/llvm-gcc4.2-2.5-x86-linux-RHEL4 --enable-optimized --enable-jit --prefix=$PREFIX/llvm-install --with-ocaml-libdir=$GODI_PATH/lib/ocaml/std-lib
make
make install

My PREFIX is my home directory, and GODI_PATH = ~/godi. First, we checkout the latest LLVM from SVN (step 2). Then we download and extract the latest release (2.5, as of writing) of LLVM-gcc (steps 3 and 4). (I couldn’t get the SVN version of LLVM-gcc to work with the SVN version of LLVM.) Notably, LLVM does not support in-place builds, so we create the llvm-objects directory to actually build LLVM; we’ll install it into llvm-install (step 5). We configure the software from the llvm-objects directory (steps 6 and 7). The long configure is necessary; the only optional item is --enable-jit. You may have to adjust your --with-ocaml-libdir to point to wherever your Ocaml libraries live. Then make and make install (steps 8 and 9). Voila!

To test it out, we can use the “Hello, World!” program written by Gordon Henrikson. I had to change it a little to bring it up to date with the latest APIs (in particular, the global context had to be added). You can download it as llvm_test.ml.

open Printf
open Llvm

let main filename =
   let c = create_context () in

   let i8_t  = i8_type c in
   let i32_t = i32_type c in

   let m = create_module c filename in

   (* @greeting = global [14 x i8] c"Hello, world!\00" *)
   let greeting =
     define_global "greeting" (const_string c "Hello, world!\000") m in

   (* declare i32 @puts(i8* ) *)
   let puts =
     declare_function "puts"
       (function_type i32_t [|pointer_type i8_t|]) m in

   (* define i32 @main() { entry: *)
   let main = define_function "main" (function_type i32_t [| |]) m in
   let at_entry = builder_at_end c (entry_block main) in

   (* %tmp = getelementptr [14 x i8]* @greeting, i32 0, i32 0 *)
   let zero = const_int i32_t 0 in
   let str = build_gep greeting [| zero; zero |] "tmp" at_entry in

   (* call i32 @puts( i8* %tmp ) *)
   ignore (build_call puts [| str |] "" at_entry);

   (* ret void *)
   ignore (build_ret (const_null i32_t) at_entry);

   (* write the module to a file *)
   if not (Llvm_bitwriter.write_bitcode_file m filename) then exit 1;
   dispose_module m

let () = match Sys.argv with
  | [|_; filename|] -> main filename
  | _ -> main "a.out"

Now we can compile:

ocamlopt -cc g++ llvm.cmxa llvm_bitwriter.cmxa llvm_test.ml -o llvm_test
./llvm_test hello.bc # generates bitcode
$PREFIX/llvm-install/bin/llvm-dis hello.bc # disassembles bitcode into hello.ll
$PREFIX/llvm-install/bin/lli hello.bc # outputs "Hello, world!"

If interpretation via lli isn’t your bag, you can also compile to native code:

$PREFIX/llvm-install/bin/llc hello.bc # generates assembly, hello.s
gcc -o hello hello.s
./hello # outputs "Hello, world!"

Filed by Michael Greenberg on 2009-09-24 at 2:44pm under Programming Languages, Software
2 Comments

Martin Rees caught another bug in PHPEnkoder, which was making it difficult to edit posts with comments containing e-mails. This problem has been solved by turning off the enkoder filters when displaying administrative panels.

In addition to the bugfix, there are two improvements. First, the internal enkoding system will choose names that are more likely to be unique. Second, I’ve added a shortcode, enkode. You can use it to manually enkode an arbitrary stretch of text, like so: [enkode]this will be enkoded[/enkode].

The latest version is available from the PHPEnkoder website and its home in the plugin directory.

Filed by Michael Greenberg on 2009-08-18 at 4:11pm under Software
4 Comments

I am immensely pleased to report that our paper on Flapjax was accepted to OOPSLA 2009.

This paper presents Flapjax, a language designed for contemporary Web applications. These applications communicate with servers and have rich, interactive interfaces. Flapjax provides two key features that simplify writing these applications. First, it provides event streams, a uniform abstraction for communication within a program as well as with external Web services. Second, the language itself is reactive: it automatically tracks data dependencies and propagates updates along those data?ows. This allows developers to write reactive interfaces in a declarative and compositional style.

Flapjax is built on top of JavaScript. It runs on unmodi?ed browsers and readily interoperates with existing JavaScript code. It is usable as either a programming language (that is compiled to JavaScript) or as a JavaScript library, and is designed for both uses. This paper presents the language, its design decisions, and illustrative examples drawn from several working Flapjax applications.

The real heroes of this story are my co-authors. Leo, Arjun, and Greg were there for the initial, heroic-effort-based implementation. Jacob and Aleks wrote incredible applications with our dog food. Shriram, of course, saw the whole thing through. Very few of my contributions remain: the original compiler is gone (thank goodness); my thesis work is discussed briefly in How many DOMs? on page 15. Here’s to a great team and a great experience (and a great language)!

Filed by Michael Greenberg on 2009-08-13 at 11:00am under Flapjax, Papers, Programming Languages
1 Comment

Benjamin Pierce, Stephanie Weirich, and I submitted a paper to POPL 2010; it’s about contracts. Here’s the abstract:

Since Findler and Felleisen introduced higher-order contracts, many variants of their system have been proposed. Broadly, these fall into two groups: some follow Findler and Felleisen in using latent contracts, purely dynamic checks that are transparent to the type system; others use manifest contracts, where refinement types record the most recent check that has been applied. These two approaches are generally assumed to be equivalent—different ways of implementing the same idea, one retaining a simple type system, and the other providing more static information. Our goal is to formalize and clarify this folklore understanding.

Our work extends that of Gronski and Flanagan, who defined a latent calculus \lambda_C and a manifest calculus \lambda_H, gave a translation \phi from \lambda_C to \lambda_H, and proved that if a \lambda_C term reduces to a constant, then so does its \phi-image. We enrich their account with a translation \psi in the opposite direction and prove an analogous theorem for \psi.

More importantly, we generalize the whole framework to dependent contracts, where the predicates in contracts can mention variables from the local context. This extension is both pragmatically crucial, supporting a much more interesting range of contracts, and theoretically challenging. We define dependent versions of \lambda_C (following Findler and Felleisen’s semantics) and \lambda_H, establish type soundness—a challenging result in itself, for \lambda_H—and extend \phi and \psi accordingly. Interestingly, the intuition that the two systems are equivalent appears to break down here: we show that \psi preserves behavior exactly, but that a natural extension of \phi to the dependent case will sometimes yield terms that blame more because of a subtle difference in the treatment of dependent function contracts when the codomain contract itself abuses the argument.

Edit on 2009-11-03: there’s a newer version, as will appear in POPL 2010.

Edit on 2010-01-22: I have removed the link to the submission, since it is properly subsumed by our published paper.

Filed by Michael Greenberg on 2009-07-30 at 3:31pm under Programming Languages, Submissions
4 Comments

I’ve added gravatar support to the website. The gravatar system is a clever way to create identity on-line: e-mails are associated with images. Critically, the URL associated with an e-mail doesn’t include the e-mail itself, but instead an MD5 hash — this way, spammers can’t harvest your address.

I was disappointed to discover that Google Chat doesn’t have support for gravatars — a Google labs feature I would use.

Filed by Michael Greenberg on 2009-05-31 at 1:40pm under Blog
No Comments

Martin Rees noticed that any user can change PHPEnkoder’s settings. I’ve change PHPEnkoder’s settings panel to require the manage_options capability. Now, by default, only administrators can change PHPEnkoder’s settings. (If you’re unfamiliar with the concept, check out the Codex documentation on roles and capabilities.)

As usual, the plugin is available from the PHPEnkoder website and its home in the plugin directory.

Filed by Michael Greenberg on 2009-05-23 at 9:44am under Software
3 Comments

Gretchen Zimmerman noticed a bug in spacing that occurred in some versions of IE. Removing a newline in the generated HTML fixes the problem.

You can download version 1.4 from the PHPEnkoder website or from the Wordpress plugin directory.

Filed by Michael Greenberg on 2009-05-18 at 12:20pm under Software
No Comments

Via the TYPES-announce mailing list:

…we are launching

  Electronic Proceedings in Theoretic Computer Science (EPTCS)

a new international refereed open access venue for the rapid
electronic publication of the proceedings of workshops and
conferences, and of festschrifts, etc, in the general area of
theoretical computer science, broadly construed.

This is exciting news! I’m even willing to overlook the fact the plural of ‘festschrift’ is ‘festschriften’, not ‘festschrifts’.

Filed by Michael Greenberg on 2009-04-30 at 8:58pm under Formal Methods
No Comments