This is the home page for research in programming languages (PL), software engineering (SE), and related work in human-computer interaction (HCI) at MIT.

Saman Amarasinghe

Commit Group

  • Compilers
  • High Performance Computing
  • High Performance Languages
  • Dynamic Program Analysis and Optimization
  • Security

View Site »


Computation Structures Group

  • Programming Languages and Compilers for Hardware and Software Synthesis
  • Functional Languages and Types
  • Ensuring Correctness by Construction

View Site »

Michael Carbin

Programming Systems Group

  • Programming Languages and Compilers for Approximate and Resilient Systems
  • Program Verification
  • Program Optimization
  • Reliability and Fault Tolerance

View Site »

Adam Chlipala

Programming Languages & Verification Group

  • Program Verification
  • Interactive Theorem Proving
  • Types and Functional Programming
  • Security

View Site »

Daniel Jackson

Software Design Group

  • Software Design
  • Dependability
  • Safety & Security
  • Language Design
  • Formal Methods & Model Checking

View Site »

Rob Miller

User Interfaces Group

  • Human-Computer Interaction
  • End-User Programming
  • Software Development Tools
  • Crowd Computing

View Site »

Martin Rinard

Program Analysis and Transformation Group

  • Probabilistic, Statistical, and Logical Reasoning for Software Systems
  • Analysis and Transformations for Secure, Robust, Resilient, and Efficient Computer Systems

View Site »

Armando Solar-Lezama

Computer-Aided Programming Group

  • Program Synthesis
  • Programming Tools
  • Programming Models for High-Performance Computing

View Site »

Project Group Description
Accuracy-Aware Computing Rinard Program analysis and transformation for approximate computations
Alloy Jackson A declarative language for modelling software systems that manipulate complex structures
Bedrock Chlipala An extensible low-level programming language designed to enable formal verification
BCL: Bluespec Codesign Language Arvind Automatic generation of HW/SW interfaces
Bolt Rinard Eliminating infinite loops in stripped x86 and x64 binaries
Cloud Intrusion Detection and Repair Rinard Security and resilience for cloud computing systems
Collabode Miller A web-based Java software development environment designed to support close, synchronous collaboration between two or more programmers
DynamoRIO Amarasinghe An efficient runtime code manipulation system
Input Rectification Rinard Eliminating vulnerabilities and preserving content by modifying inputs
Kendo Amarasinghe A deterministic multithreading library for commodity hardware
Micado Amarasinghe An AutoCAD plug-in for programmable microfluidic chips
Multi-FPGA Compiler Arvind Compiling LI-BDNs for multiple FPGA executions
PetaBricks Amarasinghe A language that exposes algorithmic choices to the compiler
Programming with Delegation Solar-Lezama Using constraints in implementations to produce robust and efficient programs
Program Verification for Secure Mobile Apps Rinard Static analysis for secure Android applications
Relaxed Programming Rinard Analysis and verification of relaxed nondeterministic programs
Rule-Based Power Gating Arvind Language semantics driven power gating of Bluespec programs
Sketch Solar-Lezama Induction-based program synthesis from implementation specifications
SPICE Rinard Eliminating vulnerabilities in stripped x86 and x64 binaries
Storyboard Programming Solar-Lezama Using abstraction and a graphical interface for usable and verifiable program synthesis
StreamIt Amarasinghe A high-performance language and compiler for streaming applications
Structural Bluespec Arvind Automatic transformation of synchronous FSM specifications into LI-BDNs
Synthesis from Program Traces Solar-Lezama Using a database of program behaviors to aid synthesis for complex object-oriented library code
Umbra Amarasinghe An efficient and scalable memory shadowing framework
Ur/Web Chlipala A statically typed functional programming language for Web applications, with security-by-construction and support for statically typed metaprogramming
Verification of Rule-Splitting Transformations in Bluespec Arvind
VIBRANCE Rinard Dynamic techniques for secure Java programs

Boston Area PL Seminars

New members of our group may wish to keep an eye on some of the following series:

Name Notes
MIT PL Seminar mailing list, calendar
New England Programming Languages and Systems Symposium (NEPLS) Meets a few times per year, usually at least once at a location reachable from MIT by MBTA public transit
Boston University PL Reading Group
Harvard PL Seminar mailing list, calendar
Northeastern University PL Seminar mailing list
General MIT CSAIL seminars mailing list, calendar

Programming Language User Groups

Name Notes
BostonHaskell Often meets in the Stata Center
New England F# User Group Usually meets at the Microsoft NERD Center in Kendall Square


Name Notes
MIT PL Group Blog
Accessibility information