5 papers · 1 filter
Compositional security definitions for higher-order where declassification
Jan Menz, Andrew K. Hirsch, Peixuan Li +1
To ensure programs do not leak private data, we often want to be able to provide formal guarantees ensuring such data is handled correctly. Often, we cannot keep such data secret e…
Choreographic Quick Changes: First-Class Location (Set) Polymorphism
Ashley Samuelson, Andrew K. Hirsch, Ethan Cecchetti
Choreographic programming is a promising new paradigm for programming concurrent systems where a developer writes a single centralized program that compiles to individual programs…
Choreographies as Macros
Alexander Bohosian, Andrew K. Hirsch
Concurrent programming often entails meticulous pairing of sends and receives between participants to avoid deadlock. Choreographic programming alleviates this burden by specifying…
Pirouette: Higher-Order Typed Functional Choreographies
Andrew K. Hirsch, Deepak Garg
We present Pirouette, a language for typed higher-order functional choreographic programming. Pirouette offers programmers the ability to write a centralized functional program and…
Giving Semantics to Program-Counter Labels via Secure Effects
Andrew K. Hirsch, Ethan Cecchetti
Type systems designed for information-flow control commonly use a program-counter label to track the sensitivity of the context and rule out data leakage arising from effectful com…