Frank Pfenning
Students and Co-authors

Contents Current Ph.D. Students | Current M.S. Students | Former Ph.D. Students | Current M.S. Students | Honors Students
Thesis Committee Member
Academic Ancestors
Postdoctoral Fellows | Visitors | Co-authors

Current Ph.D. Students

Anna Gommerstadt
Research on session-based concurrency
Flávio Cruz
Research on programming languages for parallel computation; co-advised with Seth Goldstein and Ricardo Rocha
Kristina Sojakova
Research on homotopy type theory and inductive types; co-advised with Steve Awodey
Bernardo Toninho
Research on linear logic and session types; co-advised with Luís Caires
Henry DeYoung
Research on security and privacy from a logical perspective
Chris Martens
Research on logical interactive programming for narrative worlds; co-advised with Karl Crary

Current M.S. Students

Absentia Ph.D. Students

Michael Ashley-Rollman
Research on ensemble programming; co-advised with Seth Goldstein; in absentia
Sean McLaughlin
Practical Automated Reasoning with the Polarized Inverse Method,
Thesis proposal, Department of Computer Science, May 2009.
Committee: Jeremy Avigad, Robert Harper, Dale Miller (INRIA), André Platzer. In absentia since August 2010.

Former Ph.D. Students

Rob Simmons
Substructural Logical Specifications,
Department of Computer Science, October 2012.
William Lovas
Refinement Types for Logical Frameworks,
Department of Computer Science, August 2010.
Available as Technical Report CMU-CS-10-138.
Deepak Garg
Proof Theory for Authorization Logic and Its Application to a Practical File System,
Department of Computer Science, December 2009.
Available as Technical Report CMU-CS-09-168.
Jason Reed
A Hybrid Logical Framework,
Department of Computer Science, August 2009.
Available as Technical Report CMU-CS-09-155.
Noam Zeilberger
The Logical Basis of Evaluation Order and Pattern-Matching,
Department of Computer Science, May 2009.
Available as Technical Report CMU-CS-09-122.
Co-advised with Peter Lee.
Joshua Dunfield
A Unified System of Type Refinements,
Department of Computer Science, August 2007.
Available as Technical Report CMU-CS-07-129.
Kaustuv Chaudhuri
The Focused Inverse Method for Linear Logic,
Department of Computer Science, December 2006.
Available as Technical Report CMU-CS-06-162.
Sungwoo Park
A Programming Language for Probabilistic Computation,
Department of Computer Science, August 2005.
Available as Technical Report CMU-CS-05-137.
Co-advised with Sebastian Thrun.
Rowan Davies
Practical Refinement-Type Checking,
Department of Computer Science, May 2005.
Available as Technical Report CMU-CS-05-110.
Aleks Nanevski
Functional Programming with Names and Necessity,
Department of Computer Science, August 2004.
Available as Technical Report CMU-CS-04-151.
Brigitte Pientka
Tabled Higher-Order Logic Programming,
Department of Computer Science, December 2003.
Available as Technical Report CMU-CS-03-185.
Jeff Polakow
Ordered Linear Logic and Applications,
Department of Computer Science, August 2001.
Available as Technical Report CMU-CS-01-152.
Gerald Penn
The Algebraic Structure of Attributed Type Signatures,
Language Technologies Institute, Carnegie Mellon University,
August 2000. Co-advised with Bob Carpenter.
Available as Technical Report CMU-LTI-00-164.
Nominated by CMU SCS for the ACM Dissertation Award.
Winner of the 2001 E. W. Beth Dissertation Award.
Alberto Momigliano
Elimination of Negation in a Logical Framework,
Department of Philosophy, Carnegie Mellon University, July 2000.
Available as Technical Report CMU-CS-00-175.
Carsten Schürmann
Automating the Meta-Theory of Deductive Systems,
Department of Computer Science, Carnegie Mellon University, August 2000.
Available as Technical Report CMU-CS-00-146.
Roberto Virga
Higher-Order Rewriting with Dependent Types,
Department of Mathematical Sciences, Carnegie Mellon University,
September 1999.
Hongwei Xi
Dependent Types in Practical Programming,
Department of Mathematical Sciences, Carnegie Mellon University,
November 1998.
Iliano Cervesato
A Linear Logical Framework,
Department of Computer Science, University of Turin,
February 1996.
Tim Freeman
Refinement Types for ML,
Department of Computer Science, Carnegie Mellon University,
March 1994.
Penny Anderson
Program Development by Proof Transformation,
Department of Computer Science, Carnegie Mellon University,
October 1993.
Nevin Heintze
Set Based Program Analysis,
Department of Computer Science, Carnegie Mellon University,
January 1993. Co-advised with Peter Lee.
Nominated by CMU for the ACM Dissertation Award.
Spiro Michaylov
Design and Implementation of Practical Constraint Logic Programming Systems,
Department of Computer Science, Carnegie Mellon University,
May 1992. Co-advised with Peter Lee.
Scott Dietzen
A Language for Higher-Order Explanation-Based Learning,
Department of Computer Science, Carnegie Mellon University,
May 1991.
Conal Elliott
Extensions and Applications of Higher-Order Unification,
Department of Computer Science, Carnegie Mellon University,
June 1990.

Former M.S. Students

Jason Koenig
Program Analysis for Introductory Education: Leveraging Programmer Specifications
August 2014.
Matthew Mirman
Logic Programming and Type Inference with the Calculus of Constructions
May 2014.
Anand Subramnian
Compiler Generation for Substructural Operational Semantics
December 2012.
Rob Arnold
C0, an Imperative Programming Language for Novice Computer Scientists,
December 2010.
Thilo Trapp
A Proof-Theoretic Analysis of Sorts in Intuitionistic Logic ,
University of Dresden, June 2001.
Mark Plesko
Towards Verification of a Proof-Carrying Code Architecture in a Linear Logical Framework,
M.S. Thesis, Department of Mathematics, Carnegie Mellon University,
August 2000.
Christian Skalka
Some Decision Problems for ML Refinement Types,
M.S. Thesis, Department of Philosophy, Carnegie Mellon University,
August 1997.
Carsten Schürmann
A Computational Meta-Logic for the Horn Fragment of LF,
M.S. Thesis, Department of Philosophy, Carnegie Mellon University,
December 1995.
Raymond Pelletier
The Goal Driven Production System Tertl and its Abstract Machine,
M.S. Thesis, Department of Philosophy, Carnegie Mellon University,
December 1995.
Alberto Momigliano
Negation in Logic Programming,
M.S. Thesis, Department of Philosophy, Carnegie Mellon University,
May 1994.

Honors Students

Elizabeth Davis
A Proof-Based Approach to Formalizing Protocols in Linear Epistemic Logic
May 2014
Matthew Mirman
Modes for Non-Strict Functional Logic Languages
May 2012
Jakob Uecker
A Library for Bottom-up Logic Programming in a Functional Language
Jacobs University, Bremen, Germany, May 2010.
Chris Martens
A Hybrid Formulation of the Ordered Logical Framework
May 2008.
Henry DeYoung
A Logic for Reasoning About Time-Dependent Access Control Policies
Allen Newell Award for Excellent in Undergraduate Research
May 2008.
Greg Price
Toward Efficient Proof Search for Linear Logic
May 2006
Michael Coblenz
Using Objects of Measurements to Detect Spreadsheet Errors
May 2005. Co-advised with Brad Myers.
Evan Chang
Iktara in ConCert: Realizing a Certified Grid Computing Framework from a Programmer's Perspective
May 2002. Co-advised with Robert Harper.
Available as Technical Report CMU-CS-02-150, June 2002.
Margaret DeLap
Implementing a Framework for Certified Grid Computing
May 2002. Co-advised with Robert Harper.
Jason Reed
Proof Irrelevance and Strict Definitions in a Logical Framework
May 2002.
Geoff Washburn
Modal Types for Run-Time Code Generation
May 2001. Co-advised with Peter Lee.
John Corwin
Linear Logic Theorem Proving using Artificial Intelligence Planners
May 2001. Department of Philosophy.
Mark Plesko
Towards Verification of a Proof-Carrying Code Architecture in a Linear Logical Framework,
Allen Newell Award for Excellence in Undergraduate Research
May 2000.
Doug Fearing
Proof Search in Logical Frameworks
May 1999.
Barbara Moura
Compiling Prolog to Standard ML
May 1992. Co-advised with Peter Lee.
Luke Hornof
Compiling Prolog to Standard ML: Some Optimizations
May 1992. Available as Technical Report CMU-CS-92-166, September 1992.
Co-advised with Peter Lee.

Thesis Committee Member

Arbob Ahamad
Ligia Nistor
Carsten Varming
Leigh Ann Sudol
Pongsin Poosankam, Scaling Concolic Execution of Binary Programs for Security Applications,
Department of Computer Science, Carnegie Mellon University, August 2013.
Anders Schack-Nielsen, Implementing Substructural Logical Frameworks,
Department of Computer Science, ITU Copenhagen, April 2011.
Daniel Licata, Dependently Typed Programming with Domain-Specific Logics,
Department of Computer Science, Carnegie Mellon University, February 2011.
Jeffery A. Vaughan, Aura: Programming with Authorization and Audit,
University of Pennsylvania, Proposal March 2009.
David Baelde, A Linear Approach to the Proof-theory of Least and Greatest Fixed Points,
École Polytechnique, December 2008.
Florian Rabe, Representing Logics and Logic Translations,
Department of Computer Science, Jacobs University, Bremen, June 2008.
Tom Murphy VII, Modal Types for Mobile Code,
Department of Computer Science, Carnegie Mellon University, May 2008.
Limin Jia, Linear Logic and Imperative Programming,
Department of Computer Science, Princeton University, November 2007.
Rajesh Kumar, An Ontology-based Knowledge Management Framework for Heterogeneous Verification,
Department of Electrical and Computer Engineering, Carnegie Mellon University, April 2007.
Daniel Méry, Preuves et Sémantiques dans des Logiques de Ressources,
University Henri Poincaré, Nancy, November 2004.
Chad Brown, Set Comprehension in Church's Type Theory,
Department of Mathematical Sciences, CMU, July 2004.
Alwen Tiu, A Logical Framework for Reasoning about Logical Specifications,
Pennsylvania State University, May 2004.
Andrew Bernard, Engineering Formal Security Policies for Proof-Carrying Code,
Department of Computer Science, CMU, April 2004.
Serge Autexier, Hierarchical Contextual Reasoning,
Universität des Saarlandes, 2003.
Kathryn Van Stone, A Denotational Approach to Measuring Complexity in Functional Programs,
Department of Computer Science, CMU, May 2003.
Quang Huy Nguyen, Calcul de réécriture et automatisation du raisonnement dans les assistants de preuve,
University Henri Poincaré, Nancy, October 2002.
Marco Bozzano, A Logic-Based Approach to Model Checking of Parameterized and Infinite State Systems,
University of Genoa, June 2002.
Davide Marchignoli, Natural Deduction Systems for Temporal Logics,
University of Pisa, February 2002.
Armin Fiedler, User-Adaptive Proof Explanation,
Universität des Saarlandes, Germany, October 2001.
Robert O'Callahan, Department of Computer Science, CMU, November 2000.
Andrej Bauer, Department of Computer Science, CMU, September 2000.
Pawel Rychlikowski, University of Wroclaw, May 2000.
Tomasz Truderung, University of Wroclaw, May 2000.
Matthew Bishop, Department of Mathematics, CMU, 1999.
John Byrnes, Department of Philosophy, CMU, 1999.
Christoph Benzmüller, Universität des Saarlandes, 1999.
George Necula, Department of Computer Science, CMU, 1998.
Pierre Leleu, Ecole Nationale des Ponts et Chaussees, 1998.
Denis Dancanet, Department of Computer Science, CMU, 1998.
Raymond McDowell, University of Pennsylvania, 1997.
Myra VanInwegen, University of Pennsylvania, 1996.
Chuck Liang, University of Pennsylvania, 1995.
Michael Kohlhase, Universität des Saarlandes, 1994.
Todd Wilson, Department of Computer Science, CMU, 1994.
Sunil Issar, Department of Mathematics, CMU, 1991.
Wayne Snyder, University of Pennsylvania, 1988.

Academic Ancestors

Information according to The Mathematics Genealogy Project, North Dakota State University.

  University Year of Ph.D.
Frank Pfenning Carnegie Mellon University 1987
Peter Andrews Princeton University 1964
Alonzo Church Princeton University 1927
Oswald Veblen The University of Chicago 1903
E.H. Moore Yale University 1885
H.A. Newton Yale University 1850
Michel Chasles École Polytechnique 1814
Simeon Poisson
Joseph Lagrange
Leonhard Euler Universität Basel 1726
Johann Bernoulli 1694
Jacob Bernoulli
Gottfried Leibniz Universität Altdorf 1666

My Erdös number is 3: Paul Erdös - Andreas Blass - Andre Scedrov - Frank Pfenning

Some notable academic uncles (other students of Alonzo Church, my advisor's advisor)

  University Year of Ph.D.
Raymond Smullyan Princeton University 1959
Dana Scott Princeton University 1958
Michael Rabin Princeton University 1956
Hartley Rogers, Jr. Princeton University 1952
Martin Davis Princeton University 1950
Leon Henkin Princeton University 1947
Alan Turing Princeton University 1938
Stephen Kleene Princeton University 1934
John Rosser Princeton University 1934

Some notable academic brothers (other students of Peter Andrews, my advisor)

  University Year of Ph.D.
Chad Brown Carnegie Mellon University 2004
Matthew Bishop Carnegie Mellon University 1999
Sunil Issar Carnegie Mellon University 1991
Dale Miller Carnegie Mellon University 1983

Postdoctoral Fellows

Beniamino Accattoli Bologna University Postdoctoral Fellow September 2012-August 2013
Yuxin Deng Shanghai Jiaotong University Postdoctoral Fellow March 2011-February 2012
Ron Garcia University of British Columbia Computing Innovation Fellow August 2009-August 2011
David Walker Princeton University Postdoctoral Fellow September 2000-October 2001

Visitors

Ian Zerny Aarhus University Visiting Scholar October 2011-May 2012
Carsten Schürmann ITU Copenhagen Visiting Professor February-July 2011
Jamie Morgenstern University of Chicago REU Scholar June-August 2009
Anders Schack-Nielsen ITU Copenhagen Visiting Scholar January-July 2009
David Baelde École Polytechnique Postdoctoral Visitor February-March 2009
Romain Brenguier ENS Cachan Visiting Scholar April-August 2008
Todd Wilson California State University, Fresno Visiting Professor January-May 2007
Florian Rabe International University Bremen Visiting Scholar January-December 2006
Bruno Bernardo Ecole Polytechnique Visiting Scholar May-Aug 2005
Yukiyoshi Kameyama University of Tsukuba Visiting Scientist May-July 2005
Pablo López University of Malaga Visiting Scholar September-November 2004
Erika Rice University of Washington REU Scholar June-August 2003
Andreas Abel Chalmers University Visiting Scholar May 2000-June 2001
Marco Bozzano ITC-IRST, Trento Visiting Scholar September 2000-May 2001
Wolfgang Gehrke RISC-Linz Visiting Scholar September-December 1994
Olivier Danvy BRICS, University of Aarhus Visiting Scientist January-August 1993
Gilles Dowek École Polytechnique and INRIA-Futurs Visiting Scientist January-June 1992
Masami Hagiya University of Tokyo Visiting Scientist April-June 1989

Co-authors

Andreas Abel
Penny Anderson
Peter Andrews
Lujo Bauer
Mary Berna
Matthew Bishop
Kevin Bowers
Chad Brown
Luís Caires
Iliano Cervesato
Bor-Yuh Evan Chang
Kaustuv Chaudhuri
Christopher Colby
Karl Crary
Eve Cohen
Olivier Danvy
Rowan Davies
Joëlle Despeyroux
Margaret DeLap
Henry DeYoung
Scott Dietzen
Gilles Dowek
Joshua Dunfield
Belmina Dzafic
Conal Elliott
Amy Felty
Tim Freeman
Deepak Garg
Geoff Gordon
Elsa Gunter
John Hannan
Thérèse Hardin
Robert Harper
Joshua Hodas
Sunil Issar
Claude Kirchner
Carl Klapper
Aleksey Kliger
Michael Kohlhase
Peter Lee
Brad Lisien
Mark Leone
Jason Liszka
William Lovas
Ruy Ley-Wild
Jason Liszka
Pablo López
Sean McLaughlin
Spiro Michaylov
Dale Miller
Alberto Momigliano
Tom Murphy VII
Gopalan Nadathur
Aleksandar Nanevski
Paliath Narendran
Daniel Nesmith
Robert Nord
Sungwoo Park
Christine Paulin
Gerald Penn
Leaf Petersen
Brigitte Pientka
Mark Plesko
Jeff Polakow
Greg Price
Jorge A. Pérez
Jason Reed
Mike Reiter
John Reynolds
Ekkehard Rohwedder
Eugene Rollins
Uluç Saranli
Andre Scedrov
William Scherlis
Carsten Schürmann
Dana Scott
Brennan Sellner
Denis Serenyi
Robert J. Simmons
Richard Statman
Sebastian Thrun
David Walker
Kevin Watkins
Philip Wickline
Brian Witten
Hao-Chi Wong
Hongwei Xi

[ Home | Contact | Research | Publications | CV | Students ]
[ Projects | Courses | Conferences | Organizations | Journals ]
[ Logical Frameworks | Pittsburgh Squash Racquets Assocation ]

Frank Pfenning