| |
Frank Pfenning
Students and Co-authors
- Sophia Roshal
- Research on efficient implementation of adjoint type theories
- Luiz de Sá
- Research on types for hardware design
- Siva Somayyajula
- Total Correctness Type Refinements for Communicating Processes
- Zeeshan Lakhani (S3D)
- Research on polarized functional programming
- Klaas Pruiksma
- Thesis proposal on Adjoint Logic with Applications, April 2021
- Daniel Ng
- Semi-Axiomatic Sequent Calculus Improvements
-
- Ryan Kavanagh
- Communication-Based Semantics for Recursive Session-Typed Processes
Department of Computer Science, September 2021.
- Co-advised with Steve Brookes.
-
Ankush Das
-
Resource-Aware Session Types for Digital Contracts
Computer Science Department, May 2021.
Available as Technical Report CMU-CS-21-112.
Advised by Jan Hoffmann.
-
Farzaneh Derakhshan (Dept of Philosophy)
-
Session-Typed Recursive Processes and Circular Proofs
Department of Philosophy, May 2021.
-
Henry DeYoung
- Session-Typed Ordered Logical Specifications
Department of Computer Science, December 2020.
Available as Technical Report CMU-CS-20-133.
-
Anna Gommerstadt
- Session-Typed Concurrent Contracts
Department of Computer Science, September 2019.
Available as Technical Report CMU-CS-19-119.
Co-advised with Limin Jia, ECE.
-
Kristina Sojakova
- Higher Inductive Types as Homotopy-Initial Algebras
Department of Computer Science, August 2016.
Available as Technical Report CMU-CS-16-125.
Co-advised with Steve Awodey, Department of Philosophy.
Winner of the 2016 CMU SCS Dissertation Award.
-
Dennis Griffith
- Polarized Substructural Session Types,
Department of Computer Science, University of Illinois at Urbana-Champaign, April 2016.
Co-advised with Elsa Gunter, UIUC.
- Flávio Cruz
- Linear Logic and Coordination for Parallel Programming,
Department of Computer Science, March 2016.
Available as Technical Report CMU-CS-15-148.
Co-advised with Seth Goldstein and Ricardo Rocha, University of Porto.
-
Chris Martens
-
Programming
Interactive Worlds with Linear Logic,
Department of Computer Science, September 2015.
Co-advised with Karl Crary.
Available as Technical Report CMU-CS-15-134.
- Bernardo Toninho
-
A Logical Foundation for Session-based Concurrent Computation,
Department of Computer Science, Carnegie Mellon University, and
Departamento de Informática, Universidade Nova de Lisboa,
May 2015.
Available as Technical Report CMU-CS-15-109.
Co-advised with Luís Caires.
- Rob Simmons
-
Substructural Logical Specifications,
Department of Computer Science, October 2012.
Available as Technical Report CMU-CS-12-142.
- 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.
- Jana 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.
- Zhibo Chen
- Towards a Mixed
Inductive and Coinductive Logical Framework,
December 2021.
Available as Technical Report CMU-CS-21-144.
- Chuta Sano
- On Session Typed Contracts for Imperative Languages,
December 2019.
Available as Technical Report CMU-CS-19-133.
- 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.
Available as Technical Report CMU-CS-14-110.
- Anand Subramanian
- Compiler Generation for Substructural Operational
Semantics,
December 2012.
Available as Technical Report CMU-CS-12-150.
- Rob Arnold
- C0, an Imperative Programming Language for Novice
Computer Scientists,
December 2010.
Available as Technical Report CMU-CS-10-145.
- 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.
- Aditi Gupta
- Ergometric Multilinear Futures, May 2022.
Winner of the Allen Newell Award for Excellence in Undergraduate Research.
-
Benedikt Stock
- General Pattern Matching for Session-Typed Concurrent Programs
Jacobs University, Mathematics, May 2020.
Co-supervised with Sören Petrat.
Dean's Prize for Outstanding Bachelor Thesis.
- William Chargin
- A General System of Adjoint Logic
December 2017.
-
Coşku Acay
- Refinements for Session Typed Concurrency
- May 2016
-
Max Willsey
-
Design and Implementation of Concurrent C0
- May 2016
- Designated as Exemplary Thesis by the senior thesis award committee
- 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.
- Travis Hance, proposal Verifying Concurrent Systems Code, August 2023
- David Kahn, proposal Leveraging Linearity to Improve Automatic
Amortized Resource Analysis, April 2023
- Katherine Kosaian, Formally Verifying Algorithms for Real Quantifier
Elimination, June 2023
- Yong Kiam Tan, Deductive Verification for Ordinary Differential Equations:
Safety, Liveness, and Stability, Spring 2022
- Anlun Xu (MSCS), Extending
Abstract Effects with Bounds and Algebraic Handlers, December 2020
- Rose Bohrer, Practical End-to-End Verification of Cyber-Physical Systems, May 2021
- Abulhair Saparov (MLD), Towards General Natural Language Understanding with Probabilistic
World Building, January 2022
- Micheal Coblenz, User-Centered
Design of Principled Programming Languages, August 2020
- Matthew Maurer (ECE), Holmes, October 2018
- Kuen-Bang Hou (Favonia), Higher-Dimensional
Types in the Mechanization of Homotopy Theory, February 2017
- Ligia Nistor, Object Propositions, December 2017
- Sarah Loos, Differential Refinement Logic,
February 2016
- Qinsi Wang, Formal Methods
for Biological Systems: Languages, Algorithms, and Applications, September 2016
- Filipe Militão (ISR), Rely-Guarantee
Protocols for Safe Interference over Shared Memory, December 2015
- Leigh Ann Sudol-DeLeyser, AbstractTutor:
Increasing Algorithm Implemention Expertise for Novices Through Algorithmic Feedback, December 2014
-
Pongsin Poosankam, Scaling Concolic Execution of Binary
Programs for Security Applications, 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,
February 2011.
-
Jeffery A. Vaughan, Aura: Programming with Authorization and Audit,
University of Pennsylvania, 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.
- Himanshu Jain, Verification using
Satisfiability Checking, Predicate Abstraction, and Craig Interpolation
September 2008
-
Tom Murphy VII, Modal Types for Mobile Code,
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 | École Polytechnique | 1800 |
| Joseph Lagrange | (no degree) | |
| Leonhard Euler | Universität Basel | 1726 |
| Johann Bernoulli | Universität Basel | 1694 |
| Jacob Bernoulli | Universität Basel | 1684 |
| Nicholas Malebranche | | 1672 |
| Gottfried Leibniz | Universität Leipzig | 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 |
| Stephanie Balzer |
ETH Zürich |
Postdoctoral Fellow |
August 2014-May 2016 |
| 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 |
| Adrian Francalanza |
University of Malta |
Visiting Faculty |
April 2019-May 2019 |
| Marco Carbone |
ITU Copenhagen |
Visiting Faculty |
October 2018-November 2018 |
| 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 |
See my DBLP or
Google Scholar profiles
[ Home
| Contact
| Research
| Publications
| CV
| Students
]
[ Projects
| Courses
| Conferences
| Organizations
| Journals
]
Frank Pfenning
|