Colloquium - Futures Revisited

Colloquium - Futures Revisited promotional image


Frank Pfenning


Futures have been around since Multilisp in 1985 and have been a popular abstraction for parallelism and concurrency in a variety of programming languages since then.  In brief, they allow us to spawn a new thread of computation and synchronize on the computed value.  We present a recently discovered type-theoretic foundation for futures, which turn out to arise from a formal system half-way between Hilbert-style axioms and a Gentzen-style sequent calculus with several interesting features.  We then exploit this foundation to define linear futures that avoid the need for complex concurrent  garbage collection.  We also briefly sketch ongoing work attempting to use ergometric types to inform scheduling decisions for linear futures.

[joint work with Henry DeYoung, Aditi Gupta, and Klaas Pruiksma]


 Frank Pfenning studied Mathematics and Computer Science at the Technical University Darmstadt and then left for Carnegie Mellon University on a Fulbright scholarship where he obtained his Ph.D. in Mathematics in 1987 under the supervision of Professor Peter Andrews.

He subsequently joined the Computer Science Department at Carnegie Mellon University as research faculty where he became Professor in 2002 and served as Director of Graduate Programs from 2004 to 2008 and Associate Dean for Graduate Education from 2009 to 2010. He served as Head of the Computer Science Department and Joseph F. Traub Professor of Computer Science from 2013 to 2018.

He has spent time as visiting scientist at the Max-Planck-Institute for Computer Science in Saarbrücken, as Alexander-von-Humboldt fellow at the Technical University Darmstadt, and as visiting professor at École Polytechnique and INRIA-Futurs. He has advised 29 completed Ph.D. theses and won the Herbert A. Simon Award for Teaching Excellence in the School of Computer Science in 2002.

He served as trustee, vice president, and president of CADE, Inc., the governing body of the International Conference on Automated Deduction, and on advisory boards for INRIA, the Max-Planck-Institute for Computer Science, and Seoul National University. He has chaired several conferences and program committees, including CADE and LICS, and has been a member of the editorial boards for Theoretical Computer Science, Journal of Automated Reasoning, and the Journal of Symbolic Computation. He was named Fellow of the ACM in 2015.

His research interests include programming languages, logic and type theory, logical frameworks, automated deduction, and computer security. In his spare time he enjoys playing squash, running, hiking, cooking, and reading.

Interested parties may contact us for Zoom url.

Friday, September 17, 2021 4:00pm to 5:00pm
Virtual Event
Online venue
University of Iowa, Iowa City, IA 52242
View on Event Calendar
Individuals with disabilities are encouraged to attend all University of Iowa–sponsored events. If you are a person with a disability who requires a reasonable accommodation in order to participate in this program, please contact Matthieu Biger in advance at 3194670743 or