Michael Greenberg's blog: computer science; systems; programming languages.
Live Last read · last published · next check
Along with the PaSh folks , I have two closely related papers at OSDI 2026: one about try and one about hs , which uses try extensively. These papers are the culmination of work we first talked about at HotOS XIX in our 2023 paper, "Executing Shell Scripts in the Wrong Order, Correctly" . try : a semisolate sandbox try lets you run a command and capture its filesystem effects---which can then be…
We (me, Konstantinos Kallas , Nikos Vasilakis , and Vagos Lamprou ) gave a tutorial at POPL 2026 on the POSIX shell : Recent years have seen a resurgence of research on the shell, from optimizing scripts to better leverage parallel and distributed computational resources, to the analysis of scripts for bug-finding, and even research on the usability and programmability of this simultaneously…
Following a mysterious and generous invitation from Kristopher Micinski , four computer scientists ( Annie Liu , Frank McSherry , Scott Stoller , and me) drove into deep upstate New York. The trees close around them as the road shrank from painted asphalt to a one-lane private road to a gravel driveway. What awaited them in the cedar-paneled log cabins strewn over the hill? Two days of interesting…
I frequently start interactive programs from a terminal---often using the handy xdg-open script , sometimes explicitly. I sometimes remember to redirect stdout and stderr to /dev/null , but not always. Hell, half the time I forget to run the command asynchronously with & . It's easy to put a command into the background---a quick ^Z and bg and disown and you're off to the races.…
I spoke at PLMW 2025 , giving a talk titled "How to give a good talk" . Here is an edited transcript of the talk. I wrote a précis on the SIGPLAN blog . You can watch the video on YouTube . How to give a good talk Thank you for having me. I'm going to talk to you about how to give talks, but I want to start by welcoming you to POPL. It might be your first POPL, so: welcome ! I'd like a…
I am a technical consultant for Materialize ---a database for integrating and transforming real-time data---and I just blogged for them about some of the work I've been doing there: Source Mapping and Introspection: Debugging Materialize with Materialize Materialize now exposes source maps in its catalog, so you can build your own debugging queries that attribute performance characteristics…
I finally converted my old blog, weaselhat.com to a static site. I ran on Wordpress for years, but I switched to a static site for a variety of reasons: dynamic websites are less secure and more expensive to run static sites run on markdown, which I can write in my editor of choice static sites let me compose offline static sites let me understand more of the technology stack I'm using No…
I’m looking for PhD students in the Fall 2023 application cycle, to start in Fall 2024. Come work with me at Stevens CS in Hoboken, NJ! I’m particularly looking for students with expertise in systems, but I’m happy to talk to anyone with background related to my work (systems, programming languages, databases, logic). I work in Gateway South (the left-hand side of this photo). You could, too!…
The first person to explain answer set programming (ASP, pronounced ‘ay ess pee’) to me ( Joe Osborn ) told me about the three line implementation of graph coloring and the termination guarantees. Like any PL person, I recoiled in horror: you have an always-terminating language where I can solve NP-complete problems in three lines? So every time I write a program of three lines or more, I have to…
Part of what’s hard about grad school is that things are undirected. In undergrad, you have well delimited homework assignments, maybe a project or two. But in grad school everything is open ended, and you’re lost at sea! And that broad scope—confronting the unknown and feeling stupid —really is part of what’s hard. But in this lecture about writing , Larry McEnerney makes the point that there’s…
Program synthesis is an appealing notion: I give you a pretty good (but incomplete) description of a program, and you give me a working program back out. Flash Fill—program synthesis by example that ships in Excel—is the standard example that PL people trot out, and it is an incredible success. (Check out Sumit Gulwani’s POPL 2015 keynote (video in supplemental material) if you’ve never heard of…
Kleene algebra with tests is a beautiful, powerful framework for reasoning about programs. You can easily encode conventional While programs into KAT, and KAT enjoys decidable equality. Reasoning with KAT feels like you’re cheating Alan Turing himself: here we are, deciding nontrivial properties of programs! The gist of KAT is that you write programs using a regular expression like notation: + for…
How should we summarize performance numbers? In a recent benchmark run, I had some interesting speedup numbers that I wasn't certain how to report. While it's easy to make charts that are illuminating, I'm not certain what I should say in, e.g., an abstract. Here's the raw data (also available as a spreadsheet ), noting that I've made everything as abstract as I can: In…
I want to believe in a future where the lion will lie down with the lamb; we'll beat our swords into plowshares; and developers will migrate dynamic prototypes to robust static systems with confidence. But these Aquarian visions are elusive. Having a map of the road to paradise in theory doesn't mean we know how to get there in practice. Let me tell you about two papers at OOPSLA that…
I'm looking for PhD students in the Fall 2021 application cycle, to start in Fall 2022. Come work with me at Stevens CS in Hoboken, NJ ! I work in Gateway South (the left-hand side of this photo). You could, too! (Photo credit: Stevens Alumni .) What will we work on? I'm interested in applying formalism --- all those pretty Greek letters in program semantics, type systems, and static…
After six years at Pomona College , I've moved to Stevens Institute of Technology as an assistant professor in the computer science department . I miss my lovely Pomona colleagues--- they're hiring! ---but I'm excited to be on the East Coast and to be doing more research with a new set of lovely colleagues. I've got a new webpage , but the old webpage should stay up. We'll…
Pomona College's computer science department is hiring Fall of 2021 for Fall 2022 . I used to work at Pomona , and there is a lot to recommend it. Pomona College is a small liberal arts college (SLAC) in LA County, 35mi/45-240min outside DTLA. It's a 2:2 teaching load. Steps on campus, with a view of the mountains behind. First and foremost, you'll have excellent colleagues.…
The Unix shell is incredibly powerful. I use it routinely for simple tasks (moving files around), routine work (grading scripts), and in my development process (building, deploying, etc.). When I'm working with text, the shell and its ecosystem is excellent: patching together cat , find , grep , sed , tr , and cut with shell pipelines and redirections is a convenient, expressive, and fast way…
I have a new post up on the SIGPLAN blog: "Making PL Ideas Accessible: An Open-Source, Open-Access, Interactive Journal . Inspired by Distill , I propose an open-access, open-source, interactive journal for disseminating clear presentations of current ideas and methods in programming languages. It's a particularly good moment to consider our research's reach and impact: CORE has just…
POPL 2021 is open for business on Clowdr ! The synchronous band is in the afternoon and evening in Central European Time (CET = UTC+1). I live outside LA, which is UTC-8... so the POPL happy hours at 10:30am start a little early even for me. So far as I know, this is the first POPL with a paper named after a cocktail . Accordingly, I've decide to host a POPL Cocktail Hour on Wednesday,…
I recently wrote on the SIGPLAN blog about how PL notation is a barrier to entry . While the arguments are mine, I acknowledge the many folks who helped me write it in the post. Ideas from an interesting conversation with Neel Krishnaswami came up again in a comment from Jeremy Gibbons . The universe has spoken: here's what I think about cast notation. First, here's what Neel said: I…
Robin Gandy's "On the Axiom of Extensionality--Part 1", Journal of Symbolic Logic, Vol. 21, No. 1 (Mar., 1956) quotes Alan Turing using a racist phrase. [Turing] always spoke of the axiom of extensionality as being 'the nigger in the woodpile', which suggests that he did not think his consistency proof was transcendental enough to accord with Gödel's theorem. Yikes. Those…
So you want to define a gradual type system, like all the cool kids? My SNAPL 2019 paper imagines three possible motivations: Expressiveness. You have nothing to lose but your static chains! Interoperation. Gradual typing seamlessly weaves the dynamic and static worlds into a single fabric. Typing itself. Static typing offers myriad benefits: enjoy them today! You don't have to pick just one.…
If you read a description of a static analysis in a paper, what might you find? There'll be some cute model of a language. Maybe some inference rules describing the analysis itself, but those rules probably rely on a variety of helper functions. These days, the analysis likely involves some logical reasoning: about the terms in the language, the branches conditionals might take, and so on.…
When I mentioned how important smart constructors are for Brzozowski derivatives on Twitter, when Prabhakar Ragde raised an interesting question about how big the derivative of a regex is . ( UPDATE 2024-12-14 : Prabhakar is no longer on Twitter, but the anecdote was about how Brzozowrski did not himself know the answer to this question.) The question is subtle: it's not about how many…
CS 181-N Advanced Functional Programming is a project-based elective I'm teaching this semester. The first half of the course teaches the students basic Haskell programming, from purity to FAM and IO, by way of parsing. The second half of the course has the students build a small project using a pure FP (Haskell and Elm, this go round). The projects were kicking off just as we pivoted to…
Shriram Krishnamurthi , Arjun Guha , Leo Meyerovich , and I wrote a post about Flapjax on PL Perspectives , the SIGPLAN blog. (Thanks to Mike Hicks for helping us edit the post!) Flapjax won the OOPSLA MIP award for 2009 (though the SIGPLAN website isn't yet up to date). Our blog post is about the slightly unconventional way we worked: most of the Flapjax work happened in 2006 and 2007, but…
I've been building an executable formalization of the POSIX shell semantics, which I've been calling smoosh (the Symbolic, Mechanized, Observable, Operational SHell). I'm pleased to announce an important early milestone: smoosh passes the POSIX test suite (modulo locales, which smoosh doesn't currently support). I've accordingly tagged this 'morally correct'…
The recent organizers of the Off the Beaten Track (OBT) workshop ( Luke Church , Bob Atkey , Lindsey Kuper , Swarat Chaudhuri , Ranjit Jhala , Shriram Krishnamurthi , David Walker , and me) have decided not to hold OBT at POPL 2020. OBT served a particular purpose: a venue for testing out new, weird ideas at a familiar setting with familiar faces. It was, as Lindsey Kuper explains , very…
I'll be presenting my thoughts on the state of gradual typing research---along with some goals and challenges---at SNAPL 2019 . Here's the abstract of my paper, The Dynamic Practice and Static Theory of Gradual Typing : We can tease apart the research on gradual types into two 'lineages': a pragmatic, implementation-oriented dynamic-first lineage and a formal, type-theoretic,…
While on sabbatical in Cambridge, MA (thanks, Steve !), I had the good fortune to attend my first SPLASH . I was particularly excited by one paper: Collapsible Contracts: Fixing a Pathology of Gradual Typing by Daniel Feltey , Ben Greenman , Christophe Scholliers , Robby Findler , and Vincent St-Amour . (You can get the PDF from the ACM DL or from Vincent's website .) Their collapsible…
I've been thinking about and working on the POSIX shell for a little bit over a year now. I wrote a paper for OBT 2017 , titled Understanding the POSIX Shell as a Programming Language , outlining why I think the shell is worthy of study. For some time I've had the conviction that word expansion---the process that includes globbing with * but also things like command substitution with…
NB I left Pomona college in 2021. But they're hiring again, and I recommend you consider it ! It's my fifth year as a tenure-track assistant professor at Pomona College, a small liberal arts college (SLAC) in Claremont, CA. You may have read about why mathematicians might find the liberal arts setting appealing . Here's why I think computer scientists might, too. I'll start…
I recently gave a talk to some Pomona College undergrads about how to secure their various devices (computers and phones in particular). I tried to focus on clear and concrete advice. I got tons of help on twitter , and I ultimately came up with a slides for a talk and a security checklist . First: I'd like to encourage other people to give this talk. Let me know how it goes, and I'll…
Per a request of sk19er on the Wordpress forums , I've implemented a new feature for PHPEnkoder: you can use the [noenkode] shortcode to turn off PHPEnkoder on a specific page. As always, you can get PHPEnkoder from Wordpress Plugin Directory .
In hybrid type checking , a subtyping relationship between subset types {x:T|e} determines when it's safe to omit a cast. The structural extension of subtyping to, e.g., function types, gives us a straightforward way to achieve verification by optimization : if we can prove that a cast is from a subtype to a supertype, there's no need to pay the runtime cost of checking anything. When…
I recently had some trouble getting ctypes working, so I thought I'd share my solution. I found the Real World OCaml chapter on FFIs , and I tried following their advice first. They suggest: brew install libffi opam install ctypes But it doesn't quite work. For one, you also need to install ctypes-foreign. For two, the brew installation of libffi doesn't automatically install itself…
Frank Pfenning originated the idea of refinement types in his seminal PLDI 1991 paper with Tim Freeman . Freeman and Pfenning's refinement types allow programmers to work with refined datatypes, that is, sub-datatypes induced by refining the set of available constructors. For example, here's what that looks like for lists, with a single refinement type, α singleton : datatype α list =…
I'm working on a Twitter bot, and I ran up against something very annoying: apps need to be on an account with a mobile phone number. I have just one mobile phone, and it's already tied to my real Twitter account. Rather than finding a way to get another mobile number, I had the bot authorize my app using Twitter's OAuth API. Here's how to do it. Step one: collect your API…
I've resolved some E_NOTICE -level messages that were showing up when people set WP_DEBUG to true . Thanks to Rootside for pointing out this problem on the Wordpress forums . As always, please let me know on the forums or via email if you run into any problems.
As an academic computer scientist, I frequently interact with the world of 'tech', as embodied by Silicon Valley, startups, etc. Many of my friends---from college, from graduate school---work there. My younger brother works there. One of the things that has kept me out of that world is my wariness of its politics, ethics, and aesthetics. I was delighted, then, when I was introduced to…
I'm really happy to be part of the first PLVNET , a workshop on the intersection of PL, verification, and networking. I have two abstracts up for discussion. The first abstract, Temporal NetKAT , is about adding reasoning about packet histories to a network policy language like NetKAT. The work on this is moving along quite nicely (thanks in large part to Ryan Beckett!), and I'm looking…
I am delighted to announce that Space-Efficient Manifest Contracts will appear at POPL 2015 in Mumbai . Here's the abstract: The standard algorithm for higher-order contract checking can lead to unbounded space consumption and can destroy tail recursion, altering a program's asymptotic space complexity. While space efficiency for gradual types---contracts mediating untyped and typed…
Reading Aseem Rastogi , Avik Chaudhuri , and Basil Hosmer 's POPL 2012 paper The Ins and Outs of Gradual Type Inference , I ran across a quote that could well appear directly in my POPL 2015 paper, Space-Efficient Manifest Contracts : The key insight is that ... we must recursively deconstruct higher-order types down to their first-order parts, solve for those ..., and then reconstruct the…
I recently wrote a bit of code for scheduling the discussion order of PC meetings so as to minimize traffic in and out of the room due to conflicts of interest. Given some information that HotCRP happily generates, the code generates a schedule, which can be further turned into a handout and slides showing the current paper's conflicts and the two upcoming papers. If you're interested in…
I have a new and much improved draft of my work on Space-Efficient Manifest Contracts . Here's the abstract: The standard algorithm for higher-order contract checking can lead to unbounded space consumption and can destroy tail recursion, altering a program's asymptotic space complexity. While space efficiency for gradual types---contracts mediating untyped and typed code---is well…
Cole Schlesinger , Dave Walker , and I submitted a paper to ICFP 2014 . It's called Concurrent NetCore: From Policies to Pipelines . Here's the abstract: In a Software-Defined Network (SDN), a central, computationally powerful controller manages a set of distributed, computationally simple switches. The controller computes a policy describing how each switch should route packets and…
I just finished reading A Balance of Power: Expressive, Analyzable Controller Programming . It's an interesting proposal, but I'm writing just to express my satisfaction with the following sentence: When we hit expressive limits, however, our goal is not to keep growing this language---down that path lies sendmail.cf and other sulphurous designs---but to call out to full-language code.…
I've released a bugfix for PHPEnkoder version 1.12. Get this: before version 5.5, PHP didn't support arbitrary array index expressions. The problem was a line: $ord = unpack("N",$c)[1]; Which I changed to: $bs = unpack("N",$c); $ord = $bs[1]; This is really ridiculous. Like, serious amateur hour ridiculous. Like, if your final project in a compiler's class had syntactic limitation,…
I'm really delighted to have resolved a longstanding problem with PHPEnkoder and Unicode: PHPEnkoder should no longer choke on the various multi-byte characters, such as λ and è and ワ. As usual, updates are available from the WordPress plugin directory or from your dashboard.
