Bullets are good for your Coq proofs

:: coq

By: Gabriel Scherer

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.

Fall 2016 PL Junior Retrospective

:: PL Junior

By: Ben Chung, Milo Davis, Ming-Ho Yee, Sam Caldwell

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

  1. working from the TAPL presentation of type systems, dependent types are a step up in difficulty (excepting F-omega-sub), and
  2. they represent a significant increase in the reasoning power of types over programs.



By: Gabriel Scherer

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!

Understanding Constructive Galois Connections

:: icfp, galois connection, adjunction, category theory, math

By: Max New

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.