PL + SE @ MIT CSAIL
This is the home page for research in programming languages (PL), software engineering (SE), and related work in human-computer interaction (HCI) at MIT.
Faculty
Saman Amarasinghe
Commit Group
- Compilers
- High Performance Computing
- High Performance Languages
- Dynamic Program Analysis and Optimization
- Security
Arvind
Computation Structures Group
- Programming Languages and Compilers for Hardware and Software Synthesis
- Functional Languages and Types
- Ensuring Correctness by Construction
Michael Carbin
Programming Systems Group
- Programming Languages and Compilers for Approximate and Resilient Systems
- Program Verification
- Program Optimization
- Reliability and Fault Tolerance
Adam Chlipala
Programming Languages & Verification Group
- Program Verification
- Interactive Theorem Proving
- Types and Functional Programming
- Security
Daniel Jackson
Software Design Group
- Software Design
- Dependability
- Safety & Security
- Language Design
- Formal Methods & Model Checking
Rob Miller
User Interfaces Group
- Human-Computer Interaction
- End-User Programming
- Software Development Tools
- Crowd Computing
Rachit Nigam
Foundations of Languages and Machines Group
- Hardware Design
- Compilers & Programming Languages
- Computer Architecture
- High-Performance Accelerators
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
Armando Solar-Lezama
Computer-Aided Programming Group
- Program Synthesis
- Programming Tools
- Programming Models for High-Performance Computing
Research Projects
| 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 |
Resources Useful Links
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 |
Blogs
| Name | Notes |
|---|---|
| MIT PL Group Blog |