| |
Frank Pfenning
Publications
The most recent drafts and publications
are listed on my home page.
Last Updated: Sat Feb 17 2007
This page lists publications, reports, and drafts in
reverse chronological order by year and by last name of first
author within each year. Submissions are listed at the time they are
completed and moved when they appear. Also see the
bibliography sorted by type of publication.
-
Ruy Ley-Wild and Frank Pfenning.
Avoiding causal dependencies via proof irrelevance in a concurrent
logical framework.
Technical Report CMU-CS-07-107, Carnegie Mellon University, February
2007.
In preparation.
[PDF]
-
Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka.
Contextual modal type theory.
Transactions on Computational Logic, 2007.
To appear.
[PDF]
-
Kaustuv Chaudhuri, Frank Pfenning, and Greg Price.
A logical characterization of forward and backward chaining in the
inverse method.
Submission to special issue in Journal of Automated Reasoning with
selected papers from IJCAR 2006, February 2007.
[PDF]
-
Uluç Saranli and Frank Pfenning.
Using constrained intuitionistic linear logic for hybrid robotic
planning problems.
In Proceedings of the International Conference on Robotics and
Automation (ICRA'07), Rome Italy, April 2007. IEEE Computer Society Press.
To appear.
[PDF]
-
Kevin D. Bowers, Lujo Bauer, Deepak Garg, Frank Pfenning, and Michael K.
Reiter.
Consumable credentials in logic-based access-control systems.
In Proceedings of the 14th Annual Network and Distributed System
Security Symposium (NDSS'07), San Diego, California, February 2007. Internet
Society.
To appear. Preliminary version available as Technical Report
CMU-CYLAB-06-002, Carnegie Mellon University, February 2006.
[PDF]
-
Deepak Garg, Lujo Bauer, Kevin Bowers, Frank Pfenning, and Michael Reiter.
A linear logic of affirmation and knowledge.
In D. Gollman, J. Meier, and A. Sabelfeld, editors, Proceedings
of the 11th European Symposium on Research in Computer Security
(ESORICS'06), pages 297-312, Hamburg, Germany, September 2006. Springer
LNCS 4189.
[PDF]
-
Kaustuv Chaudhuri, Frank Pfenning, and Greg Price.
A logical characterization of forward and backward chaining in the
inverse method.
In U. Furbach and N. Shankar, editors, Proceedings of the 3rd
International Joint Conference on Automated Reasoning (IJCAR'06), pages
97-111, Seattle, Washington, August 2006. Springer LNCS 4130.
[PDF]
-
Frank Pfenning, editor.
Proceedings of the 17th International Conference on Rewriting
Techniques and Applications, Seattle, Washington, August 2006. Springer
Verlag LNCS 4098.
-
Deepak Garg and Frank Pfenning.
Non-interference in constructive authorization logic.
In J. Guttman, editor, Proceedings of the 19th Computer Security
Foundations Workshop (CSFW'06), pages 283-293, Venice, Italy, July 2006.
IEEE Computer Society Press.
[PDF]
-
Lujo Bauer, Kevin D. Bowers, Frank Pfenning, and Michael K. Reiter.
Consumable credentials in logic-based access control.
Technical Report CMU-CYLAB-06-002, Carnegie Mellon University,
February 2006.
Available electronically
-
Jason Reed and Frank Pfenning.
Intuitionistic letcc via labelled deduction.
Submitted, February 2006.
[PDF]
[PostScript]
-
Aleksandar Nanevski and Frank Pfenning.
Staged computation with names and necessity.
Journal of Functional Programming, 15(6):837-891, November
2005.
[PDF]
[PostScript]
-
Kaustuv Chaudhuri and Frank Pfenning.
Focusing the inverse method for linear logic.
In L.Ong, editor, Proceedings of the 14th Annual Conference on
Computer Science Logic (CSL'05), pages 200-215, Oxford, England, August
2005. Springer Verlag LNCS 3634.
[PDF]
[PostScript]
-
Deepak Garg and Frank Pfenning.
Type-directed concurrency.
In M.Abadi and L.de Alfaro, editors, Proceedings of the 16th
International Conference on Concurrency Theory (CONCUR'05), pages 6-20, San
Francisco, California, August 2005. Springer Verlag LNCS 3653.
[PDF]
[PostScript]
-
Kaustuv Chaudhuri and Frank Pfenning.
A focusing inverse method prover for first-order linear logic.
In R.Nieuwenhuis, editor, Proceedings of the 20th International
Conference on Automated Deduction (CADE-20), pages 69-83, Tallinn, Estonia,
July 2005. Springer Verlag LNCS 3632.
[PDF]
[PostScript]
-
Pablo López, Frank Pfenning, Jeff Polakow, and Kevin Watkins.
Monadic concurrent linear logic programming.
In A.Felty, editor, Proceedings of the 7th International
Symposium on Principles and Practice of Declarative Programming (PPDP'05),
pages 35-46, Lisbon, Portugal, July 2005. ACM Press.
[PDF]
[PostScript]
-
Karl Crary, Aleksey Kliger, and Frank Pfenning.
A monadic analysis of information flow security with mutable state.
Journal of Functional Programming, 15(2):249-291, March 2005.
Preliminary version available as Technical Report CMU-CS-03-164.
[PDF]
[PostScript]
-
Sungwoo Park, Frank Pfenning, and Sebastian Thrun.
A probabilistic language based upon sampling function.
In M.Abadi, editor, Conference Record of the 32nd Symposium on
Principles of Programming Languages (POPL'05), pages 171-182, Long Beach,
California, January 2005. ACM Press.
[PDF]
[PostScript]
-
Robert Harper and Frank Pfenning.
On equivalence and canonical forms in the LF type theory.
Transactions on Computational Logic, 6:61-101, January 2005.
[PDF]
[PostScript]
-
Frank Pfenning.
Substructural operational semantics and linear destination-passing
style.
In Wei-Ngan Chin, editor, Proceedings of the 2nd Asian Symposium
on Programming Languages and Systems (APLAS'04), page 196, Taipei, Taiwan,
November 2004. Springer-Verlag LNCS 3302.
Abstract of invited talk.
[PDF]
[PostScript]
-
Frank Pfenning.
Review of ``Benjamin C. Pierce: Types and programming languages,
The MIT Proess, Cambridge, Massachusetts, 2002''.
Bulletin of Symbolic Logic, 10:213-214, 2004.
[PDF]
[PostScript]
-
Penny Anderson and Frank Pfenning.
Verifying uniqueness in a logical framework.
In K.Slind, A.Bunker, and G.Gopalakrishnan, editors, Proceedings
of the 17th International Conference on Theorem Proving in Higher Order
Logics (TPHOLs'04), pages 18-33, Park City, Utah, September 2004. Springer
LNCS 3223.
[PDF]
[PostScript]
-
Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker.
Specifying properties of concurrent computations in CLF.
In C.Schürmann, editor, Proceedings of the 4th International
Workshop on Logical Frameworks and Meta-Languages (LFM'04), Cork, Ireland,
July 2004.
[PDF]
[PostScript]
-
Tom Murphy VII, Karl Crary, Robert Harper, and Frank Pfenning.
A symmetric modal lambda calculus for distributed computing.
In H. Ganzinger, editor, Proceedings of the 19th Annual
Symposium on Logic in Computer Science (LICS'04), pages 286-295, Turku,
Finland, July 2004. IEEE Computer Society Press.
Extended version available as Technical Report CMU-CS-04-105.
[PDF]
[PostScript]
-
Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker.
A concurrent logical framework: The propositional fragment.
In S. Berardi, M. Coppo, and F. Damiani, editors, Types for
Proofs and Programs, pages 355-377. Springer-Verlag LNCS 3085, 2004.
Revised selected papers from the Third International Workshop on
Types for Proofs and Programs, Torino, Italy, April 2003.
[PDF]
[PS]
-
Peter B. Andrews, Matthew Bishop, Chad E. Brown, Sunil Issar, Frank Pfenning,
and Hongwei Xi.
ETPS: A system to help students write formal proofs.
Journal of Automated Reasoning, 32(1):75-92, 2004. Available from Kluwer Online.
Draft from December 2002 available
[PDF]
[PS]
-
Joshua Dunfield and Frank Pfenning.
Tridirectional typechecking.
In X.Leroy, editor, Conference Record of the 31st Annual
Symposium on Principles of Programming Languages (POPL'04), pages 281-292,
Venice, Italy, January 2004. ACM Press.
Extended version available as Technical Report CMU-CS-04-117, March 2004.
[PDF]
[PS]
-
Bor-Yuh Evan Chang, Kaustuv Chaudhuri, and Frank Pfenning.
A judgmental analysis of linear logic.
Submitted. Extended version available as Technical Report
CMU-CS-03-131R, December 2003.
[PDF]
[PS]
-
Alberto Momigliano and Frank Pfenning.
Higher-order pattern complement and the strict lambda-calculus.
Transactions on Computational Logic, 4(4), October 2003.
[PDF]
[PS]
-
Frank Pfenning and Yannis Smaragdakis, editors.
Proceedings of the Second International Conference on Generative
Programming and Component Engineering.
Springer-Verlag LNCS 2830, Erfurt, Germany, September 2003.
Available in the ACM Digital Library
and LNCS Online.
-
Carsten Schürmann and Frank Pfenning.
A coverage checking algorithm for LF.
In D. Basin and B. Wolff, editors, Proceedings of the 16th
International Conference on Theorem Proving in Higher Order Logics (TPHOLs
2003), pages 120-135, Rome, Italy, September 2003. Springer-Verlag LNCS
2758.
[PDF]
[PS]
-
M. Berna, B. Lisien, B. Sellner, G. Gordon, F. Pfenning, , and S. Thrun.
A learning algorithm for localizing people based on wireless signal
strength that uses labeled and unlabeled data.
In Proceedings of the 18th International Joint Conference on
Artificial Intelligence (IJCAI'03), Acapulco, Mexico, August 2003.
Poster.
[PS]
-
Aleksandar Nanevski, Brigitte Pientka, and Frank Pfenning.
A modal foundation for meta-variables.
In Proceedings of the Second Workshop on Mechanized Reasoning
about Languages with Variable Binding (MERLIN'03), Uppsala, Sweden, August
2003. ACM SIGPLAN.
[PDF]
[PS]
-
Brigitte Pientka and Frank Pfenning.
Optimizing higher-order pattern unification.
In F. Baader, editor, Proceedings of the 19th Conference on
Automated Deduction (CADE-19), pages 473-487, Miami Beach, Florida, July
2003. Springer-Verlag LNAI 2741.
[PDF]
[PS]
-
Iliano Cervesato and Frank Pfenning.
A linear spine calculus.
Journal of Logic and Computation, 13(5):639-688, 2003.
[PDF]
[PS]
-
Karl Crary, Aleksey Kliger, and Frank Pfenning.
A monadic analysis of information flow security with mutable state.
Technical Report CMU-CS-03-164, Carnegie Mellon University, September
2003.
[PDF]
[PS]
-
Christopher Colby, Karl Crary, Robert Harper, Peter Lee, and Frank Pfenning.
Automated techniques for provable safe mobile code.
Theoretical Computer Science, 290:1175-1199, 2003.
Special issue on Dependable Computing. Preliminary version
appeared in the proceedings of the DARPA Information Survivability Conference
and Exposition (DISCEX 2000), vol 1, pp. 406-419, Hilton Head Island, South
Carolina, January 2000.
[PDF]
[PS]
-
Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker.
A concurrent logical framework I: Judgments and properties.
Technical Report CMU-CS-02-101, Department of Computer Science,
Carnegie Mellon University, 2002.
Revised May 2003.
[PDF]
[PS]
-
Iliano Cervesato, Frank Pfenning, David Walker, and Kevin Watkins.
A concurrent logical framework II: Examples and applications.
Technical Report CMU-CS-02-102, Department of Computer Science,
Carnegie Mellon University, 2002.
Revised May 2003.
[PDF]
[PS]
-
Joshua Dunfield and Frank Pfenning.
Type assignment for intersections and unions in call-by-value
languages.
In A.D. Gordon, editor, Proceedings of the 6th International
Conference on Foundations of Software Science and Computation Structures
(FOSSACS'03), pages 250-266, Warsaw, Poland, April 2003. Springer-Verlag
LNCS 2620.
[PDF]
[PS]
-
Robert Harper and Frank Pfenning.
On equivalence and canonical forms in the LF type theory.
Transactions on Computational Logic, 2003.
To appear. Preliminary version available as Technical Report
CMU-CS-00-148.
[PDF]
[PS]
-
Aleksandar Nanevski and Frank Pfenning.
Meta-programming with names and necessity.
Submitted, February 2003.
[PDF]
[PS]
-
Kaustuv Chaudhuri and Frank Pfenning.
Resource management for the inverse method in linear logic.
Draft manuscript, January 2003.
[PDF]
[PS]
-
Leaf Petersen, Robert Harper, Karl Crary, and Frank Pfenning.
A type theory for memory allocation and data layout.
In G. Morrisett, editor, Conference Record of the 30th Annual
Symposium on Principles of Programming Languages (POPL'03), pages 172-184,
New Orleans, Louisiana, January 2003. ACM Press.
Extended version available as Technical Report CMU-CS-02-171,
December 2002.
[PDF]
[PS]
-
Frank Pfenning.
Computation and Deduction.
Cambridge University Press, 2003.
In preparation. Draft from April 1997 available electronically.
Available electronically
-
Iliano Cervesato and Frank Pfenning.
A linear logical framework.
Information & Computation, 179(1):19-75, November 2002.
[PDF]
[PS]
-
Bor-Yuh Evan Chang, Karl Crary, Margaret DeLap, Robert Harper, Jason Liszka,
Tom Murphy VII, and Frank Pfenning.
Trustless grid computing in ConCert.
In M. Parashar, editor, Proceedings of the 3rd International
Workshop on Grid Computing (GRID'02), pages 112-125, Baltimore, Maryland,
November 2002. Springer-Verlag LNCS 2536.
[PDF]
[PS]
-
Frank Pfenning, editor.
Proceedings of the 3rd International Workshop on Logical
Frameworks and Meta-Languages (LFM'02), volume 70(2) of Electronic
Notes in Theoretical Computer Science, Copenhagen, Denmark, July 2002.
Available electronically
-
Frank Pfenning.
Logical frameworks - a brief introduction.
In H. Schwichtenberg and R. Steinbrüggen, editors, Proof and
System-Reliability, volume 62 of NATO Science Series II, pages
137-166. Kluwer Academic Publishers, 2002.
Lecture notes from the Marktoberdorf Summer School, July 2001.
[PDF]
[PS]
-
Andreas Abel, Bor-Yuh Evan Chang, and Frank Pfenning.
Human-readable, machine-verifiable proofs for teaching constructive
logic.
In Proceedings of the Workshop on Proof Transformations, Proof
Presentations and Complexity of Proofs (PTP'01), Siena, Italy, June 2001.
[PDF]
[PS]
-
Karl Crary, Robert Harper, Peter Lee, and Frank Pfenning.
Modules matter most.
Position paper presented at the NSF Workshop on New Visions
for Software Design and Productivity, December 2001.
Nashville, Tennessee.
[PDF]
[PS]
-
Rowan Davies and Frank Pfenning.
A modal analysis of staged computation.
Journal of the ACM, 48(3):555-604, May 2001.
[PDF]
[PS]
-
Frank Pfenning.
Logical frameworks at CMU.
ALP Newsletter, 14(2), May 2001.
Available electronically
-
Frank Pfenning.
Logical frameworks.
In Alan Robinson and Andrei Voronkov, editors, Handbook of
Automated Reasoning, chapter 17, pages 1063-1147. Elsevier Science and MIT
Press, 2001.
[PDF]
[PS]
-
Frank Pfenning.
Intensionality, extensionality, and proof irrelevance in modal type
theory.
In J. Halpern, editor, Proceedings of the 16th Annual Symposium
on Logic in Computer Science (LICS'01), pages 221-230, Boston,
Massachusetts, June 2001. IEEE Computer Society Press.
[PDF]
[PS]
-
Frank Pfenning and Rowan Davies.
A judgmental reconstruction of modal logic.
Mathematical Structures in Computer Science, 11:511-540, 2001.
Notes to an invited talk at the Workshop on Intuitionistic Modal
Logics and Applications (IMLA'99), Trento, Italy, July 1999.
[PDF]
[PS]
-
Carsten Schürmann, Joëlle Despeyroux, and Frank Pfenning.
Primitive recursion for higher-order abstract syntax.
Theoretical Computer Science, 266:1-57, 2001.
-
Iliano Cervesato, Joshua S. Hodas, and Frank Pfenning.
Efficient resource management for linear logic proof search.
Theoretical Computer Science, 232(1-2):133-163, February
2000.
Special issue on Proof Search in Type-Theoretic Languages, D.
Galmiche and D. Pym, editors.
[PDF]
[PS]
-
Rowan Davies and Frank Pfenning.
Intersection types and computational effects.
In P. Wadler, editor, Proceedings of the Fifth International
Conference on Functional Programming (ICFP'00), pages 198-208, Montreal,
Canada, September 2000. ACM Press.
[PDF]
[PS]
-
Maurizio Gabrielli and Frank Pfenning, editors.
Proceedings of the International Conference on Principles and
Practice of Declarative Programming (PPDP'00), Ottawa, Canada, September
2000. ACM Press.
-
Frank Pfenning.
Structural cut elimination I. intuitionistic and classical logic.
Information and Computation, 157(1/2):84-141, March 2000.
[PDF]
-
Frank Pfenning.
On the logical foundations of staged computation.
In Julia Lawall, editor, Proceedings of the Workshop on Partial
Evaluation and Semantics-Based Program Manipulation (PEPM'00), page 33,
Boston, Massachusetts, January 2000. ACM Press.
Abstract of invited talk.
Available electronically
-
Frank Pfenning.
Reasoning about staged computation.
In W. Taha, editor, Proceedings of the International Workshop on
Semantics, Applications, and Implementation of Program Generation (SAIG
2000), pages 5-6, Montreal, Canada, September 2000. Springer-Verlag LNCS
1924.
Abstract of invited talk.
Available electronically
-
Brigitte Pientka and Frank Pfenning.
Termination and reduction checking in the logical framework.
In Carsten Schürmann, editor, Workshop on Automation of
Proofs by Mathematical Induction, Pittsburgh, Pennsylvania, June 2000.
[PDF]
[PS]
-
Jeff Polakow and Frank Pfenning.
Properties of terms in continuation-passing style in an ordered
logical framework.
In Joëlle Despeyroux, editor, 2nd Workshop on Logical
Frameworks and Meta-languages (LFM'00), Santa Barbara, California, June
2000.
Proceedings available as INRIA Technical Report.
[PDF]
[PS]
-
Olivier Danvy, Belmina Dzafic, and Frank Pfenning.
On proving syntactic properties of CPS programs.
In Andrew Gordon and Andrew Pitts, editors, Proceedings of the
Third International Workshop on Higher Order Operational Techniques in
Semantics (HOOTS'99), Paris, September 1999.
Electronic Notes in Theoretical Computer Science, Volume 26.
[PDF]
[PS]
Available electronically
-
Alberto Momigliano and Frank Pfenning.
The relative complement problem for higher-order patterns.
In D. De Schreye, editor, Proceedings of the International
Conference on Logic Programming (ICLP'99), pages 380-394, Las Cruces, New
Mexico, November 1999. MIT Press.
[PDF]
[PS]
-
Frank Pfenning and Carsten Schürmann.
System description: Twelf - a meta-logical framework for deductive
systems.
In H. Ganzinger, editor, Proceedings of the 16th International
Conference on Automated Deduction (CADE-16), pages 202-206, Trento, Italy,
July 1999. Springer-Verlag LNAI 1632.
[PDF]
[PS]
-
Frank Pfenning.
Logical and meta-logical frameworks.
In G. Nadathur, editor, Proceedings of the International
Conference on Principles and Practice of Declarative Programming (PPDP'99),
page 206, Paris, France, September 1999. Springer-Verlag LNCS 1702.
Abstract of invited talk.
-
Mark Plesko and Frank Pfenning.
A formalization of the proof-carrying code architecture in a linear
logical framework.
In A. Pnueli and P. Traverso, editors, Proceedings of the FLoC
Workshop on Run-Time Result Verification, Trento, Italy, July 1999.
[PDF]
[PS]
-
Jeff Polakow and Frank Pfenning.
Relating natural deduction and sequent calculus for intuitionistic
non-commutative linear logic.
In Andre Scedrov and Achim Jung, editors, Proceedings of the
15th Conference on Mathematical Foundations of Programming Semantics, New
Orleans, Louisiana, April 1999.
Electronic Notes in Theoretical Computer Science, Volume 20.
[PDF]
[PS]
-
Jeff Polakow and Frank Pfenning.
Natural deduction for intuitionistic non-commutative linear logic.
In J.-Y. Girard, editor, Proceedings of the 4th International
Conference on Typed Lambda Calculi and Applications (TLCA'99), pages
295-309, L'Aquila, Italy, April 1999. Springer-Verlag LNCS 1581.
[PDF]
[PS]
-
Hongwei Xi and Frank Pfenning.
Dependent types in practical programming.
In A. Aiken, editor, Conference Record of the 26th Symposium on
Principles of Programming Languages (POPL'99), pages 214-227. ACM Press,
January 1999.
[PDF]
[PS]
-
Gilles Dowek, Thérèse Hardin, Claude Kirchner, and Frank Pfenning.
Unification via explicit substitutions: The case of higher-order
patterns.
Rapport de Recherche 3591, INRIA, December 1998.
Preliminary version appeared at JICSLP'96.
[PS]
-
Robert Harper and Frank Pfenning.
A module system for a programming language based on the LF logical
framework.
Journal of Logic and Computation, 8(1):5-31, 1998.
-
Robert Harper, Peter Lee, and Frank Pfenning.
The Fox project: Advanced language technology for extensible
systems.
Technical Report CMU-CS-98-107, Department of Computer Science,
Carnegie Mellon University, January 1998.
[PDF]
[PS]
-
Frank Pfenning.
Reasoning about deductions in linear logic.
In Claude Kirchner and Hélène Kirchner, editors, Proceedings of the 15th International Conference on Automated Deduction
(CADE-15), pages 1-2, Lindau, Germany, July 1998. Springer-Verlag LNCS
1421.
Abstract for invited talk.
[PDF]
[PS]
-
Frank Pfenning and Carsten Schürmann.
Twelf User's Guide, 1.2 edition, September 1998.
Available as Technical Report CMU-CS-98-173, Carnegie Mellon
University.
-
Frank Pfenning and Carsten Schürmann.
Algorithms for equality and unification in the presence of notational
definitions.
In T. Altenkirch, W. Naraschewski, and B. Reus, editors, Types
for Proofs and Programs, pages 179-193, Kloster Irsee, Germany, March 1998.
Springer-Verlag LNCS 1657.
[PDF]
[PS]
-
Jeff Polakow and Frank Pfenning.
Ordered linear logic programming.
Technical Report CMU-CS-98-183, Department of Computer Science,
Carnegie Mellon University, December 1998.
[PDF]
[PS]
-
Carsten Schürmann and Frank Pfenning.
Automated theorem proving in a simple meta-logic for LF.
In Claude Kirchner and Hélène Kirchner, editors, Proceedings of the 15th International Conference on Automated Deduction
(CADE-15), pages 286-300, Lindau, Germany, July 1998. Springer-Verlag LNCS
1421.
[PDF]
[PS]
-
Philip Wickline, Peter Lee, and Frank Pfenning.
Run-time code generation and modal-ML.
In Keith D. Cooper, editor, Proceedings of the Conference on
Programming Language Design and Implementation (PLDI'98), pages 224-235,
Montreal, Canada, June 1998. ACM Press.
[PDF]
[PS]
-
Philip Wickline, Peter Lee, Frank Pfenning, and Rowan Davies.
Modal types as staging specifications for run-time code generation.
ACM Computing Surveys, 30(3es), September 1998.
[PDF]
[PS]
-
Hongwei Xi and Frank Pfenning.
Eliminating array bound checking through dependent types.
In Keith D. Cooper, editor, Proceedings of the Conference on
Programming Language Design and Implementation (PLDI'98), pages 249-257,
Montreal, Canada, June 1998. ACM Press.
[PDF]
[PS]
-
Iliano Cervesato and Frank Pfenning.
Linear higher-order pre-unification.
In Glynn Winskel, editor, Proceedings of the Twelfth Annual
Sumposium on Logic in Computer Science (LICS'97), pages 422-433, Warsaw,
Poland, June 1997. IEEE Computer Society Press.
[PDF]
[PS]
-
Iliano Cervesato and Frank Pfenning.
A linear spine calculus.
Technical Report CMU-CS-97-125, Department of Computer Science,
Carnegie Mellon University, April 1997.
[PDF]
[PS]
-
Iliano Cervesato and Frank Pfenning.
Linear higher-order pre-unification.
Submitted. Available as Technical Report CMU-CS-97-160, Department of
Computer Science, Carnegie Mellon University, July 1997.
[PDF]
[PS]
-
Joëlle Despeyroux, Frank Pfenning, and Carsten Schürmann.
Primitive recursion for higher-order abstract syntax.
In R. Hindley, editor, Proceedings of the Third International
Conference on Typed Lambda Calculus and Applications (TLCA'97), pages
147-163, Nancy, France, April 1997. Springer-Verlag LNCS 1210.
An extended version is available as Technical Report CMU-CS-96-172,
Carnegie Mellon University.
[PDF]
[PS]
-
Paliath Narendran, Frank Pfenning, and Richard Statman.
On the unification problem for Cartesian closed categories.
Journal of Symbolic Logic, 62(2):636-647, 1997.
-
Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, and
Hongwei Xi.
TPS: A theorem proving system for classical type theory.
Journal of Automated Reasoning, 16(3):321-353, June 1996.
-
Iliano Cervesato, Joshua S. Hodas, and Frank Pfenning.
Efficient resource management for linear logic proof search.
In R. Dyckhoff, H. Herre, and P. Schroeder-Heister, editors, Proceedings of the 5th International Workshop on Extensions of Logic
Programming, pages 67-81, Leipzig, Germany, March 1996. Springer-Verlag
LNAI 1050.
[PDF]
[PS]
-
Iliano Cervesato and Frank Pfenning.
A linear logical framework.
In E. Clarke, editor, Proceedings of the Eleventh Annual
Symposium on Logic in Computer Science, pages 264-275, New Brunswick, New
Jersey, July 1996. IEEE Computer Society Press.
[PDF]
[PS]
-
Rowan Davies and Frank Pfenning.
A modal analysis of staged computation.
In Guy Steele, Jr., editor, Proceedings of the 23rd Annual
Symposium on Principles of Programming Languages, pages 258-270, St.
Petersburg Beach, Florida, January 1996. ACM Press.
[PDF]
[PS]
-
Gilles Dowek, Thérèse Hardin, Claude Kirchner, and Frank Pfenning.
Unification via explicit substitutions: The case of higher-order
patterns.
In M. Maher, editor, Proceedings of the Joint International
Conference and Symposium on Logic Programming, pages 259-273, Bonn,
Germany, September 1996. MIT Press.
[PDF]
[PS]
-
Frank Pfenning.
The practice of logical frameworks.
In Hélène Kirchner, editor, Proceedings of the
Colloquium on Trees in Algebra and Programming, pages 119-134,
Linköping, Sweden, April 1996. Springer-Verlag LNCS 1059.
Invited talk.
[PDF]
[PS]
-
Ekkehard Rohwedder and Frank Pfenning.
Mode and termination checking for higher-order logic programs.
In Hanne Riis Nielson, editor, Proceedings of the European
Symposium on Programming, pages 296-310, Linköping, Sweden, April 1996.
Springer-Verlag LNCS 1058.
[PDF]
[PS]
-
Olivier Danvy and Frank Pfenning.
The occurrence of continuation parameters in CPS terms.
Technical Report CMU-CS-95-121, Department of Computer Science,
Carnegie Mellon University, February 1995.
[PDF]
[PS]
-
Frank Pfenning.
Structural cut elimination.
In D. Kozen, editor, Proceedings of the Tenth Annual Symposium
on Logic in Computer Science, pages 156-166, San Diego, California, June
1995. IEEE Computer Society Press.
[PDF]
[PS]
-
Frank Pfenning and Hao-Chi Wong.
On a modal lambda-calculus for S4.
In S. Brookes and M. Main, editors, Proceedings of the Eleventh
Conference on Mathematical Foundations of Programming Semantics, New
Orleans, Louisiana, March 1995.
Electronic Notes in Theoretical Computer Science, Volume 1,
Elsevier.
[PDF]
[PS]
-
Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, and
Hongwei Xi.
TPS: An interactive and automatic tool for proving theorems of type
theory.
In Jeffrey J. Joyce and Carl-Johan H. Seger, editors, Proceedings of the 6th International Workshop on Higher Order Logic Theorem
Proving and Its Applications, pages 366-370, Vancouver, B.C., Canada,
August 1993. Springer-Verlag LNCS 780.
-
Robert Harper, Peter Lee, Frank Pfenning, and Eugene Rollins.
A compilation manager for Standard ML of New Jersey.
In Didier Rémy, editor, Record of the 1994 ACM SIGPLAN
Workshop on ML and it Applications, pages 136-147, Orlando, Florida, June
1994. INRIA Technical Report 2265.
Available as Technical Report CMU-CS-94-116.
-
Frank Pfenning.
Elf: A meta-language for deductive systems.
In A. Bundy, editor, Proceedings of the 12th International
Conference on Automated Deduction, pages 811-815, Nancy, France, June 1994.
Springer-Verlag LNAI 814.
System abstract.
[PDF]
[PS]
-
Frank Pfenning, editor.
Logic Programming and Automated Reasoning, 5th International
Conference, LPAR'94, Kiev, Ukraine, July 1994. Springer-Verlag LNAI 822.
-
Frank Pfenning.
Structural cut elimination in linear logic.
Technical Report CMU-CS-94-222, Department of Computer Science,
Carnegie Mellon University, December 1994.
[PDF]
[PS]
-
Frank Pfenning.
Logical frameworks.
Home page and bibliography
on the World-Wide Web, October 1994.
-
Michael Kohlhase and Frank Pfenning.
Unification in a lambda-calculus with intersection types.
In Dale Miller, editor, Proceedings of the International Logic
Programming Symposium, pages 488-505, Vancouver, Canada, October 1993. MIT
Press.
[PDF]
[PS]
-
Spiro Michaylov and Frank Pfenning.
Higher-order logic programming as constraint logic programming.
In Position Papers for the First Workshop on Principles and
Practice of Constraint Programming, pages 221-229, Newport, Rhode Island,
April 1993. Brown University.
[PDF]
[PS]
-
Paliath Narendran, Frank Pfenning, and Richard Statman.
On the unification problem for Cartesian closed categories.
In Moshe Vardi, editor, Eighth Annual IEEE Symposium on Logic
in Computer Science, pages 57-63, Montreal, Canada, June 1993.
[PDF]
[PS]
-
Frank Pfenning.
On the undecidability of partial polymorphic type reconstruction.
Fundamenta Informaticae, 19(1,2):185-199, 1993.
Preliminary version available as Technical Report CMU-CS-92-105,
School of Computer Science, Carnegie Mellon University, January 1992.
[PDF]
[PS]
-
Frank Pfenning.
Refinement types for logical frameworks.
In Herman Geuvers, editor, Informal Proceedings of the Workshop
on Types for Proofs and Programs, pages 285-299, Nijmegen, The Netherlands,
May 1993.
[PDF]
[PS]
-
Scott Dietzen and Frank Pfenning.
Higher-order and modal logic as a framework for explanation-based
generalization.
Machine Learning, 9:23-55, 1992.
-
John Hannan and Frank Pfenning.
Compiler verification in LF.
In Andre Scedrov, editor, Seventh Annual IEEE Symposium on
Logic in Computer Science, pages 407-418, Santa Cruz, California, June
1992.
[PDF]
[PS]
-
Spiro Michaylov and Frank Pfenning.
An empirical study of the runtime behavior of higher-order logic
programs.
In D. Miller, editor, Proceedings of the Workshop on the
lambda Prolog Programming Language, pages 257-271, Philadelphia,
Pennsylvania, July 1992. University of Pennsylvania.
Available as Technical Report MS-CIS-92-86.
[PDF]
[PS]
-
Gopalan Nadathur and Frank Pfenning.
The type system of a higher-order logic programming language.
In Frank Pfenning, editor, Types in Logic Programming, pages
245-283. MIT Press, 1992.
-
Frank Pfenning, editor.
Types in Logic Programming.
MIT Press, Cambridge, Massachusetts, 1992.
-
Frank Pfenning and Ekkehard Rohwedder.
Implementing the meta-theory of deductive systems.
In D. Kapur, editor, Proceedings of the 11th International
Conference on Automated Deduction, pages 537-551, Saratoga Springs, New
York, June 1992. Springer-Verlag LNAI 607.
[PDF]
[PS]
-
Frank Pfenning.
Dependent types in logic programming.
In Frank Pfenning, editor, Types in Logic Programming,
chapter 10, pages 285-311. MIT Press, Cambridge, Massachusetts, 1992.
-
Scott Dietzen and Frank Pfenning.
A declarative alternative to assert in logic programming.
In Vijay Saraswat and Kazunori Ueda, editors, International
Logic Programming Symposium, pages 372-386. MIT Press, October 1991.
[PDF]
[PS]
-
Conal Elliott and Frank Pfenning.
A semi-functional implementation of a higher-order logic programming
language.
In Peter Lee, editor, Topics in Advanced Language
Implementation, pages 289-325. MIT Press, 1991.
Available electronically
-
Tim Freeman and Frank Pfenning.
Refinement types for ML.
In Proceedings of the SIGPLAN '91 Symposium on Language Design
and Implementation, pages 268-277, Toronto, Ontario, June 1991. ACM Press.
[PDF]
[PS]
-
Spiro Michaylov and Frank Pfenning.
Compiling the polymorphic lambda-calculus.
In Paul Hudak and Neil Jones, editors, Proceedings of the
Symposium on Partial Evaluation and Semantics Based Program Manipulation,
pages 285-296, New Haven, Connecticut, June 1991. ACM Press.
Published in SIGPLAN Notices 26(9), September 1991.
-
Spiro Michaylov and Frank Pfenning.
Natural semantics and some of its meta-theory in Elf.
In L.-H. Eriksson, L. Hallnäs, and P. Schroeder-Heister, editors,
Proceedings of the Second International Workshop on Extensions of Logic
Programming, pages 299-344, Stockholm, Sweden, January 1991.
Springer-Verlag LNAI 596.
[PDF]
[PS]
-
Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov.
Uniform proofs as a foundation for logic programming.
Annals of Pure and Applied Logic, 51:125-157, 1991.
-
Frank Pfenning.
Logic programming in the LF logical framework.
In Gérard Huet and Gordon Plotkin, editors, Logical
Frameworks, pages 149-181. Cambridge University Press, 1991.
[PDF]
[PS]
-
Frank Pfenning.
Unification and anti-unification in the Calculus of
Constructions.
In Sixth Annual IEEE Symposium on Logic in Computer Science,
pages 74-85, Amsterdam, The Netherlands, July 1991.
[PDF]
[PS]
-
Frank Pfenning and Peter Lee.
Metacircularity in the polymorphic lambda-calculus.
Theoretical Computer Science, 89:137-159, 1991.
-
Peter B. Andrews, Sunil Issar, Dan Nesmith, and Frank Pfenning.
The TPS theorem proving system.
In M.E. Stickel, editor, 10th International Conference on
Automated Deduction, pages 641-642, Kaiserslautern, Germany, July 1990.
Springer-Verlag LNCS 449.
System abstract.
-
Amy Felty, Elsa Gunter, Dale Miller, and Frank Pfenning.
Tutorial on lambda Prolog.
In M.E. Stickel, editor, Proceedings of the 10th International
Conference on Automated Deduction, page 682, Kaiserslautern, Germany, July
1990. Springer-Verlag LNCS 449.
Abstract.
-
Robert Harper, Peter Lee, and Frank Pfenning.
Foundations of programming: Aspects of research in Ergo.
In Computer Science Research Review 1988/1989, pages 29-37.
School of Computer Science, Carnegie Mellon University, 1990.
-
Frank Pfenning and Daniel Nesmith.
Presenting intuitive deductions via symmetric simplification.
In M.E. Stickel, editor, 10th International Conference on
Automated Deduction, pages 336-350, Kaiserslautern, Germany, July 1990.
Springer-Verlag LNCS 449.
-
Frank Pfenning.
Program development through proof transformation.
Contemporary Mathematics, 106:251-262, 1990.
-
Frank Pfenning.
Types in logic programming.
In David H.D. Warren and Peter Szeredi, editors, Proceedings of
the Seventh International Conference on Logic Programming. MIT Press, June
1990.
Abstract of advanced tutorial.
-
Scott Dietzen and Frank Pfenning.
Higher-order and modal logic as a framework for explanation-based
generalization.
In Alberto Maria Segre, editor, Sixth International Workshop on
Machine Learning, pages 447-449, San Mateo, California, June 1989. Morgan
Kaufmann Publishers.
Expanded version available as Technical Report CMU-CS-89-160,
Carnegie Mellon University.
-
Scott Dietzen and Frank Pfenning.
Explanation-based learning in logic programming.
Ergo Report 89-086, Carnegie Mellon University, November 1989.
-
Peter Lee, Mark Leone, Spiro Michaylov, and Frank Pfenning.
Towards a practical programming language based on the polymorphic
lambda calculus.
Ergo Report 89-085, School of Computer Science, Carnegie Mellon
University, November 1989.
-
Frank Pfenning.
Review of ``Jean H. Gallier: Logic for Computer Science, Harper
& Row, New York 1986''.
Journal of Symbolic Logic, 54(1):288-289, March 1989.
-
Frank Pfenning.
Elf: A language for logic definition and verified meta-programming.
In Fourth Annual Symposium on Logic in Computer Science, pages
313-322, Pacific Grove, California, June 1989. IEEE Computer Society Press.
[PDF]
[PS]
-
Frank Pfenning and Christine Paulin-Mohring.
Inductively defined types in the Calculus of Constructions.
In M. Main, A. Melton, M. Mislove, and D. Schmidt, editors, Proceedings of the Fifth Conference on the Mathematical Foundations of
Programming Semantics, Tulane University, New Orleans, Louisiana, pages
209-228. Springer-Verlag LNCS 442, March 1989.
-
Frank Pfenning and Peter Lee.
LEAP: A language with eval and polymorphism.
In Proceedings of the International Joint Conference on Theory
and Practice in Software Development, pages 345-359, Barcelona, Spain,
March 1989. Springer-Verlag LNCS 352.
-
Peter Lee, Frank Pfenning, Gene Rollins, and William Scherlis.
The Ergo Support System: An integrated set of tools for prototyping
integrated environments.
In Peter Henderson, editor, Proceedings of the ACM
SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software
Development Environments, pages 25-34. ACM Press, November 1988.
-
Peter Lee, Frank Pfenning, John Reynolds, Gene Rollins, and Dana Scott.
Research on semantically based program-design environments: The Ergo
Project in 1988.
Technical Report CMU-CS-88-118, Carnegie Mellon University, March
1988.
-
Robert L. Nord and Frank Pfenning.
The Ergo attribute system.
In Peter Henderson, editor, Proceedings of the ACM
SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software
Development Environments, pages 110-120. ACM Press, November 1988.
-
Frank Pfenning.
Single axioms in the implicational propositional calculus.
In Ewing Lusk and Ross Overbeek, editors, Proceedings of the 9th
International Conference on Automated Deduction, pages 710-713, Argonne,
Illinois, May 1988. Springer-Verlag LNCS 310.
Problem set.
-
Frank Pfenning.
Partial polymorphic type inference and higher-order unification.
In Proceedings of the 1988 ACM Conference on Lisp and
Functional Programming, pages 153-163, Snowbird, Utah, July 1988. ACM
Press.
Available electronically
-
Frank Pfenning and Conal Elliott.
Higher-order abstract syntax.
In Proceedings of the ACM SIGPLAN '88 Symposium on Language
Design and Implementation, pages 199-208, Atlanta, Georgia, June 1988.
[PDF]
[PS]
-
Conal Elliott and Frank Pfenning.
A family of program derivations for higher-order unification.
Ergo Report 87-045, Carnegie Mellon University, November 1987.
-
Frank Pfenning.
Proof Transformations in Higher-Order Logic.
PhD thesis, Carnegie Mellon University, January 1987.
-
Peter B. Andrews, Dale Miller, Eve Cohen, and Frank Pfenning.
Automating higher-order logic.
Contemporary Mathematics, 29:169-192, August 1984.
-
Frank Pfenning.
Analytic and non-analytic proofs.
In R.E. Shostak, editor, Proceedings of the 7th Conference on
Automated Deduction, pages 394-413, Napa, California, May 1984.
Springer-Verlag LNCS 170.
[ Home
| Contact
| Research
| Publications
| CV
| Students
]
[ Projects
| Courses
| Conferences
| Organizations
| Journals
]
[ Logical Frameworks
| Pittsburgh Squash Racquets Assocation
]
http://www.cs.cmu.edu/~fp
|