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]
A Confidentiality Extension to the Aura Programming Language. 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]
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]
Thesis
Aura: Programming with Authorization and Audit. Jeffrey A. Vaughan. Ph.D. Thesis, 2009. [pdf | bib | slides]
Other workshops
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]
Papers in preparation
A Platform for Expressive and Secure Data Sharing with Untrusted Third Parties Eric Griffis, Jeffrey A. Vaughan, and Todd Millstein. Working Paper, 2011. [pdf]
Inference of Usable Declassification Policies. Jeffrey A. Vaughan and Stephen Chong. Working paper, 2010. [pdf]
Paladin: Helping Programs Help Themselves with System Call Interposition. Jeffrey A. Vaughan and Andrew D. Hilton. Working paper, 2009. [pdf]
Posters
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]