Henry DeYoung

E-mail: hdey...@cs...
Personal E-mail: henr...@gmail...
Office: GHC 9002
Office Phone: +1 (412) 268-3069

I am a fifth-year Ph.D. student in the Computer Science Department at Carnegie Mellon University, advised by Frank Pfenning.

Previously, I was an computer science undergraduate at Carnegie Mellon, advised by Frank Pfenning on an undergraduate thesis on η logic, an authorization logic with explicit time.

Research Interests

I am generally interested in logic and programming languages.

  • Proof theory and Martin-Löf's judgmental approach
  • Languages and logics for security
  • Proof checkers for teaching logic
  • Mechanized metatheory


I am currently working with Frank Pfenning and Michael Ashley-Rollman on a logic programming interpretation of linear epistemic logic for writing secure distributed programs. Our preliminary results on reasoning about the consequences of authorization policies in linear epistemic logic appeared at FCS 2009.

I am also working with Carsten Schürmann on using linear logic for electronic voting. Our preliminary results appeared at VoteID 2011 and include a specification of the single transferable vote protocol in linear logic.

I have previously worked with Anupam Datta and his group on extensions to a logic for modeling privacy regulations. Our results of formalizing HIPAA and GLBA in the logic appeared at WPES 2010.


Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication
Henry DeYoung, Luís Caires, Frank Pfenning, Bernardo Toninho.
21st Annual Conference of the European Association for Computer Science Logic, September 2012.
To appear. Slides
Understanding and Protecting Privacy: Formal Semantics and Principled Audit Mechanisms
Anupam Datta, Jeremiah Blocki, Nicolas Christin, Henry DeYoung, Deepak Garg, Limin Jia, Dilsun Kaynar, Arunesh Sinha.
7th International Conference on Information Systems Security (ICISS), pages 1-27, Kolkata, India, December 2011.
Linear Logical Voting Protocols
Henry DeYoung and Carsten Schürmann.
3rd International Conference on E-voting and Identity (VoteID), Tallinn, Estonia, September 2011. Slides
Experiences in the Logical Specification of the HIPAA and GLBA Privacy Laws
Henry DeYoung, Deepak Garg, Limin Jia, Dilsun Kaynar, and Anupam Datta.
9th ACM Workshop on Privacy in the Electronic Society (WPES), October 2010.
Extended version available as Technical Report CMU-CyLab-10-007, April 2010.
Privacy Policy Specification and Audit in a Fixed-Point Logic – How to enforce HIPAA, GLBA and all that
Henry DeYoung, Deepak Garg, Limin Jia, Dilsun Kaynar, Anupam Datta.
Technical Report CMU-CyLab-10-008, May 2010.
Reasoning about the Consequences of Authorization Policies in a Linear Epistemic Logic
Henry DeYoung and Frank Pfenning.
Workshop on Foundations of Computer Security (FCS), Los Angeles, California, August 2009.
An Authorization Logic with Explicit Time
Henry DeYoung, Deepak Garg, and Frank Pfenning.
21st IEEE Computer Security Foundations Symposium (CSF).
Pittsburgh, Pennsylvania. June, 2008.
Long version with detailed proofs available as Technical Report CMU-CS-07-166.
A Logic for Reasoning About Time-Dependent Access Control Policies
Henry DeYoung.
Senior Research Thesis.
Carnegie Mellon University, May 2008.
Available as Technical Report CMU-CS-08-131.


Linear Logical Voting Protocols
Speaking Skills Requirement.
Carnegie Mellon University. April 2013.
Reasoning about the Consequences of Authorization Policies in a Linear Epistemic Logic
Manifest Security Meeting.
Carnegie Mellon University. May 2009.

Miscellaneous Documents

Reasoning about the Consequences of Authorization Policies in a Linear Epistemic Logic Technical Report
A draft technical report corresponding to the FCS 2009 paper.
A catalog of commuting conversions for linear logic
Comparison of commuting conversions and π-calculus process conversions.

Other Interests