Research Papers – 2011 onwards

• Object Capability Policies

  • Holistic Specifications for Robust Programs, by Drossopoulou, Noble, Mackay, and Eisenbach, full version in arxiv, shorter version published at FASE 2020
  • by Swapsies on the Internet – First steps towards Reasoning about Risk and Trust in the Open World, by Drossopoulou, Noble and Miller — accepted at PLAS 2015.A recent talk, with more results can be found here.
  • How to Break the Bank: Semantics of Capability Policies, by  Drossopoulou and Noble  —  iFM’14, pages 18-35.
  • Rationally Reconstructing the Escrow Example, by Noble and Drossopoulou  —  FTfJP 2014
  • The Need for Capability Policies, by Drossopoulou and Noble, FTfJP 2013
  • Policy as Types, by Meredith, Stay, and Drossopoulou, CoRR abs/1307.7766 (2013)
  • Towards Capability Policy Specification and Verification, – version II by Drossopoulou and Noble —  and Reasoning about Risk and Trust in the Open World, by Drossopoulou, Noble, Murray, and Miller, work in progress.

• Concurrent Programming, Pony, Garbage Collection
  

  • Deny Capabilities for safe, fast actors, by Clebsch, Drossopoulou, Blessing, and McNeil  — accepted at AGERE!-splash2015.
    A more detailed, yet unpublished older version can be found here. A talk that animates some of these aspects, given at IFIP WG2.16: in *.pptx format, and in *.pdf format,
  • Ownership and Reference Counting based Garbage Collection in the Actor World, by Clebsch, Blessing, Franco and Drossopoulou — accepted at ICOOLPS 2015
  • Fully Concurrent Garbage Collection of Actors on Many-Core Machines, by Clebsch and Drossopoulou, OOPSLA 2013;
    slides here
  • Orca: GC and Type System Co-Design for Actor Languages, by Clebsch, Franco, Drossopoulou, Yang, Wrigstad and Vitek, OOPSLA2017
  • Correctness of a Concurrent Object Collector for Actor Languages, Juliana Franco, Sylvan Clebsch, Sophia Drossopoulou, Jan Vitek, and Tobias Wrigstad. ESOP’18   [full version]
  • Tree Topologies for Causal Message Delivery, by Blessing, Clebsch and Drossopoulou, AGERE 2017
  • snmalloc: a message passing allocator, Paul Liétar, Theodore Butler, Sylvan Clebsch, Sophia Drossopoulou, Juliana Franco, Matthew J. Parkinson, Alex Shamis, Christoph M. Wintersteiger, David Chisnall, ISMM 2019
  • Run Actor, Run, Sebastian Blessing, Tobias Wrigstad, and Sophia Drossopoulou, CurryON 2019, . and also
    Run Actor, Run, Sebastian Blessing, Kiko Fernandez, Albert Netymk, Tobias Wrigstad, and Sophia Drossopoulou, AGERE 2019.

• Types for Locality and Performance

  • Towards Enabling Low-Level Memory Optimisations at the High-Level with Ownership Annotations. , by Juliana Franco, Tobias Wrigstad and Sophia Drossopoulou. IWACO 2016
  • You can have it all: Abstraction and good cache Performance, by Franco, Hagelin, Wrigstand, Drossopoulou, and Eisenbach, Onward! 2017
  • Extending SHAPES for SIMD Architectures: An approach to native support for Struct of Arrays in language, by Alexandros Tasos, Juliana Franco, Tobias Wrigstad, Sophia Drossopoulou, Susan Eisenbach, ICOOOLPS@ECOOP 2018:.
  • Safely Abstracting Memory Layouts, by Juliana Franco, Alexandros Tasos, Sophia Drossopoulou, Tobias Wrigstad, Susan Eisenbach, CoRR abs/1901.08006 (2019).

• Program Verification
  • A Formal Semantics for Isorecursive and Equirecursive State Abstractions, by Summers and Drossopoulou, ECOOP 2013
  • A Sip of the Chalice, by Raad and Drossopoulou, FTfJP 2011

• Theorem Proving
  • Zeno: An automated prover for properties of recursive data structures, by Sonnex, Drossopoulou and Eisenbach, TACAS 2012

• Session and Behavioural Types
  • Behavioural Types for Numa, by Juliana Franco and Sophia Drossopoulou, PLACES’15
    Calculating Communications Costs with Session Types and Sizes, Juliana Franco and Sophia Drossopoulou, ICSSW;14
  • Automatic Generation of Self-monitoring MASs from Multiparty Global Session Types in Jason, by Ancona, Drossopoulou and Mascardi, DALT 2012: 76-95
• Characterization of Program Evolution
  • Modular Verification of Procedure Equivalance in the Presence of Memory Allocation, by Wood, Drossopoulou, Lahiri and Eisenbah, ESOP 2017, Upsalla
  • Program Equivalence through Trace Equivalence, by Wood and Drossopoulou, FOOL 2014
  • Refactoring Boundary,   by Wood and Drossopoulou, ICCSW 2013
• Ownership Types
  • Understanding Ownership Types with Dependent Types,  by Cameron, Drossopoulou, and Noble, Aliasing in Object-Oriented Programming 2013: 84-108, LNCS
  • Separating ownership topology and encapsulation with generic universe types, by Dietl,  Drossopoulou, and Müller,  ACM Trans. Program. Lang. Syst. 33(6): 20 (2011)
  • The Roles of Owners, by Clarke, Drossopoulou and Noble, IWACO 2011
  • Smart Contracts
    • Writing Safe  Smart Contracts in Flint, Franklin Schrans, Susan Eisenbach, Sophia Drossopoulou, Programming 2018

Older papers can be found here.