2 citations · 5 across the 9 of their papers we have counts for
11 papers
Step in Tine: Forking Processes in Functional Choreographies
Ashley Samuelson, Andrew K. Hirsch, Ethan Cecchetti
Traditional concurrent-programming techniques require programmers to painstakingly write programs for each participant in a concurrent system. Choreographic programming, in contras…
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…
Corps: A Core Calculus of Hierarchical Choreographic Programming
Andrew K. Hirsch
Functional choreographic programming suggests a new propositions-as-types paradigm might be possible. In this new paradigm, communication is not modeled linearly; instead, ownershi…
Alice or Bob?: Process Polymorphism in Choreographies
Eva Graversen, Andrew K. Hirsch, Fabrizio Montesi
We present PolyChor, a language for higher-order functional \emph{choreographic programming} -- an emerging paradigm by which programmers write the desired cooperative behaviour…
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…
First-Order Logic for Flow-Limited Authorization
Andrew K. Hirsch, Pedro H. Azevedo de Amorim, Ethan Cecchetti +2
We present the Flow-Limited Authorization First-Order Logic (FLAFOL), a logic for reasoning about authorization decisions in the presence of information-flow policies. We formalize…
Belief Semantics of Authorization Logic
Andrew K. Hirsch, Michael R. Clarkson
Authorization logics have been used in the theory of computer security to reason about access control decisions. In this work, a formal belief semantics for authorization logics is…
Nexus Authorization Logic (NAL): Logical Results
Andrew K. Hirsch, Michael R. Clarkson
Nexus Authorization Logic (NAL) [Schneider et al. 2011] is a logic for reasoning about authorization in distributed systems. A revised version of NAL is given here, including revis…