Better Embedded Languages with Modal Type Theory

This month, I (Dan Doel) will be presenting some ideas from type theory research that have excited me recently, and would probably have made some practical problems I've worked on a lot easier if I'd discovered it earlier.

Abstract

According to the Curry-Howard correspondence, for every logic, there is a type theory. This, of course, extends to modal logics, which allow one to distinguish things like 'global' vs. 'local' constructions. Modalities are reasonably common in programming language research, but with the possible exception of those associated with linear logic, they are not commonly seen in languages under wide use. This talk will explain what modal type theory is, some of the things it's used for, and why a language that incorporates contextual modal types could be the ideal framework for embedded languages, which are a staple of (functional) programming. Some possibilities will be demonstrated in Beluga, a logical framework/proof assistant based on contextual modal type theory.

Bio

Dan has been using Haskell for over a decade, and has learned quite a bit of esoteric math and computer science stuff that is occasionally tangentially related to the real world. He works at S&P Global, using functional programming for portfolio analytics and report generation.

Logistics

The meetup will be at the Thoughtbot location in downtown Boston. Food should be available near the 6:30PM start time, and the talk will begin shortly after that.

Food and beverages will be provided by Thoughtbot.

Streaming

Unfortunately, we won't be able to stream the event tonight. The person with the equipment is busy.