
Frank Pfenning
Publications
The most recent drafts and publications
are listed on my home page.
Last Updated: Sat December 7 2013
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.

Luís Caires, Frank Pfenning, and Bernardo Toninho.
Linear logic propositions as session types.
Mathematical Structures in Computer Science, 2013.
To appear. Special Issue on Behavioural Types.
[PDF]

Frank Pfenning, editor.
Proceedings of the 16th International Conference on Foundations
of Software Science and Computation Structures, ETAPS 2013, Rome, Italy,
March 2013. Springer LNCS 7794.
[PDF]

Bernardo Toninho, Luís Caires, and Frank Pfenning.
Higherorder processes, functions, and sessions: A monadic
integration.
In M.Felleisen and P.Gardner, editors, Proceedings of the
European Symposium on Programming (ESOP'13), pages 350369, Rome, Italy,
March 2013. Springer LNCS 7792.
[PDF]

Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho.
Behavioral polymorphism and parametricity in sessionbased
communication.
In M.Felleisen and P.Gardner, editors, Proceedings of the
European Symposium on Programming (ESOP'13), pages 330349, Rome, Italy,
March 2013. Springer LNCS 7792.
[PDF]

Deepak Garg and Frank Pfenning.
Stateful authorization logic  proof theory and a case study.
Journal of Computer Security, 20(4):353391, 2012.
[PDF]

Iliano Cervesato, Frank Pfenning, Jorge Luis Sacchini, Carsten Schürmann,
and Robert J. Simmons.
Trace matching in a concurrent logical framework.
In A. Chlipala and C. Schürmann, editors, Proceedings of the
7th International Workshop on Logical Frameworks and Metalanguages: Theory
and Practice, Copenhagen, Denmark, September 2012. ACM.
[PDF]

Iliano Cervesato, Frank Pfenning, Jorge Luis Sacchini, Carsten Schürmann,
and Robert J. Simmons.
On matching concurrent traces.
In S. Escobar, K. Korovin, and V. Rybakov, editors, Proceedings
of the 26th International Workshop on Unification, July 2012.
[PDF]

Henry DeYoung, Luís Caires, Frank Pfenning, and Bernardo Toninho.
Cut reduction in linear logic as asynchronous sessiontyped
communication.
In P. Cégielski and A. Durand, editors, Proceedings of the
21st Conference on Computer Science Logic, CSL 2012, pages 228242,
Fontainebleau, France, September 2012. Leibniz International Proceedings in
Informatics.
[PDF]

Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho.
Termination in sessionbased concurrency via linear logical
relations.
In H. Seidl, editor, 22nd European Symposium on Programming,
ESOP'12, pages 539558, Tallinn, Estonia, March 2012. Springer LNCS 7211.
[PDF]

Bernardo Toninho, Luís Caires, and Frank Pfenning.
Functions as sessiontyped processes.
In L. Birkedal, editor, 15th International Conference on
Foundations of Software Science and Computation Structures, FoSSaCS'12,
pages 346360, Tallinn, Estonia, March 2012. Springer LNCS.
[PDF]

Flávio Cruz, Michael AshleyRollman, Seth Copen Goldstein inad
Ricardo Rocha, and Frank Pfenning.
Bottomup logic programming for multicores.
In Proceedings of the Workshop on Declarative Aspects of
Multicore Programming, DAMP'12, Philadelphia, PA, January 2012. ACM Press.
Short paper.
[PDF]

Robert J. Simmons and Frank Pfenning.
Logical approximation for program analysis.
HigherOrder and Symbolic Computation, 24(12):4180, 2011.
[PDF]

Frank Pfenning, Luís Caires, and Bernardo Toninho.
Proofcarrying code in a sessiontyped process calculus.
In 1st International Conference on Certified Programs and
Proofs, CPP'11, pages 2136, Kenting, Taiwan, December 2011. Springer LNCS
7086.
[PDF]

Frank Pfenning, Thomas J. Cortina, and William Lovas.
Teaching imperative programming with contracts at the freshmen level.
Experience report. Unpublished manuscript, September 2011.
[PDF]

Bernardo Toninho, Luís Caires, and Frank Pfenning.
Dependent session types via intuitionistic linear type theory.
In Proceedings of the 13th International Conference on
Principles and Practice of Declarative Programming, PPDP'11, pages 161172,
Odense, Denmark, July 2011. ACM.
[PDF]

Jamie Morgenstern, Deepak Garg, and Frank Pfenning.
A proofcarrying file system with revocable and useonce
certificates.
In C.Meadows and C.FernandezGago, editors, Proceedings of the
7th International Workshop on Security and Trust Management (STM 2011),
Copenhagen, Denmark, June 2011. Springer LNCS.
[PDF]

Robert J. Simmons, Bernardo Toninho, and Frank Pfenning.
Distributed deductive databases, declaratively.
Short paper, ACM SIGPLAN X10 Workshop, June 2011.
[PDF]

Robert J. Simmons and Frank Pfenning.
Weak focusing for ordered linear logic.
Technical Report CMUCS10147, Carnegie Mellon University, 2011.
Revision of April 2011.
[PDF]

Deepak Garg and Frank Pfenning.
Stateful authorization logic  proof theory and a case study.
In J.Cuellar and J.Lopez, editors, Proceedings of the 6th
International Workshop on Security and Trust Management (STM'10), Athens,
Greece, September 2010. Springer LNCS.
[PDF]

Luís Caires and Frank Pfenning.
Session types as intuitionistic linear propositions.
In Proceedings of the 21st International Conference on
Concurrency Theory (CONCUR 2010), pages 222236, Paris, France, August
2010. Springer LNCS 6269.
[PDF]

Deepak Garg and Frank Pfenning.
A proofcarrying file system.
In D.Evans and G.Vigna, editors, Proceedings of the 31st
Symposium on Security and Privacy (Oakland 2010), pages 349364, Berkeley,
California, May 2010. IEEE.
Extended version available as Technical Report CMUCS09123, June
2009.
[PDF]

William Lovas and Frank Pfenning.
Refinement types for logical frameworks and their interpretation as
proof irrelevance.
Logical Methods in Computer Science, 6(4):150, December 2010.
[PDF]

Frank Pfenning.
Possession as linear knowledge.
In B.Farwer, editor, Proceedings of the 3rd International
Workshop on Logics, Agents, and Mobility (LAM 2010), Edinburgh, Scotland,
July 2010.
Abstract of invited talk.
[PDF]

Frank Pfenning.
The practice and promise of substructural frameworks.
In K.Crary and M.Miculan, editors, Proceedings of 5th
International Workshop on Logical Frameworks and MetaLanguages: Theory and
Practice (LFMTP 2010), pages 12, Edinburgh, Scotland, July 2010.
Abstract of invited talk.

Jason C. Reed and Frank Pfenning.
Focuspreserving embeddings of substructural logics in intuitionistic
logic.
Unpublished Manuscript, January 2010.
[PDF]

Robert J. Simmons and Frank Pfenning.
Logical approximation for program analysis.
Submitted to the Journal on HigherOrder and Symbolic Computation,
March 2010.
[PDF]

Henry DeYoung and Frank Pfenning.
Reasoning about the consequences of authorization policies in a
linear epistemic logic.
In Workshop on Foundations of Computer Security (FCS'09), Los
Angeles, California, August 2009.
[PDF]

Deepak Garg, Frank Pfenning, Denis Serenyi, and Brian Witten.
A logical representation of common rule for controlling access to
classified information.
Technical Report CMUCS09139, Carnegie Mellon University, June
2009.
[PDF]

William Lovas and Frank Pfenning.
Refinement types as proof irrelevance.
In P.L. Curien, editor, Proceedings of the 9th International
Conference on Typed Lambda Calculi and Applications (TLCA 2009), pages
157171, Brasilia, Brazil, July 2009. Springer LNCS 5608.
[PDF]

Sean McLaughlin and Frank Pfenning.
Efficient intuitionistic theorem proving with the polarized inverse
method.
In R.A.Schmidt, editor, Proceedings of the 22nd International
Conference on Automated Deduction (CADE22), pages 230244, Montreal,
Canada, August 2009. Springer LNCS 5663.
[PDF]

Frank Pfenning and Robert J. Simmons.
Substructural operational semantics as ordered logic programming.
In Proceedings of the 24th Annual Symposium on Logic in Computer
Science (LICS 2009), pages 101110, Los Angeles, California, August 2009.
IEEE Computer Society Press.
[PDF]

Robert J. Simmons and Frank Pfenning.
Linear logical approximations.
In G. Puebla and G. Vidal, editors, Proceedings of the Workshop
on Partial Evaluation and Program Manipulation, pages 920, Savannah,
Georgia, January 2009. ACM SIGPLAN.
[PDF]

Kaustuv Chaudhuri, Frank Pfenning, and Greg Price.
A logical characterization of forward and backward chaining in the
inverse method.
Journal of Automated Reasoning, 40(23):133177, 2008.
Special issue with selected papers from IJCAR 2006.
[PDF]

Henry DeYoung, Deepak Garg, and Frank Pfenning.
An authorization logic with explicit time.
In Proceedings of the 21st Computer Security Foundations
Symposium (CSF21), pages 133145, Pittsburgh, Pennsylvania, June 2008.
IEEE Computer Society Press.
Extended version available as Technical Report CMUCS07166, revised
February 2008.
[PDF]

Sean McLaughlin and Frank Pfenning.
Imogen: Focusing the polarized inverse method for intuitionistic
propositional logic.
In I.Cervesato, H.Veith, and A.Voronkov, editors, Proceedings of
the 15th International Conference on Logic for Programming, Artificial
Intelligence, and Reasoning (LPAR'08), pages 174181, Doha, Qatar, November
2008. Springer LNCS 5330.
System Description.
[PDF]

Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka.
Contextual modal type theory.
Transactions on Computational Logic, 9(3), 2008.
[PDF]

Sungwoo Park, Frank Pfenning, and Sebastian Thrun.
A probabilistic language based upon sampling functions.
Transactions on Programming Languages and Systems, 31(1),
December 2008.
[PDF]

F. Pfenning, editor.
Proceedings of the 23rd Annual Symposium on Logic in Computer
Science (LICS 2008), Pittsburgh, Pennsylvania, June 2008. IEEE Computer
Society Press.

Frank Pfenning.
Church and Curry: Combining intrinsic and extrinsic typing.
In C.Benzmüller, C.Brown, J.Siekmann, and R.Statman, editors,
Reasoning in Simple Type Theory: Festschrift in Honor of Peter B.
Andrews on His 70th Birthday, Studies in Logic 17, pages 303338. College
Publications, 2008.
[PDF]

Robert J. Simmons and Frank Pfenning.
Linear logical algorithms.
In Proceedings of the 35th International Colloquium on Automata,
Languages and Programming (ICALP'08), pages 336345, Reykjavik, Iceland,
July 2008. Springer LNCS 5126.
[PDF]

Lujo Bauer, Frank Pfenning, and Michael K. Reiter.
Distributed system security via logical frameworks.
In Information Security Research: New Methods for Protecting
Against Cyber Threads, pages 108115. Department of Defense, Wiley
Publishing, 2007.

Kevin D. Bowers, Lujo Bauer, Deepak Garg, Frank Pfenning, and Michael K.
Reiter.
Consumable credentials in logicbased accesscontrol systems.
In Proceedings of the 14th Annual Network and Distributed System
Security Symposium (NDSS'07), pages 143157, San Diego, California,
February 2007. Internet Society.
Preliminary version available as Technical Report CMUCYLAB06002,
Carnegie Mellon University, February 2006.
[PDF]

Henry DeYoung, Deepak Garg, and Frank Pfenning.
An authorization logic with explicit time.
Technical Report CMUCS07166, Carnegie Mellon University,
Department of Computer Science, December 2007.
Revised February 2008.
[PDF]

Ruy LeyWild and Frank Pfenning.
Avoiding causal dependencies via proof irrelevance in a concurrent
logical framework.
Technical Report CMUCS07107, Carnegie Mellon University, February
2007.
[PDF]

William Lovas and Frank Pfenning.
A bidirectional refinement type system for LF.
In B. Pientka and C. Schürmann, editors, Proceedings of the
Second International Workshop on Logical Frameworks and MetaLanguages:
Theory and Practice, pages 113128, Bremen, Germany, July 2007. Electronic
Notes in Theoretical Computer Science (ENTCS), vol 196.
[PDF]

F. Pfenning, editor.
Proceedings of the 21st International Conference on Automated
Deduction (CADE21), Bremen, Germany, July 2007. Springer LNCS 4603.

Frank Pfenning.
On a logical foundation for explicit substitutions.
In S. Ronchi Della Rocca, editor, Proceedings of the 8th
International Conference on Typed Lambda Calculi and Applications (TLCA
2007), page 1, Paris, France, June 2007. Springer LNCS 4583.
Abstract of TLCA/RTA joint invited talk.

Frank Pfenning.
Subtyping and intersection types revisited.
In R. Hinze and N. Ramsey, editors, Proceedings of the 12th
International Symposium on Functional Programming (ICFP 2007), page 219,
Freiburg, Germany, October 2007. ACM Press.
Abstract of invited talk.

Jason Reed and Frank Pfenning.
Intuitionistic letcc via labelled deduction.
In Proceedings of the 5th Workshop on Methods for Modalities
(M4M5 2007), pages 91111, Cachan, France, November 2007.
Electronic Notes in Theoretical Computer Science (ENTCS), vol 213,
March 2009.
[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), pages 37053710, Rome Italy, April 2007. IEEE
Computer Society Press.
[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
97111, Seattle, Washington, August 2006. Springer LNCS 4130.
[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 297312, Hamburg, Germany, September 2006. Springer
LNCS 4189.
[PDF]

Deepak Garg and Frank Pfenning.
Noninterference in constructive authorization logic.
In J. Guttman, editor, Proceedings of the 19th Computer Security
Foundations Workshop (CSFW'06), pages 283293, Venice, Italy, July 2006.
IEEE Computer Society Press.
[PDF]

Frank Pfenning, editor.
Proceedings of the 17th International Conference on Rewriting
Techniques and Applications, Seattle, Washington, August 2006. Springer
Verlag LNCS 4098.

Kaustuv Chaudhuri and Frank Pfenning.
A focusing inverse method prover for firstorder linear logic.
In R.Nieuwenhuis, editor, Proceedings of the 20th International
Conference on Automated Deduction (CADE20), pages 6983, Tallinn, Estonia,
July 2005. Springer Verlag LNCS 3632.
[PDF]

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 200215, Oxford, England, August
2005. Springer Verlag LNCS 3634.
[PDF]

Karl Crary, Aleksey Kliger, and Frank Pfenning.
A monadic analysis of information flow security with mutable state.
Journal of Functional Programming, 15(2):249291, March 2005.
Preliminary version available as Technical Report CMUCS03164.
[PDF]

Deepak Garg and Frank Pfenning.
Typedirected concurrency.
In M.Abadi and L.de Alfaro, editors, Proceedings of the 16th
International Conference on Concurrency Theory (CONCUR'05), pages 620, San
Francisco, California, August 2005. Springer Verlag LNCS 3653.
[PDF]

Robert Harper and Frank Pfenning.
On equivalence and canonical forms in the LF type theory.
Transactions on Computational Logic, 6:61101, January 2005.
[PDF]

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 3546, Lisbon, Portugal, July 2005. ACM Press.
[PDF]

Aleksandar Nanevski and Frank Pfenning.
Staged computation with names and necessity.
Journal of Functional Programming, 15(6):837891, November
2005.
[PDF]

Sungwoo Park, Frank Pfenning, and Sebastian Thrun.
A probabilistic language based upon sampling functions.
In M.Abadi, editor, Conference Record of the 32nd Symposium on
Principles of Programming Languages (POPL'05), pages 171182, Long Beach,
California, January 2005. ACM Press.
[PDF]

Frank Pfenning.
Towards a type theory of contexts.
In Proceedings of the 3rd Workshop on Mechanized Reasoning About
Languages with Variable Binding (MERLIN'05), page 1, Tallinn, Estonia,
September 2005. ACM Press.
Abstract for invited talk.

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 1833, Park City, Utah, September 2004. Springer
LNCS 3223.
[PDF]

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):7592, 2004.
Available electronically

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 281292,
Venice, Italy, January 2004. ACM Press.
Extended version available as Technical Report CMUCS04117, March
2004.
[PDF]

Frank Pfenning.
Review of ``Benjamin C. Pierce: Types and programming languages,
The MIT Proess, Cambridge, Massachusetts, 2002''.
Bulletin of Symbolic Logic, 10:213214, 2004.
[PDF]

Frank Pfenning.
Substructural operational semantics and linear destinationpassing
style.
In W.N. Chin, editor, Proceedings of the 2nd Asian Symposium on
Programming Languages and Systems (APLAS'04), page 196, Taipei, Taiwan,
November 2004. SpringerVerlag LNCS 3302.
Abstract of invited talk.
[PDF]

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 286295, Turku,
Finland, July 2004. IEEE Computer Society Press.
Extended version available as Technical Report CMUCS04105.
[PDF]

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 355377. SpringerVerlag LNCS 3085, 2004.
Revised selected papers from the Third International Workshop on
Types for Proofs and Programs, Torino, Italy, April 2003.
[PDF]

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 MetaLanguages (LFM'04), Cork, Ireland,
July 2004. Electronic Notes in Theoretical Computer Science (ENTCS), vol 199,
pp. 133145, 2008.
[PDF]

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.
[PDF]

Iliano Cervesato and Frank Pfenning.
A linear spine calculus.
Journal of Logic and Computation, 13(5):639688, 2003.

BoyYuh Evan Chang, Kaustuv Chaudhuri, and Frank Pfenning.
A judgmental analysis of linear logic.
Technical Report CMUCS03131R, Carnegie Mellon University,
Department of Computer Science, December 2003.
[PDF]

Kaustuv Chaudhuri and Frank Pfenning.
Resource management for the inverse method in linear logic.
Draft manuscript, January 2003.
[PDF]

Christopher Colby, Karl Crary, Robert Harper, Peter Lee, and Frank Pfenning.
Automated techniques for provable safe mobile code.
Theoretical Computer Science, 290:11751199, 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. 406419, Hilton Head Island, South
Carolina, January 2000.
[PDF]

Joshua Dunfield and Frank Pfenning.
Type assignment for intersections and unions in callbyvalue
languages.
In A.D. Gordon, editor, Proceedings of the 6th International
Conference on Foundations of Software Science and Computation Structures
(FOSSACS'03), pages 250266, Warsaw, Poland, April 2003. SpringerVerlag
LNCS 2620.
[PDF]

Alberto Momigliano and Frank Pfenning.
Higherorder pattern complement and the strict lambdacalculus.
Transactions on Computational Logic, 4(4), October 2003.
[PDF]

Aleksandar Nanevski, Brigitte Pientka, and Frank Pfenning.
A modal foundation for metavariables.
In Proceedings of the Second Workshop on Mechanized Reasoning
about Languages with Variable Binding (MERLIN'03), Uppsala, Sweden, August
2003. ACM SIGPLAN.

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 172184,
New Orleans, Louisiana, January 2003. ACM Press.
Extended version available as Technical Report CMUCS02171,
December 2002.
[PDF]

Frank Pfenning and Yannis Smaragdakis, editors.
Proceedings of the Second International Conference on Generative
Programming and Component Engineering.
SpringerVerlag LNCS 2830, Erfurt, Germany, September 2003.

Brigitte Pientka and Frank Pfenning.
Optimizing higherorder pattern unification.
In F. Baader, editor, Proceedings of the 19th Conference on
Automated Deduction (CADE19), pages 473487, Miami Beach, Florida, July
2003. SpringerVerlag LNAI 2741.
[PDF]

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 120135, Rome, Italy, September 2003. SpringerVerlag LNCS
2758.
[PDF]

Iliano Cervesato and Frank Pfenning.
A linear logical framework.
Information & Computation, 179(1):1975, November 2002.
Revised and expanded version of an extended abstract, LICS 1996, pp.
264275.
[PDF]

Iliano Cervesato, Frank Pfenning, David Walker, and Kevin Watkins.
A concurrent logical framework II: Examples and applications.
Technical Report CMUCS02102, Department of Computer Science,
Carnegie Mellon University, 2002.
Revised May 2003.
[PDF]

BorYuh 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 112125, Baltimore, Maryland,
November 2002. SpringerVerlag LNCS 2536.
[PDF]

Frank Pfenning.
Logical frameworks  a brief introduction.
In H. Schwichtenberg and R. Steinbrüggen, editors, Proof and
SystemReliability, volume 62 of NATO Science Series II, pages
137166. Kluwer Academic Publishers, 2002.
Lecture notes from the Marktoberdorf Summer School, July 2001.
[PDF]

Frank Pfenning, editor.
Proceedings of the 3rd International Workshop on Logical
Frameworks and MetaLanguages (LFM'02), volume 70(2) of Electronic
Notes in Theoretical Computer Science, Copenhagen, Denmark, July 2002.
Available electronically

Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker.
A concurrent logical framework I: Judgments and properties.
Technical Report CMUCS02101, Department of Computer Science,
Carnegie Mellon University, 2002.
Revised May 2003.
[PDF]

Andreas Abel, BorYuh Evan Chang, and Frank Pfenning.
Humanreadable, machineverifiable 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]

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]

Rowan Davies and Frank Pfenning.
A modal analysis of staged computation.
Journal of the ACM, 48(3):555604, May 2001.
[PDF]

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 221230, Boston,
Massachusetts, June 2001. IEEE Computer Society Press.
[PDF]

Frank Pfenning.
Logical frameworks.
In Alan Robinson and Andrei Voronkov, editors, Handbook of
Automated Reasoning, chapter 17, pages 10631147. Elsevier Science and MIT
Press, 2001.
[PDF]

Frank Pfenning.
Logical frameworks at CMU.
ALP Newsletter, 14(2), May 2001.
Available electronically

Frank Pfenning and Rowan Davies.
A judgmental reconstruction of modal logic.
Mathematical Structures in Computer Science, 11:511540, 2001.
Notes to an invited talk at the Workshop on Intuitionistic Modal
Logics and Applications (IMLA'99), Trento, Italy, July 1999.
[PDF]

Carsten Schürmann, Joëlle Despeyroux, and Frank Pfenning.
Primitive recursion for higherorder abstract syntax.
Theoretical Computer Science, 266:157, 2001.

Iliano Cervesato, Joshua S. Hodas, and Frank Pfenning.
Efficient resource management for linear logic proof search.
Theoretical Computer Science, 232(12):133163, February
2000.
Special issue on Proof Search in TypeTheoretic Languages, D.
Galmiche and D. Pym, editors.
[PDF]

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 198208, Montreal,
Canada, September 2000. ACM Press.
[PDF]

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.
On the logical foundations of staged computation.
In Julia Lawall, editor, Proceedings of the Workshop on Partial
Evaluation and SemanticsBased Program Manipulation (PEPM'00), page 33,
Boston, Massachusetts, January 2000. ACM Press.

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 56, Montreal, Canada, September 2000. SpringerVerlag LNCS
1924.
Abstract of invited talk.
Available electronically

Frank Pfenning.
Structural cut elimination I. Intuitionistic and classical logic.
Information and Computation, 157(1/2):84141, March 2000.
[PDF]

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]

Jeff Polakow and Frank Pfenning.
Properties of terms in continuationpassing style in an ordered
logical framework.
In Joëlle Despeyroux, editor, 2nd Workshop on Logical
Frameworks and Metalanguages (LFM'00), Santa Barbara, California, June
2000.
Proceedings available as INRIA Technical Report.
[PDF]

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]
Available electronically

Alberto Momigliano and Frank Pfenning.
The relative complement problem for higherorder patterns.
In D. De Schreye, editor, Proceedings of the International
Conference on Logic Programming (ICLP'99), pages 380394, Las Cruces, New
Mexico, November 1999. MIT Press.
[PDF]

Frank Pfenning.
Logical and metalogical 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. SpringerVerlag LNCS 1702.
Abstract of invited talk.

Frank Pfenning and Carsten Schürmann.
System description: Twelf  a metalogical framework for deductive
systems.
In H. Ganzinger, editor, Proceedings of the 16th International
Conference on Automated Deduction (CADE16), pages 202206, Trento, Italy,
July 1999. SpringerVerlag LNAI 1632.
[PDF]

Mark Plesko and Frank Pfenning.
A formalization of the proofcarrying code architecture in a linear
logical framework.
In A. Pnueli and P. Traverso, editors, Proceedings of the FLoC
Workshop on RunTime Result Verification, Trento, Italy, July 1999.
[PDF]

Jeff Polakow and Frank Pfenning.
Natural deduction for intuitionistic noncommutative linear logic.
In J.Y. Girard, editor, Proceedings of the 4th International
Conference on Typed Lambda Calculi and Applications (TLCA'99), pages
295309, L'Aquila, Italy, April 1999. SpringerVerlag LNCS 1581.
[PDF]

Jeff Polakow and Frank Pfenning.
Relating natural deduction and sequent calculus for intuitionistic
noncommutative linear logic.
In Andre Scedrov and Achim Jung, editors, Proceedings of the
15th Conference on Mathematical Foundations of Programming Semantics, pages
449466, New Orleans, Louisiana, April 1999.
Electronic Notes in Theoretical Computer Science, Volume 20.
[PDF]

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 214227. ACM Press,
January 1999.
[PDF]

Gilles Dowek, Thérèse Hardin, Claude Kirchner, and Frank Pfenning.
Unification via explicit substitutions: The case of higherorder
patterns.
Rapport de Recherche 3591, INRIA, December 1998.
Preliminary version appeared at JICSLP'96.
[PDF]

Robert Harper, Peter Lee, and Frank Pfenning.
The Fox project: Advanced language technology for extensible
systems.
Technical Report CMUCS98107, Department of Computer Science,
Carnegie Mellon University, January 1998.
[PDF]

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):531, 1998.

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
(CADE15), pages 12, Lindau, Germany, July 1998. SpringerVerlag LNCS
1421.
Abstract for invited talk.
[PDF]

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 179193, Kloster Irsee, Germany, March 1998.
SpringerVerlag LNCS 1657.
[PDF]

Frank Pfenning and Carsten Schürmann.
Twelf User's Guide, 1.2 edition, September 1998.
Available as Technical Report CMUCS98173, Carnegie Mellon
University.

Jeff Polakow and Frank Pfenning.
Ordered linear logic programming.
Technical Report CMUCS98183, Department of Computer Science,
Carnegie Mellon University, December 1998.
[PDF]

Carsten Schürmann and Frank Pfenning.
Automated theorem proving in a simple metalogic for LF.
In Claude Kirchner and Hélène Kirchner, editors, Proceedings of the 15th International Conference on Automated Deduction
(CADE15), pages 286300, Lindau, Germany, July 1998. SpringerVerlag LNCS
1421.
[PDF]

Philip Wickline, Peter Lee, and Frank Pfenning.
Runtime code generation and modalML.
In Keith D. Cooper, editor, Proceedings of the Conference on
Programming Language Design and Implementation (PLDI'98), pages 224235,
Montreal, Canada, June 1998. ACM Press.
[PDF]

Philip Wickline, Peter Lee, Frank Pfenning, and Rowan Davies.
Modal types as staging specifications for runtime code generation.
ACM Computing Surveys, 30(3es), September 1998.
[PDF]

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 249257,
Montreal, Canada, June 1998. ACM Press.
[PDF]

Iliano Cervesato and Frank Pfenning.
Linear higherorder preunification.
In Glynn Winskel, editor, Proceedings of the Twelfth Annual
Sumposium on Logic in Computer Science (LICS'97), pages 422433, Warsaw,
Poland, June 1997. IEEE Computer Society Press.
[PDF]

Iliano Cervesato and Frank Pfenning.
A linear spine calculus.
Technical Report CMUCS97125, Department of Computer Science,
Carnegie Mellon University, April 1997.
[PDF]

Joëlle Despeyroux, Frank Pfenning, and Carsten Schürmann.
Primitive recursion for higherorder abstract syntax.
In R. Hindley, editor, Proceedings of the Third International
Conference on Typed Lambda Calculus and Applications (TLCA'97), pages
147163, Nancy, France, April 1997. SpringerVerlag LNCS 1210.
An extended version is available as Technical Report CMUCS96172,
Carnegie Mellon University.
[PDF]

Paliath Narendran, Frank Pfenning, and Richard Statman.
On the unification problem for Cartesian closed categories.
Journal of Symbolic Logic, 62(2):636647, 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):321353, 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. SchroederHeister, editors, Proceedings of the 5th International Workshop on Extensions of Logic
Programming, pages 6781, Leipzig, Germany, March 1996. SpringerVerlag
LNAI 1050.
[PDF]

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 264275, New Brunswick, New
Jersey, July 1996. IEEE Computer Society Press.
[PDF]

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 258270, St.
Petersburg Beach, Florida, January 1996. ACM Press.
[PDF]

Gilles Dowek, Thérèse Hardin, Claude Kirchner, and Frank Pfenning.
Unification via explicit substitutions: The case of higherorder
patterns.
In M. Maher, editor, Proceedings of the Joint International
Conference and Symposium on Logic Programming, pages 259273, Bonn,
Germany, September 1996. MIT Press.
[PDF]

Frank Pfenning.
The practice of logical frameworks.
In Hélène Kirchner, editor, Proceedings of the
Colloquium on Trees in Algebra and Programming, pages 119134,
Linköping, Sweden, April 1996. SpringerVerlag LNCS 1059.
Invited talk.
[PDF]

Ekkehard Rohwedder and Frank Pfenning.
Mode and termination checking for higherorder logic programs.
In Hanne Riis Nielson, editor, Proceedings of the European
Symposium on Programming, pages 296310, Linköping, Sweden, April 1996.
SpringerVerlag LNCS 1058.
[PDF]

Olivier Danvy and Frank Pfenning.
The occurrence of continuation parameters in CPS terms.
Technical Report CMUCS95121, Department of Computer Science,
Carnegie Mellon University, February 1995.
[PDF]

Frank Pfenning.
Structural cut elimination.
In D. Kozen, editor, Proceedings of the Tenth Annual Symposium
on Logic in Computer Science, pages 156166, San Diego, California, June
1995. IEEE Computer Society Press.
[PDF]

Frank Pfenning and HaoChi Wong.
On a modal lambdacalculus 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]

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 136147, Orlando, Florida, June
1994. INRIA Technical Report 2265.
Available as Technical Report CMUCS94116.

Frank Pfenning.
Elf: A metalanguage for deductive systems.
In A. Bundy, editor, Proceedings of the 12th International
Conference on Automated Deduction, pages 811815, Nancy, France, June 1994.
SpringerVerlag LNAI 814.
System abstract.
[PDF]

Frank Pfenning, editor.
Logic Programming and Automated Reasoning, 5th International
Conference, LPAR'94, Kiev, Ukraine, July 1994. SpringerVerlag LNAI 822.

Frank Pfenning.
Logical frameworks.
Home page and bibliography
on the WorldWide Web, October 1994.

Frank Pfenning.
Structural cut elimination in linear logic.
Technical Report CMUCS94222, Department of Computer Science,
Carnegie Mellon University, December 1994.
[PDF]

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 CarlJohan H. Seger, editors, Proceedings of the 6th International Workshop on Higher Order Logic Theorem
Proving and Its Applications, pages 366370, Vancouver, B.C., Canada,
August 1993. SpringerVerlag LNCS 780.

Michael Kohlhase and Frank Pfenning.
Unification in a lambdacalculus with intersection types.
In Dale Miller, editor, Proceedings of the International Logic
Programming Symposium, pages 488505, Vancouver, Canada, October 1993. MIT
Press.
[PDF]

Spiro Michaylov and Frank Pfenning.
Higherorder logic programming as constraint logic programming.
In Position Papers for the First Workshop on Principles and
Practice of Constraint Programming, pages 221229, Newport, Rhode Island,
April 1993. Brown University.
[PDF]

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 5763, Montreal, Canada, June 1993.
[PDF]

Frank Pfenning.
On the undecidability of partial polymorphic type reconstruction.
Fundamenta Informaticae, 19(1,2):185199, 1993.
Preliminary version available as Technical Report CMUCS92105,
School of Computer Science, Carnegie Mellon University, January 1992.
[PDF]

Frank Pfenning.
Refinement types for logical frameworks.
In Herman Geuvers, editor, Informal Proceedings of the Workshop
on Types for Proofs and Programs, pages 285299, Nijmegen, The Netherlands,
May 1993.
[PDF]

Scott Dietzen and Frank Pfenning.
Higherorder and modal logic as a framework for explanationbased
generalization.
Machine Learning, 9:2355, 1992.

John Hannan and Frank Pfenning.
Compiler verification in LF.
In Andre Scedrov, editor, Seventh Annual IEEE Symposium on
Logic in Computer Science, pages 407418, Santa Cruz, California, June
1992.
[PDF]

Spiro Michaylov and Frank Pfenning.
An empirical study of the runtime behavior of higherorder logic
programs.
In D. Miller, editor, Proceedings of the Workshop on the
lambda Prolog Programming Language, pages 257271, Philadelphia,
Pennsylvania, July 1992. University of Pennsylvania.
Available as Technical Report MSCIS9286.
[PDF]

Gopalan Nadathur and Frank Pfenning.
The type system of a higherorder logic programming language.
In Frank Pfenning, editor, Types in Logic Programming, pages
245283. MIT Press, 1992.

Frank Pfenning.
Dependent types in logic programming.
In Frank Pfenning, editor, Types in Logic Programming,
chapter 10, pages 285311. MIT Press, Cambridge, Massachusetts, 1992.

Frank Pfenning, editor.
Types in Logic Programming.
MIT Press, Cambridge, Massachusetts, 1992.

Frank Pfenning and Ekkehard Rohwedder.
Implementing the metatheory of deductive systems.
In D. Kapur, editor, Proceedings of the 11th International
Conference on Automated Deduction, pages 537551, Saratoga Springs, New
York, June 1992. SpringerVerlag LNAI 607.
[PDF]

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 372386. MIT Press, October 1991.
[PDF]

Conal Elliott and Frank Pfenning.
A semifunctional implementation of a higherorder logic programming
language.
In Peter Lee, editor, Topics in Advanced Language
Implementation, pages 289325. 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 268277, Toronto, Ontario, June 1991. ACM Press.
[PDF]

Spiro Michaylov and Frank Pfenning.
Compiling the polymorphic lambdacalculus.
In Paul Hudak and Neil Jones, editors, Proceedings of the
Symposium on Partial Evaluation and Semantics Based Program Manipulation,
pages 285296, 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 metatheory in Elf.
In L.H. Eriksson, L. Hallnäs, and P. SchroederHeister, editors,
Proceedings of the Second International Workshop on Extensions of Logic
Programming, pages 299344, Stockholm, Sweden, January 1991.
SpringerVerlag LNAI 596.
[PDF]

Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov.
Uniform proofs as a foundation for logic programming.
Annals of Pure and Applied Logic, 51:125157, 1991.

Frank Pfenning.
Logic programming in the LF logical framework.
In Gérard Huet and Gordon Plotkin, editors, Logical
Frameworks, pages 149181. Cambridge University Press, 1991.
[PDF]

Frank Pfenning.
Unification and antiunification in the Calculus of
Constructions.
In Sixth Annual IEEE Symposium on Logic in Computer Science,
pages 7485, Amsterdam, The Netherlands, July 1991.
[PDF]

Frank Pfenning and Peter Lee.
Metacircularity in the polymorphic lambdacalculus.
Theoretical Computer Science, 89:137159, 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 641642, Kaiserslautern, Germany, July 1990.
SpringerVerlag LNCS 449.
System abstract.
[PDF]

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. SpringerVerlag LNCS 449.
Abstract.
[PDF]

Robert Harper, Peter Lee, and Frank Pfenning.
Foundations of programming: Aspects of research in Ergo.
In Computer Science Research Review 1988/1989, pages 2937.
School of Computer Science, Carnegie Mellon University, 1990.

Frank Pfenning.
Program development through proof transformation.
Contemporary Mathematics, 106:251262, 1990.
[PDF]

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.
[PDF]

Frank Pfenning and Daniel Nesmith.
Presenting intuitive deductions via symmetric simplification.
In M.E. Stickel, editor, 10th International Conference on
Automated Deduction, pages 336350, Kaiserslautern, Germany, July 1990.
SpringerVerlag LNCS 449.
[PDF]

Scott Dietzen and Frank Pfenning.
Explanationbased learning in logic programming.
Ergo Report 89086, Carnegie Mellon University, November 1989.

Scott Dietzen and Frank Pfenning.
Higherorder and modal logic as a framework for explanationbased
generalization.
In Alberto Maria Segre, editor, Sixth International Workshop on
Machine Learning, pages 447449, San Mateo, California, June 1989. Morgan
Kaufmann Publishers.
Expanded version available as Technical Report CMUCS89160,
Carnegie Mellon University.
[PDF]

Peter Lee, Mark Leone, Spiro Michaylov, and Frank Pfenning.
Towards a practical programming language based on the polymorphic
lambda calculus.
Ergo Report 89085, School of Computer Science, Carnegie Mellon
University, November 1989.
[PDF]

Frank Pfenning.
Elf: A language for logic definition and verified metaprogramming.
In Fourth Annual Symposium on Logic in Computer Science, pages
313322, Pacific Grove, California, June 1989. IEEE Computer Society Press.
[PDF]

Frank Pfenning.
Review of ``Jean H. Gallier: Logic for Computer Science, Harper
& Row, New York 1986''.
Journal of Symbolic Logic, 54(1):288289, 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 345359, Barcelona, Spain,
March 1989. SpringerVerlag LNCS 352.
[PDF]

Frank Pfenning and Christine PaulinMohring.
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
209228. SpringerVerlag LNCS 442, March 1989.
[PDF]

Peter Lee, Frank Pfenning, John Reynolds, Gene Rollins, and Dana Scott.
Research on semantically based programdesign environments: The Ergo
Project in 1988.
Technical Report CMUCS88118, Carnegie Mellon University, March
1988.
[PDF]

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 2534. ACM Press, November 1988.
[PDF]

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 110120. ACM Press, November 1988.
[PDF]

Frank Pfenning.
Partial polymorphic type inference and higherorder unification.
In Proceedings of the 1988 ACM Conference on Lisp and
Functional Programming, pages 153163, Snowbird, Utah, July 1988. ACM
Press.
[PDF]

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 710713, Argonne,
Illinois, May 1988. SpringerVerlag LNCS 310.
Problem set.
[PDF]

Frank Pfenning and Conal Elliott.
Higherorder abstract syntax.
In Proceedings of the ACM SIGPLAN '88 Symposium on Language
Design and Implementation, pages 199208, Atlanta, Georgia, June 1988.
[PDF]

Conal Elliott and Frank Pfenning.
A family of program derivations for higherorder unification.
Ergo Report 87045, Carnegie Mellon University, November 1987.
[PDF]

Frank Pfenning.
Proof Transformations in HigherOrder Logic.
PhD thesis, Carnegie Mellon University, January 1987.
[PDF]

Peter B. Andrews, Dale Miller, Eve Cohen, and Frank Pfenning.
Automating higherorder logic.
Contemporary Mathematics, 29:169192, August 1984.
[PDF]

Frank Pfenning.
Analytic and nonanalytic proofs.
In R.E. Shostak, editor, Proceedings of the 7th Conference on
Automated Deduction, pages 394413, Napa, California, May 1984.
SpringerVerlag LNCS 170.
[PDF]
[ Home
 Contact
 Research
 Publications
 CV
 Students
]
[ Projects
 Courses
 Conferences
 Organizations
 Journals
]
[ Logical Frameworks
 Pittsburgh Squash Racquets Assocation
]
http://www.cs.cmu.edu/~fp
