This semester at Northeastern, Matthias Felleisen is organizing the History of Programming Languages seminar. Look for posts tagged
HOPL for updates from the lectures.
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).