| |
Frank Pfenning
Students and Co-authors
- Rob Simmons
- Research on concurrent logical frameworks and logic programming
- Michael Ashley-Rollman
- Research on ensemble programming; co-advised with Seth Goldstein
- Henry DeYoung
- Research on security and privacy from a logical perspective
- Bernardo Toninho
- Research on linear logic and session types; co-advised with Luís Caires
- Jamie Morgenstern
- Research on logic and game theory; co-advised with Avrim Blum
- Kristina Sojakova
- Research on logical framework and categorical type theory;
co-advised with Steve Awodey
- Flávio Cruz
- Research on programming languages for parallel computation;
co-advised with Seth Goldstein and Ricardo Rocha
- Anton Bachin
- Research on compiling authorization policies
- Anand Subramnian
- Research on substructural operational semantics
- 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.
- 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.
- Rob Arnold
- C0, an Imperative Programming Language for Novice
Computer Scientists,
December 2010.
- 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.
- 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.
-
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.
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 |
| 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 |
| 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 |
[ Home
| Contact
| Research
| Publications
| CV
| Students
]
[ Projects
| Courses
| Conferences
| Organizations
| Journals
]
[ Logical Frameworks
| Pittsburgh Squash Racquets Assocation
]
Frank Pfenning
|