Frank Pfenning
Curriculum Vitæ

Academic Appointments

Visiting Positions

Education

Awards

Herbert A. Simon Award for Teaching Excellence in Computer Science,
School of Computer Science, Carnegie Mellon University, May 2002.

Jugend Forscht,
State Champion Hessen, Mathematics/Computer Science, 1975.

Fellowships

Alexander-von-Humboldt Fellowship, Technical University Darmstadt, 1996

Research Fellowship, Carnegie Mellon University, 1981-1986

Fulbright Scholarship, Carnegie Mellon University, 1980-1981

Personal Information

Born in Rüsselsheim, Hessen, Germany
German citizen, U.S. permanent resident
Married to Nancy Pfenning, Lecturer, Department of Statistics, University of Pittsburgh
Children Andreas, Marina, and Nils
One brother (Robert) and one sister (Katja Funke)

Hobbies

University Service

SCS Council, 1991-1996, 2004-present.

Departmental Review Committee (DRC), 1992-2001; chair 2004-present.

Academic Review Board, 2001-present.

Speaker's Club, 2001-present.

CMU Graduate Student Service Award Committee, 2006.

CMU Barbara Lazarus Award Committee, 2005.

CSD Advisory Board Committee, 2005.

Hiring Committee, Associate Vice Provost of Graduate Education, 2005.

Co-Chair, SCS Dean Search Committee, 2004.

Faculty Recruiting Committee, 1997, 2002, 2003.

Graduate Admissions Committee, 2002; Co-Chair 2003; 2005.

Reappointment and Promotions Committees, 1995-present.

Special Faculty Review Committee, 1995, 1999.

Lecturer Review Comittees, 1993-2000.

Undergraduate Curriculum Committee, Fall 2000.

Qualifier Review Committee (QRC), 1993-1995, 1998-1999.

POP Seminar Organization, 1991-1996.

Government Service

NASA Review Panel, 2003.

NSF Review Panels, 2002, 2003.

Advisory Boards

School of Computer Science and Engineering, Seoul National University

External review committee, June 2007.

Max-Planck-Institut für Informatik, Saarbrücken, Germany.

International Ph.D. program evaluation committee, October 2004.

INRIA, Paris, France, October 2002.

Evaluation board for Theme 2A: sémantique et programmation.

Max-Planck-Institut für Informatik, Saarbrücken, Germany.

Scientific advisory board (Fachbeirat) Member, 2001-2006; 2007-present.

Summer Schools

Software Security: Theory to Practice

Eugene, Oregon, June 17-25, 2004. Member of the scientific committee.

Foundations of Security

Eugene, Oregon, June 16-27, 2003. Member of the scientific committee.

Proofs-as-Programs

Eugene, Oregon, June 24-July 5, 2002. Member of the scientific committee.

See also Summer Courses.

Publications

See Publications.

Invited Talks

Conferences

Substructural Operational Semantics and Linear Destination-Passing Style

Second Asian Symposium on Programming Languages and Systems (APLAS'04),
Taipei, Taiwan, November 2004. Abstract (PDF) (PS) © Springer-Verlag
Slides (PDF) (PS)

Logical and Meta-Logical Frameworks

International Conference on Principles and Practice of Declarative Programming (PPDP'99),
Paris, France, September 1999. (Slides)

Reasoning about Deductions in Linear Logic

15th International Conference on Automated Deduction (CADE-15),
Lindau, Germany, July 1998.

The Practice of Logical Frameworks

Colloquium on Trees in Algebra and Programming (CAAP'96),
Linköping, Sweden, April 1996.

Universities

Distributed System Security via Logical Frameworks

Computer Science Colloquium, McGill University, November 2005.
Slides (PDF) (PS)

Modal Logic Revisited

Frank Pfenning.
Talk presented at The Scottfest in honor of Dana Scott on his 70th Birthday.
Pittsburgh, Pennsylvania, October 12, 2002.
Slides (PDF, PostScript)

Verifying Program Invariants with Refinement Types

Princeton and Yale Colloquium Talks, February 2001.
Abstract, Slides (PDF, PostScript)
Max-Planck-Institut Saarbrücken, October 2001.
Abstract, Slides (PDF, PS)

Language Techniques for Provably Safe Mobile Code

Distinguished lecture, Computing and Information Sciences,
Kansas State University, October 2000.

Workshops

Spurious Causal Dependency and Proof Irrelevance

Workshop on Logic Programming and Concurrency, Marseille, France, February 2006.

Towards a Type Theory of Contexts

Invited talk at Workshop on Mechanized Reasoning about Languages with Variable Binding (Merλin'05), Tallinn, Estonia, September 2005.
Slides (PDF) (PS)

Constructive Authorization Logics

Invited talk at the 4th Workshop on Foundations of Computer Security (FCS'05), Chicago, Illinois, July 2005.
Slides (PDF) (PS)

Linear Logical Algorithms

Worknshop on Programming Logics in Memory of Harald Ganzinger, Saarbrücken, Germany, June 2005.
Slides (PDF) (PS)

Distributed System Security via Logical Frameworks

5th Workshop on Issues in the Theory of Security (WITS'05)
Long Beach, California, January 2005.
Slides (PDF) (PS)

Tri-Directional Type Checking

Frank Pfenning, joint work with Joshua Dunfield.
Workshop on Intersection Types and Related Systems (ITRS'02), July 2002.
Slides (PDF, PostScript)

Three Applications of Strictness in the Efficient Implementation of Higher-Order Terms

Workshop on Implementations of Logic,
Réunion, France, November 2000.

Towards Modal Type Theory

Symposium on Constructivism in Non-Classical Logics and Computer Science, In Memoriam Pierangelo Miglioli,
Mantova, Italy, October 2000.
Slides.

Reasoning About Staged Computation

Workshop on Semantics, Applications and Implementation of Program Generation (SAIG'00),
Montreal, Canada, September 2000.
Abstract, Slides.

On the Logical Foundations of Staged Computation

Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'00),
Boston, Massachusetts, January 2000.
Abstract (Text, PostScript), Slides (PostScript, PDF).

A Judgmental Reconstruction of Modal Logics

Workshop on Intuitionistic Modal Logics and Applications,
Trento, Italy, July 1999.

Structural Cut Elimination

Workshop on Types for Proofs and Programs,
Turin, Italy, June 1995.

Refinement Types

Workshop on Logic, Domains and Programming Languages,
Darmstadt, Germany, May 1995.

Refinement Types for Logical Frameworks

Workshop on Types for Proofs and Programs,
Nijmegen, The Netherlands, May 1993.

Implementing the Meta-Theory of Deductive Systems

Third European Summer School on Language, Logic and Information,
Saarbrücken, Germany, August 1991.

Dependent Types in Logic Programming

Second Workshop on Extensions of Logic Programming, Stockholm, Sweden, January 1991.

Logical Frameworks and Logic Programming

Workshop on Logical Frameworks,
Sophia-Antipolis, France, May 1990.

Higher-Order Logic Programming

Meeting of the IFIP WG 2.3 on Programming Methodology,
Pittsburgh, Pennsylvania, August 1988.

Tutorials

Logical Frameworks

12th International Conference on Automated Deduction,
Nancy, France, June 1994.

Type Theory (with Peter Andrews)

11th International Conference on Automated Deduction,
Saratoga Springs, New York, June 1992.

Types in Logic Programming

9th International Conference on Logic Programming,
Jerusalem, Israel, June 1990.

Lambda Prolog (with Amy Felty, Elsa Gunter, and Dale Miller)

10th International Conference on Automated Deduction,
Kaiserslautern, Germany, July 1990.

Summer Courses

Logical and Meta-Logical Frameworks (4 lectures)

NATO Summer School on Proof and System Reliability,
Marktoberdorf, Germany, July 2001.

Reasoning about Programming Languages (5 lectures)

European Summer School on Language, Logic and Information,
Copenhagen, Denmark, August 1994.

Logical Frameworks and Logic Programming (5 hours)

Third European Summer School on Language, Logic and Information,
Saarbrücken, Germany, August 1991.

Conference Committees

See Conferences.

Professional Organizations

See Organizations.

Teaching

See Courses.

Advising

See Students and Co-authors.

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

Frank Pfenning