The Programming Language Seminar, Junior (or “PL Junior”), is a seminar for junior students to learn and discuss topics at a pace more suitable to our background. This semester, we decided to study dependent types. We chose this topic because
- working from the TAPL presentation of type systems, dependent types are a step up in difficulty (excepting F-omega-sub), and
- they represent a significant increase in the reasoning power of types over programs.
How do researchers know whether they are doing “enough” or “too many” reviews? A measurable goal is to be review-neutral: to have demanded, through our submissions, as many reviews as we have produced as reviewers.
Max New, Daniel Patterson and Ben Greenman recently wrote three two-page abstracts on what they are working on right now. Come have a look — and any feedback is welcome!
One of my favorite papers at ICFP 2016 (in lovely Nara, Japan) was Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory by David Darais and David Van Horn. The central technical result is quite interesting, but a little intimidating, so I’d like to share a “de-generalization” of the result that I found helpful to understand.
The λ-calculus is often introduced by showing how to build a real programming language from it’s simple syntactic forms. In this series of post, I attempt to introduce it as a tool for modeling semantics. So if you’re opening Barendregt for the first time, trying to understand a lecture from a programming languages or functional programming class, or just starting to become involved in PL research, I hope this post will help you understand evaluation by substitution (β-reduction).
“Meaningful distinctions deserve to be maintained.” — Errett A. Bishop
Likewise, memorable quotations deserve to be read in context. In this spirit, I am happy to present the above “basic principle” in its context: Schizophrenia in contemporary mathematics (pdf)
Read on for a brief summary.
Christos Dimoulas is currently teaching a “History of Programming Languages” class at Harvard. The class is, as Christos writes, “definitely not about this”; instead, each meeting is a deep examination of a single, mature research topic, in terms of three to five key papers from the literature.
On Monday, I presented “the History of Actors” for the class. I’ve made the written-out talk notes and an annotated bibliography available here.
In the early days of the famous Emacs/Vim debates, Emacs was often ridiculed for its bulkiness (Eight Megabytes-of-RAM And Constantly Swapping, etc.). The computational power of our computer has grown much faster than Emacs’ bloat: it takes exactly one second to load on my machine. However, our workflows have also changed, and my workflow implies frequently starting new text editors — on each git commit for example, or when I use a Firefox extension to edit a textarea content in a proper editor.
In this blog post, I describe how to use
emacsclient to reuse an existing Emacs process when creating a new editor window, which reduces editor startup times from 1s to 0.150s on my machine.
If you are interested in learning about the internals of the CompCert C compiler but would rather not read its source code, this post is for you.