Principles of Programming Group

Computer Science Department

Carnegie Mellon University


Research Projects

Project Faculty Description
Principles of Parallel Computing Umut Acar
Data Centric Computation Umut Acar
Semantics of Concurrent Programs Stephen Brookes Denotational semantics for weak memory concurrency and logics for proving program correctness
Typecoin Karl Crary Peer-to-peer linear commitment using the Bitcoin network
Languages (1,2) for Computer Music Roger Dannenberg Programming languages to address timing, gestural control, concurrency, and signal processing for computer music applications
Compositional Security Anupam Datta Programming language methods to support modular construction and analysis of cryptographic protocols and systems software
Privacy Through Accountability Anupam Datta Theories and tools for oversight of personal information processing systems (including big data programs) to ensure privacy, fairness, and other values threatened by unfettered collection and use of personal information.
Security, Privacy, and Inference Matt Fredrikson Formal approaches for reasoning about security and privacy in statistical learning applications
Models for Privacy-Aware Programming Matt Fredrikson Theory, tools, and language-based techniques that simplify the task of writing correct privacy-aware code
Higher Type Theory Robert Harper Theory and application of higher type theory
Resource Aware ML Jan Hoffmann A programming language that statically infers symbolic resource-usage bounds
CURB Jan Hoffmann A DARPA STAC project that uses resource bounds to detect space/time vulnerabilities in Java bytecode
Session-Typed Concurrency Frank Pfenning, Stephanie Balzer Programming languages and logics based on session-typed message-passing concurrent computation
KeYmaera X André Platzer KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems
Logical Foundations of CPS André Platzer Develops logical foundations for cyber-physical systems, i.e., systems that combine cyber aspects such as communication and computer control with physical aspects such as movement in space
HA-Spiral André Platzer Verified synthesis of high assurance implementations of controllers for vehicular systems
Policy-Agnostic Programming Jean Yang A programming model for separating privacy and security policies from other computations