Nexus Authorization Logic (NAL): Logical Results - Andrew K. Hirsch; Michael R. Clarkson (CoRR, 2012)

Belief semantics of authorization logic. - Andrew K. Hirsch; Michael R. Clarkson (CCS, 2013)

Strict and lazy semantics for effects: layering monads and comonads. - Andrew K. Hirsch; Ross Tate (Proc. ACM Program. Lang., 2018)

Semantics for Secure Software. - Andrew K. Hirsch (2019)

First-Order Logic for Flow-Limited Authorization. - Andrew K. Hirsch; Pedro H. Azevedo de Amorim; Ethan Cecchetti; Ross Tate; Owen Arden (CSF, 2020)

Giving semantics to program-counter labels via secure effects. - Andrew K. Hirsch; Ethan Cecchetti (Proc. ACM Program. Lang., 2021)

Pirouette: higher-order typed functional choreographies. - Andrew K. Hirsch; Deepak Garg 001 (Proc. ACM Program. Lang., 2022)

Semantics for Noninterference with Interaction Trees. - Lucas Silver; Paul He; Ethan Cecchetti; Andrew K. Hirsch; Steve Zdancewic (ECOOP, 2023)

Semantics for Noninterference with Interaction Trees (Artifact). - Lucas Silver; Paul He; Ethan Cecchetti; Andrew K. Hirsch; Steve Zdancewic (Dagstuhl Artifacts Ser., 2023)

Compositional Security Definitions for Higher-Order Where Declassification. - Jan Menz; Andrew K. Hirsch; Peixuan Li; Deepak Garg 001 (Proc. ACM Program. Lang., 2023)

Corps: A Core Calculus of Hierarchical Choreographic Programming. - Andrew K. Hirsch (CoRR, 2024)

Alice or Bob?: Process polymorphism in choreographies. - Eva Graversen; Andrew K. Hirsch; Fabrizio Montesi (J. Funct. Program., 2024)

Choreographies as Macros. - Alexander Bohosian; Andrew K. Hirsch (PLACES@ETAPS, 2025)

Choreographic Quick Changes: First-Class Location (Set) Polymorphism. - Ashley Samuelson; Andrew K. Hirsch; Ethan Cecchetti (CoRR, 2025)