Posts tagged academia

I’ve been doing, and experiencing, a lot of peer reviewing lately. I’ve been ranting about it on Twitter as I get reviews that don’t help me and, in many ways, hurt me, and lauding reviews that provide useful constructive feedback (even if I disagree with it or the decisions). I’ve been trying to figure out how to provide good reviews and avoid negative aspects of reviewing.

I need to get the thoughts out of my head. These are not declarations of what peer reviewing is or should be, but my attempt to work through those questions.

I wrote the follow at some semester prior to today, about no one in particular, while updating syllabus.

It’s weird, but professors are almost never taught how to teach, how to design a course, how to assess students, how to design an exam or what the point of an exam even is. We’re just expected to pick this up on our own, I guess. It’s not as nonsensical as it sounds, since we are trained how to do research and communicate that research, and there is some overlap. But still.

If my experience is any indication, we just pick up an existing course structure and more or less follow that. Oh, the last person who taught this course used this material, and this syllabus, and these exams, so I’ll just do more or less that for now. If we’re ambitious and/or want to shoot our tenure track in the foot, we might try to innovate soon after. Otherwise, we might innovate later.

Anyway I’m not good at doing things just because that’s how they’ve always been done; I need first principles. After designing, administering, grading, invigilating several of them, I was struggling to figure out what the point of a final exam is. So I had a bunch of conversations on Twitter and now I’m collecting my thoughts on what the point of a final exam is and how it might, or might not, serve a purpose in my course.

Warning: I am not an education researcher, and this is not research, and it’s got a lot of stream-of-consciousness.

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.