::

::

## Top Five Results of the Past 50 Years of Programming Languages Research

::

Over the past 50 years, which result from programming languages research has had the greatest impact on working programmers?

## What even is compiler correctness? (cross-post)

:: by William J. Bowman

::

::

## PLT Redex: mf-apply

::

The mf-apply keyword is for checked metafunction application in PLT Redex. In other words, (mf-apply f x) is just like (f x), but errors if f is not a previously-defined metafunction.

Also, consider applying to attend The Racket School of Semantics and Languages in Salt Lake City this summer: http://summer-school.racket-lang.org/2017/

## PLISS: Oregon without the greek

::

What does every student interested in programming languages need to learn about the practical side of the field? That is the question that the first international summer school on programming language implementation (or PLISS for short) has set out to answer.

::

## Bullets are good for your Coq proofs

::

I believe that bullets are one of the most impactful features of recent versions of Coq, among those that non-super-expert users can enjoy. They had a big impact on the maintainability of my proofs. Unfortunately, they are not very well-known, due to the fact that some introductory documents have not been updated to use them.

Bullets are a very general construction and there are several possible ways to use them; I have iterated through different styles. In this post I will give the general rules, and explain my current usage style.