CMSC 499A: Compiling Concurrent Functional Programs to an Abstract Process Machine
Fall 2026. Current UMD undergraduates may participate through CMSC499A: Research with Professorial Faculty. Interested students should email dvanhorn@cs.umd.edu before the start of the semester.
This research project will explore the design and implementation of a compiler for a small concurrent functional programming language inspired by Concurrent ML. The project will investigate how high-level language features such as functions, lexical scope, process spawning, synchronous communication, events, and message passing can be compiled to a lower-level abstract process machine.
The central idea is to treat the operating-system/runtime interface as a semantic target for compilation. Rather than compiling directly to conventional hardware, we will compile programs to an executable process-machine language that provides abstractions such as processes, channels, scheduling, blocking communication, and resource handles. This target machine may also connect to a separate project on modeling operating systems as implementations of abstract machines.
The study will focus on:
- designing a small ML-like source language,
- defining its operational semantics,
- implementing a parser, interpreter, and compiler,
- designing a process-machine target language,
- compiling functional abstractions such as closures and environments,
- compiling concurrency constructs such as spawn, send, recv, and possibly CML-style events,
- testing compiler correctness using executable semantics,
- and stating key semantic correctness properties.
Possible project components include:
- a small type checker or type inference engine,
- a bytecode or abstract-machine backend,
- a runtime representation for closures and channels,
- examples such as echo servers, pipelines, client/server programs, and interactive shells,
- lightweight correctness proofs or refinement arguments in Lean,
- and integration with an executable abstract OS/process-machine model.
The project is exploratory and implementation-oriented. Students do not need prior experience with formal verification, but should be interested in programming languages, compilers, functional programming, concurrency, or operating systems. The goal is to develop working infrastructure and examples that could form the basis for a future course on compiling concurrent functional languages and their runtime systems.