Effective Chemistry for Synchrony and Asynchrony. - Deepak Garg 001; Akash Lal; Sanjiva Prasad (IFIP TCS, 2004)

Type-Directed Concurrency. - Deepak Garg 001; Frank Pfenning (CONCUR, 2005)

Non-Interference in Constructive Authorization Logic. - Deepak Garg 001; Frank Pfenning (CSFW, 2006)

A Linear Logic of Authorization and Knowledge. - Deepak Garg 001; Lujo Bauer; Kevin D. Bowers; Frank Pfenning; Michael K. Reiter (ESORICS, 2006)

Consumable Credentials in Linear-Logic-Based Access-Control Systems. - Kevin D. Bowers; Lujo Bauer; Deepak Garg 001; Frank Pfenning; Michael K. Reiter (NDSS, 2007)

An Authorization Logic With Explicit Time. - Henry DeYoung; Deepak Garg 001; Frank Pfenning (CSF, 2008)

A Modal Deconstruction of Access Control Logics. - Deepak Garg 001; Martín Abadi (FoSSaCS, 2008)

PCAL: Language Support for Proof-Carrying Authorization Systems. - Avik Chaudhuri; Deepak Garg 001 (ESORICS, 2009)

A Logic of Secure Systems and its Application to Trusted Computing. - Anupam Datta; Jason Franklin; Deepak Garg 001; Dilsun Kirli Kaynar (SP, 2009)

A Proof-Carrying File System. - Deepak Garg 001; Frank Pfenning (IEEE Symposium on Security and Privacy, 2010)

Experiences in the logical specification of the HIPAA and GLBA privacy laws. - Henry DeYoung; Deepak Garg 001; Limin Jia 001; Dilsun Kirli Kaynar; Anupam Datta (WPES, 2010)

Compositional System Security with Interface-Confined Adversaries. - Deepak Garg 001; Jason Franklin; Dilsun Kirli Kaynar; Anupam Datta (MFPS, 2010)

Policy auditing over incomplete logs: theory, implementation and applications. - Deepak Garg 001; Limin Jia 001; Anupam Datta (CCS, 2011)

Understanding and Protecting Privacy: Formal Semantics and Principled Audit Mechanisms. - Anupam Datta; Jeremiah Blocki; Nicolas Christin; Henry DeYoung; Deepak Garg 001; Limin Jia 001; Dilsun Kirli Kaynar; Arunesh Sinha (ICISS, 2011)

Verification of Information Flow and Access Control Policies with Dependent Types. - Aleksandar Nanevski; Anindya Banerjee 001; Deepak Garg 001 (IEEE Symposium on Security and Privacy, 2011)

New Modalities for Access Control Logics: Permission, Control and Ratification. - Valerio Genovese; Deepak Garg 001 (STM, 2011)

A Proof-Carrying File System with Revocable and Use-Once Certificates. - Jamie Morgenstern; Deepak Garg 001; Frank Pfenning (STM, 2011)

A Logical Method for Policy Enforcement over Evolving Audit Logs - Deepak Garg 001; Limin Jia 001; Anupam Datta (CoRR, 2011)

On Adversary Models and Compositional Security. - Anupam Datta; Jason Franklin; Deepak Garg 001; Limin Jia 001; Dilsun Kirli Kaynar (IEEE Secur. Priv., 2011)

Labeled Sequent Calculi for Access Control Logics: Countermodels, Saturation and Abduction. - Valerio Genovese; Deepak Garg 001; Daniele Rispoli (CSF, 2012)

Superficially substructural types. - Neelakantan R. Krishnaswami; Aaron Turon; Derek Dreyer; Deepak Garg 001 (ICFP, 2012)

Countermodels from Sequent Calculi in Multi-Modal Logics. - Deepak Garg 001; Valerio Genovese; Sara Negri (LICS, 2012)

Labeled Goal-Directed Search in Access Control Logic. - Valerio Genovese; Deepak Garg 001; Daniele Rispoli (STM, 2012)

Stateful authorization logic - Proof theory and a case study. - Deepak Garg 001; Frank Pfenning (J. Comput. Secur., 2012)

Dependent Type Theory for Verification of Information Flow and Access Control Policies. - Aleksandar Nanevski; Anindya Banerjee 001; Deepak Garg 001 (ACM Trans. Program. Lang. Syst., 2013)

Temporal Mode-Checking for Runtime Monitoring of Privacy Policies. - Omar Chowdhury; Limin Jia 001; Deepak Garg 001; Anupam Datta (CAV, 2014)

Privacy-preserving audit for broker-based health information exchange. - Se Eun Oh; Ji Young Chun; Limin Jia 001; Deepak Garg 001; Carl A. Gunter; Anupam Datta (CODASPY, 2014)

Generalizing Permissive-Upgrade in Dynamic Information Flow Analysis. - Abhishek Bichhawat; Vineet Rajani; Deepak Garg 001; Christian Hammer 001 (PLAS@ECOOP, 2014)

Information Flow Control in WebKit's JavaScript Bytecode. - Abhishek Bichhawat; Vineet Rajani; Deepak Garg 001; Christian Hammer 001 (POST, 2014)

Equivalence-based Security for Querying Encrypted Databases: Theory and Application to Privacy Policy Audits. - Omar Chowdhury; Deepak Garg 001; Limin Jia 001; Anupam Datta (CCS, 2015)

Program Actions as Actual Causes: A Building Block for Accountability. - Anupam Datta; Deepak Garg 001; Dilsun Kirli Kaynar; Divya Sharma; Arunesh Sinha (CSF, 2015)

A Logic of Programs with Interface-Confined Code. - Limin Jia 001; Shayak Sen; Deepak Garg 001; Anupam Datta (CSF, 2015)

Information Flow Control for Event Handling and the DOM in Web Browsers. - Vineet Rajani; Abhishek Bichhawat; Deepak Garg 001; Christian Hammer 001 (CSF, 2015)

Refinement Types for Incremental Computational Complexity. - Ezgi Çiçek; Deepak Garg 001; Umut A. Acar (ESOP, 2015)

Guardat: enforcing data policies at the storage layer. - Anjo Vahldiek-Oberwagner; Eslam Elnikety; Aastha Mehta; Deepak Garg 001; Peter Druschel; Rodrigo Rodrigues 001; Johannes Gehrke; Ansley Post (EuroSys, 2015)

System M: A Program Logic for Code Sandboxing and Identification. - Limin Jia 001; Shayak Sen; Deepak Garg 001; Anupam Datta (CoRR, 2015)

Causally Consistent Dynamic Slicing. - Roly Perera; Deepak Garg 001; James Cheney (CONCUR, 2016)

On Access Control, Capabilities, Their Equivalence, and Confused Deputy Attacks. - Vineet Rajani; Deepak Garg 001; Tamara Rezk (CSF, 2016)

Progress-Sensitive Security for SPARK. - Willard Rafnsson; Deepak Garg 001; Andrei Sabelfeld (ESSoS, 2016)

A type theory for incremental computational complexity with control flow changes. - Ezgi Çiçek; Zoe Paraskevopoulou; Deepak Garg 001 (ICFP, 2016)

Light-Weight Contexts: An OS Abstraction for Safety and Performance. - James Litton; Anjo Vahldiek-Oberwagner; Eslam Elnikety; Deepak Garg 001; Bobby Bhattacharjee; Peter Druschel (OSDI, 2016)

Asymmetric Secure Multi-execution with Declassification. - Iulia Bolosteanu; Deepak Garg 001 (POST, 2016)

Thoth: Comprehensive Policy Compliance in Data Retrieval Systems. - Eslam Elnikety; Aastha Mehta; Anjo Vahldiek-Oberwagner; Deepak Garg 001; Peter Druschel (USENIX Security Symposium, 2016)

Secure Compilation and Hyperproperty Preservation. - Marco Patrignani; Deepak Garg 001 (CSF, 2017)

WebPol: Fine-Grained Information Flow Policies for Web Browsers. - Abhishek Bichhawat; Vineet Rajani; Jinank Jain; Deepak Garg 001; Christian Hammer 001 (ESORICS (1), 2017)

Relational cost analysis. - Ezgi Çiçek; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Jan Hoffmann 002 (POPL, 2017)

Qapla: Policy compliance for database-backed systems. - Aastha Mehta; Eslam Elnikety; Katura Harvey; Deepak Garg 001; Peter Druschel (USENIX Security Symposium, 2017)

Robust Hyperproperty Preservation for Secure Compilation (Extended Abstract). - Deepak Garg 001; Catalin Hritcu; Marco Patrignani; Marco Stronati; David Swasey (CoRR, 2017)

An Instrumenting Compiler for Enforcing Confidentiality in Low-Level Code. - Ajay Brahmakshatriya; Piyus Kedia; Derrick Paul McKee; Pratik Bhatu; Deepak Garg 001; Akash Lal; Aseem Rastogi (CoRR, 2017)

Encrypting Messages for Incomplete Chains of Certificates. - Sanjit Chatterjee; Deepak Garg 001; Aniket Kate; Tobias Theobald (IACR Cryptol. ePrint Arch., 2017)

A relational logic for higher-order programs. - Alejandro Aguirre 001; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Pierre-Yves Strub (Proc. ACM Program. Lang., 2017)

Robust and compositional verification of object capability patterns. - David Swasey; Deepak Garg 001; Derek Dreyer (Proc. ACM Program. Lang., 2017)

Type systems for information flow control: the question of granularity. - Vineet Rajani; Iulia Bastys; Willard Rafnsson; Deepak Garg 001 (ACM SIGLOG News, 2017)

Types for Information Flow Control: Labeling Granularity and Semantic Models. - Vineet Rajani; Deepak Garg 001 (CSF, 2018)

Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. - Alejandro Aguirre 001; Gilles Barthe; Lars Birkedal; Ales Bizjak; Marco Gaboardi; Deepak Garg 001 (ESOP, 2018)

UniTraX: Protecting Data Privacy with Discoverable Biases. - Reinhard Munz; Fabienne Eigner; Matteo Maffei; Paul Francis; Deepak Garg 001 (POST, 2018)

Shai: Enforcing Data-Specific Policies with Near-Zero Runtime Overhead. - Eslam Elnikety; Deepak Garg 001; Peter Druschel (CoRR, 2018)

ERIM: Secure and Efficient In-process Isolation with Memory Protection Keys. - Anjo Vahldiek-Oberwagner; Eslam Elnikety; Deepak Garg 001; Peter Druschel (CoRR, 2018)

Robustly Safe Compilation or, Efficient, Provably Secure Compilation. - Marco Patrignani; Deepak Garg 001 (CoRR, 2018)

Exploring Robust Property Preservation for Secure Compilation. - Carmine Abate; Roberto Blanco; Deepak Garg 001; Catalin Hritcu; Marco Patrignani; Jérémy Thibault (CoRR, 2018)

Formal verification of higher-order probabilistic programs. - Tetsuya Sato 001; Alejandro Aguirre 001; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Justin Hsu (CoRR, 2018)

SATE: Robust and Private Allegation Escrows. - Venkat Arun; Aniket Kate; Deepak Garg 001; Peter Druschel; Bobby Bhattacharjee (CoRR, 2018)

Secure Compilation (Dagstuhl Seminar 18201). - Amal Ahmed 001; Deepak Garg 001; Catalin Hritcu; Frank Piessens (Dagstuhl Reports, 2018)

Accountability in Security Protocols. - Robert Künnemann; Deepak Garg 001; Michael Backes 001 (IACR Cryptol. ePrint Arch., 2018)

Monadic refinements for relational cost analysis. - Ivan Radicek; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Florian Zuleger (Proc. ACM Program. Lang., 2018)

Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation. - Carmine Abate; Roberto Blanco; Deepak Garg 001; Catalin Hritcu; Marco Patrignani; Jérémy Thibault (CSF, 2019)

Robustly Safe Compilation. - Marco Patrignani; Deepak Garg 001 (ESOP, 2019)

ConfLLVM: A Compiler for Enforcing Data Confidentiality in Low-Level Code. - Ajay Brahmakshatriya; Piyus Kedia; Derrick Paul McKee; Deepak Garg 001; Akash Lal; Aseem Rastogi; Hamed Nemati; Anmol Panda; Pratik Bhatu (EuroSys, 2019)

Composing Abstractions using the null-Kernel. - James Litton; Deepak Garg 001; Peter Druschel; Bobby Bhattacharjee (HotOS, 2019)

Bidirectional type checking for relational properties. - Ezgi Çiçek; Weihao Qu; Gilles Barthe; Marco Gaboardi; Deepak Garg 001 (PLDI, 2019)

ERIM: Secure, Efficient In-process Isolation with Protection Keys (MPK). - Anjo Vahldiek-Oberwagner; Eslam Elnikety; Nuno O. Duarte; Michael Sammler; Peter Druschel; Deepak Garg 001 (USENIX Security Symposium, 2019)

Trace-Relating Compiler Correctness and Secure Compilation. - Carmine Abate; Roberto Blanco; Stefan Ciobaca; Deepak Garg 001; Catalin Hritcu; Marco Patrignani; Éric Tanter; Jérémy Thibault (CoRR, 2019)

Pacer: Network Side-Channel Mitigation in the Cloud. - Aastha Mehta; Mohamed Alzayat; Roberta De Viti; Björn B. Brandenburg; Peter Druschel; Deepak Garg 001 (CoRR, 2019)

Causality & Control Flow. - Robert Künnemann; Deepak Garg 001; Michael Backes 001 (CREST@ETAPS, 2019)

Relational cost analysis for functional-imperative programs. - Weihao Qu; Marco Gaboardi; Deepak Garg 001 (Proc. ACM Program. Lang., 2019)

Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization. - Tetsuya Sato 001; Alejandro Aguirre 001; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Justin Hsu (Proc. ACM Program. Lang., 2019)

Trace-Relating Compiler Correctness and Secure Compilation. - Carmine Abate; Roberto Blanco; Stefan Ciobaca; Adrien Durier; Deepak Garg 001; Catalin Hritcu; Marco Patrignani; Éric Tanter; Jérémy Thibault (ESOP, 2020)

Finding Safety in Numbers with Secure Allegation Escrows. - Venkat Arun; Aniket Kate; Deepak Garg 001; Peter Druschel; Bobby Bhattacharjee (NDSS, 2020)

PanCast: Listening to Bluetooth Beacons for Epidemic Risk Mitigation. - Gilles Barthe; Roberta De Viti; Peter Druschel; Deepak Garg 001; Manuel Gomez-Rodriguez; Pierfrancesco Ingo; Matthew Lentz; Aastha Mehta; Bernhard Schölkopf (CoRR, 2020)

On the expressiveness and semantics of information flow types. - Vineet Rajani; Deepak Garg 001 (J. Comput. Secur., 2020)

The high-level benefits of low-level sandboxing. - Michael Sammler; Deepak Garg 001; Derek Dreyer; Tadeusz Litak (Proc. ACM Program. Lang., 2020)

CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle. - Akram El-Korashy; Stelios Tsampas 001; Marco Patrignani; Dominique Devriese; Deepak Garg 001; Frank Piessens (CSF, 2021)

Accountability in the Decentralised-Adversary Setting. - Robert Künnemann; Deepak Garg 001; Michael Backes 001 (CSF, 2021)

RefinedC: automating the foundational verification of C code with refined ownership types. - Michael Sammler; Rodolphe Lepigre; Robbert Krebbers; Kayvan Memarian; Derek Dreyer; Deepak Garg 001 (PLDI, 2021)

Isolation Without Taxation: Near Zero Cost Transitions for SFI. - Matthew Kolosick; Shravan Narayan; Conrad Watt; Michael LeMay; Deepak Garg 001; Ranjit Jhala; Deian Stefan (CoRR, 2021)

Secure Compilation (Dagstuhl Seminar 21481). - David Chisnall; Deepak Garg 001; Catalin Hritcu; Mathias Payer (Dagstuhl Reports, 2021)

Permissive runtime information flow control in the presence of exceptions. - Abhishek Bichhawat; Vineet Rajani; Deepak Garg 001; Christian Hammer 001 (J. Comput. Secur., 2021)

Relational cost analysis in a functional-imperative setting. - Weihao Qu; Marco Gaboardi; Deepak Garg 001 (J. Funct. Program., 2021)

Higher-order probabilistic adversarial computations: categorical semantics and program logics. - Alejandro Aguirre 001; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Shin-ya Katsumata; Tetsuya Sato 001 (Proc. ACM Program. Lang., 2021)

A unifying type-theory for higher-order (amortized) cost analysis. - Vineet Rajani; Marco Gaboardi; Deepak Garg 001; Jan Hoffmann 002 (Proc. ACM Program. Lang., 2021)

An Extended Account of Trace-relating Compiler Correctness and Secure Compilation. - Carmine Abate; Roberto Blanco; Stefan Ciobaca; Adrien Durier; Deepak Garg 001; Catalin Hritcu; Marco Patrignani; Éric Tanter; Jérémy Thibault (ACM Trans. Program. Lang. Syst., 2021)

Robustly Safe Compilation, an Efficient Form of Secure Compilation. - Marco Patrignani; Deepak Garg 001 (ACM Trans. Program. Lang. Syst., 2021)

SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation. - Akram El-Korashy; Roberto Blanco; Jérémy Thibault; Adrien Durier; Deepak Garg 001; Catalin Hritcu (CSF, 2022)

Islaris: verification of machine code against authoritative ISA semantics. - Michael Sammler; Angus Hammond; Rodolphe Lepigre; Brian Campbell 001; Jean Pichon-Pharabod; Derek Dreyer; Deepak Garg 001; Peter Sewell (PLDI, 2022)

Pacer: Comprehensive Network Side-Channel Mitigation in the Cloud. - Aastha Mehta; Mohamed Alzayat; Roberta De Viti; Björn B. Brandenburg; Peter Druschel; Deepak Garg 001 (USENIX Security Symposium, 2022)

CoVault: A Secure Analytics Platform. - Roberta De Viti; Isaac Sheff; Noemi Glaeser; Baltasar Dinis; Rodrigo Rodrigues 001; Jonathan Katz; Bobby Bhattacharjee; Anwar Hithnawi; Deepak Garg 001; Peter Druschel (CoRR, 2022)

From Fine- to Coarse-Grained Dynamic Information Flow Control and Back, a Tutorial on Dynamic Information Flow. - Marco Vassena; Alejandro Russo; Deepak Garg 001; Vineet Rajani; Deian Stefan (CoRR, 2022)

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

Isolation without taxation: near-zero-cost transitions for WebAssembly and SFI. - Matthew Kolosick; Shravan Narayan; Evan Johnson 001; Conrad Watt; Michael LeMay; Deepak Garg 001; Ranjit Jhala; Deian Stefan (Proc. ACM Program. Lang., 2022)

BFF: foundational and automated verification of bitfield-manipulating programs. - Fengmin Zhu; Michael Sammler; Rodolphe Lepigre; Derek Dreyer; Deepak Garg 001 (Proc. ACM Program. Lang., 2022)

Groundhog: Efficient Request Isolation in FaaS. - Mohamed Alzayat; Jonathan Mace; Peter Druschel; Deepak Garg 001 (EuroSys, 2023)

Blueprint: A Toolchain for Highly-Reconfigurable Microservice Applications. - Vaastav Anand; Deepak Garg 001; Antoine Kaufmann; Jonathan Mace (SOSP, 2023)

From Fine- to Coarse-Grained Dynamic Information Flow Control and Back. - Marco Vassena; Alejandro Russo; Deepak Garg 001; Vineet Rajani; Deian Stefan (Found. Trends Program. Lang., 2023)

DimSum: A Decentralized Approach to Multi-language Semantics and Verification. - Michael Sammler; Simon Spies; Youngju Song; Emanuele D'Osualdo; Robbert Krebbers; Deepak Garg 001; Derek Dreyer (Proc. ACM Program. Lang., 2023)

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

Toast: A Heterogeneous Memory Management System. - Maurice Bailleu; Dimitrios Stavrakakis; Rodrigo Caetano Rocha; Soham Chakraborty 001; Deepak Garg 001; Pramod Bhatotia (PACT, 2024)

ProLoc: Robust Location Proofs in Hindsight. - Roberta De Viti; Pierfrancesco Ingo; Isaac Sheff; Peter Druschel; Deepak Garg 001 (CoRR, 2024)

Program Analysis for Adaptive Data Analysis. - Jiawen Liu; Weihao Qu; Marco Gaboardi; Deepak Garg 001; Jonathan R. Ullman (Proc. ACM Program. Lang., 2024)

A Modal Type Theory of Expected Cost in Higher-Order Probabilistic Programs. - Vineet Rajani; Gilles Barthe; Deepak Garg 001 (Proc. ACM Program. Lang., 2024)

RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers. - Kimaya Bedarkar; Laila Elbeheiry; Michael Sammler; Lennard Gäher; Björn B. Brandenburg; Derek Dreyer; Deepak Garg 001 (Proc. ACM Program. Lang., 2025)

Towards Online Code Specialization of Systems. - Vaastav Anand; Deepak Garg 001; Antoine Kaufmann (CoRR, 2025)