Papers, etc.

Conferences, journals, and selective workshops

Secure Information Flow for Concurrent Programs under Total Store Order Jeffrey A. Vaughan and Todd Millstein. CSF, 2012. [pdf]
(Proofs: UCLA Technical Report 120007 [pdf])

Inference of Expressive Declassification Policies. Jeffrey A. Vaughan and Stephen Chong. IEEE Security and Privacy (Oakland), 2011. [pdf | bib | slides]

AuraConf: A Unified Approach to Authorization and Confidentiality. Jeffrey A. Vaughan. TLDI, 2011. [pdf | slides | bib | coq]

Self-Identifying Sensor Data. Stephen Chong, Christian Skalka, and Jeffrey A. Vaughan. IPSN, 2010. [pdf | bib | slides]
Journal Version JDIQ, 2015. [pdf | bib]

Aura: A Programming Language for Authorization and Audit. Limin Jia, Jeffrey A. Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph Schorr, and Steve Zdancewic. ICFP, 2008. [pdf | bib | slides]
(Long version U. Pennsylvania Technical Report MS-CIS-08-10 [pdf])

Evidence-based Audit. Jeffrey A. Vaughan, Limin Jia, Karl Mazurak, and Steve Zdancewic. CSF, 2008. [pdf | bib | slides]
(Long version U. Pennsylvania Technical Report MS-CIS-08-09 [pdf])

A Cryptographic Decentralized Label Model. Jeffrey A. Vaughan and Steve Zdancewic. IEEE Security and Privacy (Oakland), 2007. [pdf | bib | slides]

Relational Lenses: A Language for Updateable Views. Aaron Bohannon, Jeffrey A. Vaughan and Benjamin C. Pierce. In Principles of Database Systems (PODS), 2006. [bib | pdf]
(Long version U. Pennsylvania Technical Report MS-CIS-05-27. [bib | pdf])

Factors Affecting Energy Deposition and Expansion in Single Wire Low Current Experiments. Peter U. Duselis, Jeffrey A. Vaughan, and Bruce R. Kusse. Physics of Plasmas 11, 4025 (2004). [pdf]


Aura: Programming with Authorization and Audit. Jeffrey A. Vaughan. Ph.D. Thesis, 2009. [pdf | bib | slides]

Other workshops

Dr. Android and Mr. Hide: Fine-grained Permissions in Android Applications. Jinseong Jeon, Kristopher K. Micinski, Jeffrey A. Vaughan, Ari Fogel, Nikhilesh Reddy, Jeffrey S. Foster, and Todd Millstein. Workshop on Security and Privacy in Smartphones and Mobile Devices (SPSM), 2012. [pdf]
(See also the .)

A Framework for Internalizing Relations into Type Theory. Peng Fu, Aaron Stump, and Jeffrey A. Vaughan. Workshop on Proof-Search in Axiomatic Theories and Type Theories (PSATTT), 2011. [pdf]

A logical interpretation of Java-style exceptions. Jeffrey A. Vaughan. Classical Logic and Computation (CL&C), 2010. [pdf | slides]

SML2Java: A Source to Source Translator. Justin Koser, Haakon Larsen, and Jeffrey A. Vaughan. Declarative Programming in the Context of Object-Oriented Languages (DP-COOL), 2003. [pdf | slides-pdf | slides-ppt]


Normalization in the Dual Calculus with Sigma Reductions. Jeffrey A. Vaughan, Stephanie Weirich, and Steve Zdancewic. For ICFP, Fall 2008. [pdf | abstract]

Relational Lenses: A Language for Defining Updateable Views. Aaron Bohannon, Jeffrey A. Vaughan, Benjamin C. Pierce. For DB/IR Day, Fall 2005. [pdf]

Notes and surveys

A Proof of Correctness for the Hindley-Milner Type Inference Algorithm. Notes, U. Pennsylvania, 2005 (revised 2008). [pdf]

A Review of Three Techniques for Formally Representing Variable Binding. Jeffrey A. Vaughan. Technical Report MS-CIS-06-19, U. Pennsylvania, Dec. 2006. (WPE-ii qualifying exam.) [bib | ps | pdf]

Plasma Formation Mechanisms in Exploding Wire Experiments. Notes, Cornell Institute for Plasma Studies, 2003. [pdf]