Posts tagged academia

After a successful virtual PLDI, some of us expressed support for more virtual conferences in the future, and some expressed dissent and concerns. The result was an interesting discussion on Twitter, which is essentially impossible to follow. I summarize the discussions here, and include some of my own editorializing.

Please forgive the typos; my fingers quickly get out of sync with my brain, especially at 1am while following multiple twitter discussions.

Around this time of year (graduate student recruiting season), I see lots of:

1. Stress from students who are unsure about the graduate recruiting process and how their application is viewed.
2. Reassurance from people who have been through the process, e.g.,:

https://twitter.com/TaliaRinger/status/1225981382708514817

What I don’t see much from professors explaining WTF.

I’ve now been on both sides of this process and wants to give a peak behind the mysterious curtain in an attempt to reduce stress from students currently going through this process, and hopefully help future students with their applications.

This started as a tweet thread; you can view the original here:

https://twitter.com/wilbowma/status/1226023671946330113

In this post, I maintain that thread and elaborate on it.

In this post, I describe a proposal to redevelop the Construction Science introduction course to use hammers, a standard and state-of-the-art industry tool that students should have experience with.

In August, I was reflecting on why I even go to conferences. I set forth an experiment to judge my own hypothesis about why I go to ICFP. ICFP 2017 met both criteria: I sat through a talk that was not on my list of expected interesting talks, and I had one unexpected interaction and learned something new (and got a new research idea out of it).

I submitted two papers to POPL 2018. The first, “Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible”, was accepted. The second, “Correctly Closure-Converting Coq and Keeping the Types, Too” (draft unavailable), was rejected.

Initially, I was annoyed about the reviews. I’ve since reconsidered the reviews and my work, and think the reviewers were right: this paper needs more work.

I am once more attending, contributing to, and volunteering at ICFP. But why do I do that?

Almost two months ago, my colleagues in the Northeastern PRL wrote about three of our POPL 2017 Student Research Competition submissions. There was fourth submission, but because I was hard at work completing proofs, it wasn’t announced.

Toward Type-Preserving Compilation of Coq

Toward Type-Preserving Compilation of Coq
William J. Bowman
2016

A type-preserving compiler guarantees that a well-typed source program is compiled to a well-typed target program. Type-preserving compilation can support correctness guarantees about compilers, and optimizations in compiler intermediate languages (ILs). For instance, Morrisett et al. (1998) use type-preserving compilation from System F to a Typed Assembly Languages (TAL) to guarantee absence of stuckness, even when linking with arbitrary (well-typed) TAL code. Tarditi et al. (1996) develop a compiler for ML that uses a typed IL for optimizations.

We develop type-preserving closure conversion for the Calculus of Constructions (CC). Typed closure conversion has been studied for simply-typed languages (Minamide1996, Ahmed2008, New2016) and polymorphic languages (Minamide1996, Morrisett1998). Dependent types introduce new challenges to both typed closure conversion in particular and to type preservation proofs in general.

Full disclosure: This blog post is sponsored in part by ACM SIGPLAN. ACM SIGPLAN! Pushing the envelope of language abstractions for making programs better, faster, correcter, stronger.

TLDR

I went to ICFP again this year. I’m a frequent attendee. Last year I had a paper and gave a talk. This year I had a paper, but someone else gave the talk. But I also gave a talk at HOPE 2016. I met some people and saw some talks and pet a deer.

I returned from ECOOP a few weeks ago, and have been trying to figure out what I got of the experience. I’ll focus on two big things.

For a long time I have been debating what I should do after I graduate, which I usually phrase as “industry vs academia”. I’m coming to understand this is a false dichotomy, as most dichotomies are. (It helps that a friend spelled it out for me.) Dave Herman’s talk, on starting and running a research lab doing academic-style work (e.g., developing a principled, safe programming language) in industry, helped me see that. Shriram’s summer school lectures were equally helpful, and sort of the dual of this: taking objects from industry—scripting languages—and applying academic rigor to them. ECOOP, more than any other conference I’ve been to, brought together industry and academia in a smooth spectrum. I wish I had attended as a younger student.

The other big thing was a crystallized version of thoughts I had on programming language. Matthias Felleisen on Racket and Larry Wall on Perl 6 helped me see this: anything you might want to do to or in a program should be expressible in your programming language (Matthias said it better). This is what annoys me about languages like C, Java, and Coq. C has the preprocessor and make and the dynamic linker, etc. Java has Eclipse. Coq has OCaml plugins. All of these languages require doing “more” than writing programs, but have no way to express it in the language. Racket (and, apparently, Perl 6) pulls those things into the language so that those too become just writing programs: extend the reader, dynamically load a library, muck about with the top level, add new syntax.

I got a handful of smaller things: insights about what objects are best at, what a long-term (~25 year) research agenda looks like, an appreciation for the 99 different designs for any given program.

ECOOP was a great experience. If I go again, though, I hope the summer school won’t conflict with the entire research track.

Full disclosure: This blog post is sponsored and required by the National Science Foundation (NSF): The NSF! Funding SCIENCE! since 1683 or whenever.

TLDR

I’m going to ECOOP to see a part of the PL community I wouldn’t normally see, talk to people that I wouldn’t normally talk to, attend the co-located summer school, and figure out what I want to do with my (academic) life. If you want to know why I might do those things, read a little about me.

The long story

On Sunday, I am heading to ECOOP. I have never been to ECOOP, the conference is a little outside of my specialty, I do not know anyone there, and I do not even have a paper or talk at one of the workshops. However, a few weeks ago I ignored an email from one of the mailing lists that said there was some NSF funding that students should apply for. Then I saw an email from Jan Vitek on a local mailing list saying students should really apply for this funding and get to go to Rome.

“Huh”, I thought to myself, “I wonder what’s interesting in Rome”. I went to the ECOOP program and started looking around.

The Curry On program looks interesting. This co-located conference should help me understand how PL applies to industry problems. Unfortunately, I’m going to miss most or all the first day. But the talk I’m most interested in is the final keynote, “Building an Open Source Research Lab”; hopefully this will give me some insights on this industry vs academia problem I have been struggling with.

There is also a summer school. While the history of typed and untyped languages looks fascinating, I’m going to have to skip part of it to learn about type specialization of JavaScript programs; I prove things on type-preserving compilation and I want to see more work that uses types for optimizations. Next up, the lecture on “Building a Research Program for Scripting Languages” should help me better understand what an academic career will look like, and give me some idea of how to be a good academic. Then I’m going to learn how to build a JIT compiler for free, because despite being a compilers expert, I don’t know anything about JIT compilers. Finally, I’m going to learn a little about experimental evaluation; I normally do theory and proofs, but I imagine one day I might need to measure something.

Unfortunately, the summer school is in parallel with most of the conference talks, so it’s going to be tough to decide how much of the summer school to miss in order to see new research.

“Yeah”, I thought after much consideration, “I guess there are some interesting things to see in Rome”. I’m a little concerned about the accommodations and venue though; I understand that a lot of the architecture in Rome is very old.