About Me

I am a PhD student in the Computer Science Department at Carnegie Mellon University, advised by Frank Pfenning. My thesis research is on proof-theoretic foundations of session-typed concurrency.  Previously, I was a computer science undergraduate at Carnegie Mellon, advised by Frank Pfenning.

Peer-Reviewed Publications

Semi-Axiomatic Sequent Calculus - Henry DeYoung, Frank Pfenning, and Klaas Pruiksma. 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020. 29:1-29:22. DOI
Substructural Proofs as Automata - Henry DeYoung and Frank Pfenning. 14th Asian Symposium on Programming Languages and Systems, APLAS 2016. 3-22. DOI
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, CSL 2012. 228-242. DOI
Understanding and Protecting Privacy: Formal Semantics and Principled Audit Mechanisms - Anupam Datta, Jeremiah Blocki, Nicolas Christin, Henry DeYoung, Deepak Garg, Limin Jia, Dilsun Kırlı Kaynar, and Arunesh Sinha. 7th International Conference on Information Systems Security, ICISS 2011. 1-27. DOI
Linear Logical Voting Protocols - Henry DeYoung and Carsten Schürmann. 7th International Conference on E-Voting and Identity, VoteID 2011. 53-70. DOI
Experiences in the Logical Specification of the HIPAA and GLBA Privacy Laws - Henry DeYoung, Deepak Garg, Limin Jia, Dilsun Kırlı Kaynar, and Anupam Datta. 2010 ACM Workshop on Privacy in the Electronic Society, WPES 2010. 73-82. DOI
Reasoning About the Consequences of Authorization Policies in a Linear Epistemic Logic - Henry DeYoung and Frank Pfenning. Workshop on Foundations of Computer Security, FCS 2009.
An Authorization Logic With Explicit Time - Henry DeYoung, Deepak Garg, and Frank Pfenning. 21st IEEE Computer Security Foundations Symposium, CSF 2008. 133-145. DOI

Other Writings

Session-Typed Ordered Logical Specifications - Henry DeYoung. PhD thesis, December 2020.
Session-Typed Concurrent Logical Specifications - Henry DeYoung. PhD thesis proposal.


Music: Neapolitan partimento theory, 18th century composition;
Board games: German-style family games, Eurogames