Write a Blog >>

This tutorial provides a brief introduction to the Redex programming language for semantic modeling. It does so by developing several semantic models of a simple programming language and then showing how to construct a program analyzer for this language using the “Abstracting Abstract Machines” method (Van Horn and Might, ICFP 2010).

So this tutorial aims to accomplish two goals:

  1. to introduce semantic engineers (programming language researchers, language designers and implementors, analysis and tool builders, etc.) to the Redex programming language;

  2. to demonstrate the method of building abstract interpreters known as AAM.

This tutorial serves either purpose. If you want to learn Redex, this tutorial will build a bunch of standard semantic systems: reduction relations, type judgments, evaluators, machines, and finally a program analyzer. If you want an explicit and approachable introduction to the AAM method, this tutorial will walk you through a detailed construction.

I work toward making the construction of reusable, trusted software components possible and effective. My research has spanned program analysis; semantics; verification and model-checking; security; logic; complexity; and algorithms.

With Jeff Foster and Mike Hicks, I direct the laboratory for Programming Languages at the University of Maryland (PLUM). Previously, I’ve worked with the Programming Research Laboratory (PRL) at Northeastern University.

I currently serve as a steering committee member and the publicity chair for ICFP, as a program committee member for ICFP 2015, Scheme 2015, and ECOOP 2016, and as an external review committee member for POPL 2016.

I co-authored the book Realm of Racket with Matthias Felleisen and undergraduates from Northeastern University, which introduces programming interactive video games.

Mon 18 Jan

08:30 - 10:00: Tutorials - T1: An Introduction to Redex with Abstracting Abstract Machines at Room HTC 1
POPL-2016-tutorials145310220000008:30 - 10:00
Link to publication