-
Choreographies as Macros
Authors:
Alexander Bohosian,
Andrew K. Hirsch
Abstract:
Concurrent programming often entails meticulous pairing of sends and receives between participants to avoid deadlock. Choreographic programming alleviates this burden by specifying the system as a single program. However, there are more applications than implementations of choreographies, and developing new implementations takes a lot of time and effort. Our work uses Racket to expedite building a…
▽ More
Concurrent programming often entails meticulous pairing of sends and receives between participants to avoid deadlock. Choreographic programming alleviates this burden by specifying the system as a single program. However, there are more applications than implementations of choreographies, and developing new implementations takes a lot of time and effort. Our work uses Racket to expedite building a new choreographic language called Choret. Racket has a powerful macro system which allows Choret to reuse much of its infrastructure for greater functionality and correctness.
△ Less
Submitted 27 May, 2025;
originally announced May 2025.
-
Corps: A Core Calculus of Hierarchical Choreographic Programming
Authors:
Andrew K. Hirsch
Abstract:
Functional choreographic programming suggests a new propositions-as-types paradigm might be possible. In this new paradigm, communication is not modeled linearly; instead, ownership of a piece of data is modeled as a modality, and communication changes that modality. However, we must find an appropriate modal logic for the other side of the propositions-as-types correspondence. This paper argues f…
▽ More
Functional choreographic programming suggests a new propositions-as-types paradigm might be possible. In this new paradigm, communication is not modeled linearly; instead, ownership of a piece of data is modeled as a modality, and communication changes that modality. However, we must find an appropriate modal logic for the other side of the propositions-as-types correspondence. This paper argues for doxastic logics, or logics of belief. In particular, authorization logics -- doxastic logics with explicit communication -- appear to represent hierarchical choreographic programming. This paper introduces hierarchical choreographic programming and presents Corps, a language for hierarchical choreographic programming with a propositions-as-types interpretation in authorization logic.
△ Less
Submitted 3 June, 2024;
originally announced June 2024.
-
Alice or Bob?: Process Polymorphism in Choreographies
Authors:
Eva Graversen,
Andrew K. Hirsch,
Fabrizio Montesi
Abstract:
We present PolyChor$λ$, a language for higher-order functional \emph{choreographic programming} -- an emerging paradigm by which programmers write the desired cooperative behaviour of a system of communicating processes and then compile it into distributed implementations for each process, a translation called \emph{endpoint projection}. Unlike its predecessor, Chor$λ$, PolyChor$λ$ has both type a…
▽ More
We present PolyChor$λ$, a language for higher-order functional \emph{choreographic programming} -- an emerging paradigm by which programmers write the desired cooperative behaviour of a system of communicating processes and then compile it into distributed implementations for each process, a translation called \emph{endpoint projection}. Unlike its predecessor, Chor$λ$, PolyChor$λ$ has both type and \emph{process} polymorphism inspired by System F$_ω$. That is, PolyChor$λ$ is the first (higher-order) functional choreographic language which gives programmers the ability to write generic choreographies and determine the participants at runtime. This novel combination of features also allows PolyChor$λ$ processes to communicate \emph{distributed values}, leading to a new and intuitive way to write delegation. While some of the functional features of PolyChor$λ$ give it a weaker correspondence between the semantics of choreographies and their endpoint-projected concurrent systems than some other choreographic languages, we still get the hallmark end result of choreographic programming: projected programs are deadlock-free by design.
△ Less
Submitted 8 March, 2023;
originally announced March 2023.
-
Pirouette: Higher-Order Typed Functional Choreographies
Authors:
Andrew K. Hirsch,
Deepak Garg
Abstract:
We present Pirouette, a language for typed higher-order functional choreographic programming. Pirouette offers programmers the ability to write a centralized functional program and compile it via endpoint projection into programs for each node in a distributed system. Moreover, Pirouette is defined generically over a (local) language of messages, and lifts guarantees about the message type system…
▽ More
We present Pirouette, a language for typed higher-order functional choreographic programming. Pirouette offers programmers the ability to write a centralized functional program and compile it via endpoint projection into programs for each node in a distributed system. Moreover, Pirouette is defined generically over a (local) language of messages, and lifts guarantees about the message type system to its own. Message type soundness also guarantees deadlock freedom. All of our results are verified in Coq.
△ Less
Submitted 9 November, 2021; v1 submitted 5 November, 2021;
originally announced November 2021.
-
Giving Semantics to Program-Counter Labels via Secure Effects
Authors:
Andrew K. Hirsch,
Ethan Cecchetti
Abstract:
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 computation in a sensitive context. Currently, type-system designers reason about this label informally except in security proofs, where they use ad-hoc techniques. We develop a framework based on monadic semantics for effe…
▽ More
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 computation in a sensitive context. Currently, type-system designers reason about this label informally except in security proofs, where they use ad-hoc techniques. We develop a framework based on monadic semantics for effects to give semantics to program-counter labels. This framework leads to three results about program-counter labels. First, we develop a new proof technique for noninterference, the core security theorem for information-flow control in effectful languages. Second, we unify notions of security for different types of effects, including state, exceptions, and nontermination. Finally, we formalize the folklore that program-counter labels are a lower bound on effects. We show that, while not universally true, this folklore has a good semantic foundation.
△ Less
Submitted 10 December, 2020; v1 submitted 25 October, 2020;
originally announced October 2020.
-
First-Order Logic for Flow-Limited Authorization
Authors:
Andrew K. Hirsch,
Pedro H. Azevedo de Amorim,
Ethan Cecchetti,
Ross Tate,
Owen Arden
Abstract:
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 the FLAFOL proof system, characterize its proof-theoretic properties, and develop its security guarantees. In particular, FLAFOL is the first logic to provide a non-interference guarantee while supporting all connective…
▽ More
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 the FLAFOL proof system, characterize its proof-theoretic properties, and develop its security guarantees. In particular, FLAFOL is the first logic to provide a non-interference guarantee while supporting all connectives of first-order logic. Furthermore, this guarantee is the first to combine the notions of non-interference from both authorization logic and information-flow systems. All theorems in this paper are proven in Coq.
△ Less
Submitted 28 January, 2020;
originally announced January 2020.
-
Tunable energy and mass renormalization from homothetic Quantum dot arrays
Authors:
Ignacio Piquero-Zulaica Jun Li,
Zakaria M. Abd El-Fattah,
Leonid Solianyk,
Iker Gallardo,
Leticia Monjas,
Anna K. H. Hirsch,
Andres Arnau,
J. Enrique Ortega,
Meike Stohr,
Jorge Lobo-Checa
Abstract:
Quantum dot arrays in the form of molecular nanoporous networks are renown for modifying the electronic surface properties through quantum confinement. Here we show that, compared to the pristine surface state, the fundamental energy of the confined states can exhibit downward shifts accompanied by a lowering of the effective masses simultaneous to the appearance of tiny gaps at the Brillouin zone…
▽ More
Quantum dot arrays in the form of molecular nanoporous networks are renown for modifying the electronic surface properties through quantum confinement. Here we show that, compared to the pristine surface state, the fundamental energy of the confined states can exhibit downward shifts accompanied by a lowering of the effective masses simultaneous to the appearance of tiny gaps at the Brillouin zone boundaries. We observed these effects by angle resolved photoemission for two self-assembled homothetic (scalable) Co-coordinated metal-organic networks. Complementary scanning tunneling spectroscopy measurements confirmed these findings. Electron plane wave expansion simulations and density functional theory calculations provide insight into the nature of this phenomenon, which we assign to metal-organic overlayer-substrate interactions in the form of adatom-substrate hybridization. The absence to date of the experimental band structure resulting from single adatom metal-coordinated nanoporous networks has precluded the observation of the significant surface state renormalization reported here, which we infer are general of low interacting and well-defined adatom arrays.
△ Less
Submitted 15 October, 2019;
originally announced October 2019.
-
Belief Semantics of Authorization Logic
Authors:
Andrew K. Hirsch,
Michael R. Clarkson
Abstract:
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 given. The belief semantics is proved to subsume a standard Kripke semantics. The belief semantics yields a direct representation of principals' beliefs, without resorting to the technical machinery used in Kripke seman…
▽ More
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 given. The belief semantics is proved to subsume a standard Kripke semantics. The belief semantics yields a direct representation of principals' beliefs, without resorting to the technical machinery used in Kripke semantics. A proof system is given for the logic; that system is proved sound with respect to the belief and Kripke semantics. The soundness proof for the belief semantics, and for a variant of the Kripke semantics, is mechanized in Coq.
△ Less
Submitted 3 August, 2013; v1 submitted 8 February, 2013;
originally announced February 2013.
-
Nexus Authorization Logic (NAL): Logical Results
Authors:
Andrew K. Hirsch,
Michael R. Clarkson
Abstract:
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 revised syntax, a revised proof theory using localized hypotheses, and a new Kripke semantics. The proof theory is proved sound with respect to the semantics, and that proof is formalized in Coq.
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 revised syntax, a revised proof theory using localized hypotheses, and a new Kripke semantics. The proof theory is proved sound with respect to the semantics, and that proof is formalized in Coq.
△ Less
Submitted 15 November, 2012; v1 submitted 15 November, 2012;
originally announced November 2012.
