Frank Pfenning
Students and Co-authors

Current Ph.D. Students

Jason Reed

A Hybrid Metalogical Framework,
Thesis proposal, Department of Computer Science, February 2007.
Committee: Robert Harper, Karl Crary, Rajeev Goré (Australian National University)

Noam Zeilberger

The Logical Basis of Evaluation Order,
Thesis proposal, Department of Computer Science, May 2007.
Committee: Peter Lee (co-advisor), Robert Harper, Paul-André Melliès (Université Paris 7)

Deepak Garg

Research on concurrency and authorization logics

Sean McLaughlin

Research on theorem proving in logical frameworks

William Lovas

Research on refinement types for logical frameworks

Rob Simmons

Research on concurrent logical frameworks and security

Absentia Ph.D. Students

Kevin Watkins

CLF: A Logical Framework for Concurrent Systems,
Thesis proposal, Department of Computer Science, May 2003.
Committee: Stephen Brookes, Robert Harper, Gordon Plotkin (University of Edinburgh)
On leave in 2006; in absentia since Spring 2007.

Former Ph.D. Students

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.

M.S. Students

Mark Plesko

Towards Verification of a Proof-Carrying Code Architecture in a Linear Logical Framework,

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

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

Limin Jia, Linear Logic and Imperative Programming,
Department of Computer Science, Princeton University, November 2007.

Tom Murphy VII
Thesis proposal, February 2005.

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.

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)

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

Visitors

Co-authors

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

Frank Pfenning