<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
@InProceedings{Abel01ptp,
  author = 	 "Andreas Abel and Bor-Yuh Evan Chang and Frank Pfenning",
  title = 	 "Human-Readable, Machine-Verifiable Proofs for Teaching
		  Constructive Logic",
  booktitle =	 "Proceedings of the Workshop on Proof Transformations, Proof
		  Presentations and Complexity of Proofs (PTP'01)",
  year =	 2001,
  address =	 "Siena, Italy",
  month =	 jun,
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/ptp01.pdf",
}

@InProceedings{Anderson04tphols,
  author = 	 {Penny Anderson and Frank Pfenning},
  title = 	 {Verifying Uniqueness in a Logical Framework},
  booktitle = 	 {Proceedings of the 17th International Conference on
                  Theorem Proving in Higher Order Logics (TPHOLs'04)},
  pages =	 {18--33},
  year =	 2004,
  editor =	 {K.Slind and A.Bunker and G.Gopalakrishnan},
  address =	 {Park City, Utah},
  month =	 sep,
  publisher =	 {Springer LNCS 3223},
  keywords =     {LF, Elf},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/tphols04.pdf},
}

@Article{Andrews04jar,
  author = 	 {Peter B. Andrews and Matthew Bishop and Chad E. Brown and
                  Sunil Issar and Frank Pfenning and Hongwei Xi},
  title = 	 {{ETPS}: A System to Help Students Write Formal Proofs},
  journal = 	 {Journal of Automated Reasoning},
  volume =       32,
  number =       1,
  pages =        {75--92},
  year = 	 2004,
  url =          {http://journals.kluweronline.com/article.asp?PIPS=5264938}
}

@Article{Andrews84,
  author =	"Peter B. Andrews and Dale Miller and Eve Cohen and Frank
		  Pfenning",
  title =	"Automating Higher-Order Logic",
  journal =	"Contemporary Mathematics",
  volume =	29,
  month =	aug,
  year =	1984,
  pages =	"169--192",
  urlpdf =      "http://www.cs.cmu.edu/~fp/papers/conm84.pdf",
  keywords =	"TPS, atp"
}

@InProceedings{Andrews90,
  author =	"Peter B. Andrews and Sunil Issar and Dan Nesmith and Frank
		  Pfenning",
  title =	"The {TPS} Theorem Proving System",
  booktitle =	"10th International Conference on Automated Deduction",
  address =	"Kaiserslautern, Germany",
  editor =	"M.E. Stickel",
  publisher =	"Springer-Verlag LNCS 449",
  month =	jul,
  year =	1990,
  pages =	"641--642",
  note =	"System abstract",
  keywords =	"TPS, atp",
  urlpdf =      "http://www.cs.cmu.edu/~fp/papers/cade90tps.pdf"
}

@InProceedings{Andrews94,
  author =	"Peter B. Andrews and Matthew Bishop and Sunil Issar and Dan
		  Nesmith and Frank Pfenning and Hongwei Xi",
  title =	"{TPS}: An Interactive and Automatic Tool for Proving Theorems
		  of Type Theory",
  booktitle =	"Proceedings of the 6th International Workshop on Higher Order
		  Logic Theorem Proving and Its Applications",
  address =	"Vancouver, B.C., Canada",
  editor =	"Jeffrey J. Joyce and Carl-Johan H. Seger",
  publisher =	"Springer-Verlag LNCS 780",
  month =	aug,
  year =	1993,
  pages =	"366--370",
  keywords =	"TPS, atp"
}

@Article{Andrews96,
  author = 	 "Peter B. Andrews and Matthew Bishop and Sunil Issar and Dan
		  Nesmith and Frank Pfenning and Hongwei Xi",
  title = 	 "{TPS}: A Theorem Proving System for Classical Type Theory",
  journal =	 "Journal of Automated Reasoning",
  volume =       16,
  number =       3,
  month =        jun,
  pages =        "321--353",
  year =	 "1996",
  keywords =     "TPS, atp"
}

@InCollection{Bauer07isr,
  author = 	 {Lujo Bauer and Frank Pfenning and Michael K. Reiter},
  title = 	 {Distributed System Security via Logical Frameworks},
  booktitle = 	 {Information Security Research: New Methods for Protecting Against Cyber Threads},
  pages = 	 {108--115},
  publisher =    {Department of Defense, Wiley Publishing},
  year = 	 2007
}

@InProceedings{Berna03ijcai,
  author = 	 {M. Berna and B. Lisien and B. Sellner and G. Gordon and
                  F. Pfenning and and S. Thrun},
  title = 	 {A Learning Algorithm for Localizing People Based on Wireless
                  Signal Strength that Uses Labeled and Unlabeled Data},
  booktitle = 	 {Proceedings of the 18th International Joint Conference on
                  Artificial Intelligence (IJCAI'03)},
  year =	 2003,
  address =	 {Acapulco, Mexico},
  month =	 aug,
  note =	 {Poster},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/ijcai03.pdf}
}

@InProceedings{Bowers07ndss,
  author = 	 {Kevin D. Bowers and Lujo Bauer and Deepak Garg and
                  Frank Pfenning and Michael K. Reiter},
  title = 	 {Consumable Credentials in Logic-Based Access-Control Systems},
  booktitle = 	 {Proceedings of the 14th Annual Network and Distributed
                  System Security Symposium (NDSS'07)},
  pages = 	 {143--157},
  year = 	 2007,
  address = 	 {San Diego, California},
  month = 	 feb,
  publisher =    {Internet Society},
  note = 	 {Preliminary version available as
                  Technical Report CMU-CYLAB-06-002, Carnegie Mellon University, February 2006},
  urlpdf =	 {http://www.cs.cmu.edu/~fp/papers/ndss07.pdf}
}

@InProceedings{Caires10concur,
  author = 	 {Lu{\'\i}s Caires and Frank Pfenning},
  title = 	 {Session Types as Intuitionistic Linear Propositions},
  booktitle = {Proceedings of the 21st International Conference on Concurrency Theory (CONCUR 2010)},
  OPTpages = 	 {},
  year = 	 {2010},
  editor = 	 {P.Gastin and F.Laroussinie},
  address = 	 {Paris, France},
  month = 	 aug,
  publisher = {Springer LNCS},
  note = 	 {To appear},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/sill10.pdf}
}

@Article{Cervesato00tcs,
  author = 	 "Iliano Cervesato and Joshua S. Hodas and Frank Pfenning",
  title = 	 "Efficient Resource Management for Linear Logic Proof Search",
  journal =	 "Theoretical Computer Science",
  year =	 2000,
  volume =       232,
  number =       "1--2",
  month =        feb,
  pages =        "133--163",
  note =	 "Special issue on Proof Search in
		  Type-Theoretic Languages, D. Galmiche and D. Pym, editors",
  keywords =	 "LF, Elf, linear",
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/erm97.pdf",
}

@Article{Cervesato02ic,
  title =        "A Linear Logical Framework",
  author =       "Iliano Cervesato and Frank Pfenning",
  journal =      "Information \& Computation",
  volume =       179,
  number =       1,
  pages =        "19--75",
  year =         2002,
  month =        nov,
  urlpdf =       "http://www.cs.cmu.edu/~fp/papers/llf00.pdf",
  note =         "Revised and expanded version of an extended abstract,
                  LICS 1996, pp. 264-275"
}

@TechReport{Cervesato02tr,
  author = 	 {Iliano Cervesato and Frank Pfenning and David Walker
                  and Kevin Watkins},
  title = 	 {A Concurrent Logical Framework {II}: Examples and Applications},
  institution =  {Department of Computer Science, Carnegie Mellon University},
  year = 	 2002,
  number =	 {CMU-CS-02-102},
  note =	 {Revised May 2003},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/CMU-CS-02-102.pdf}
}

@article{Cervesato03jlc,
  author = 	 {Iliano Cervesato and Frank Pfenning},
  title = 	 {A Linear Spine Calculus},
  journal = 	 {Journal of Logic and Computation},
  year = 	 2003,
  volume =	 13,
  number =	 5,
  pages =	 {639--688}
}

@InProceedings{Cervesato96elp,
  author = 	 "Iliano Cervesato and Joshua S. Hodas and Frank Pfenning",
  title = 	 "Efficient Resource Management for Linear Logic Proof Search",
  editor =	 "R. Dyckhoff and H. Herre and P. Schroeder-Heister",
  booktitle =	 "Proceedings of the 5th International Workshop on Extensions
		  of Logic Programming",
  year =	 1996,
  pages =        "67--81",
  publisher =	 "Springer-Verlag LNAI 1050",
  address =	 "Leipzig, Germany",
  month =	 mar,
  keywords =	 "linear",
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/elp96.pdf",
}

@InProceedings{Cervesato96lics,
  author = 	 "Iliano Cervesato and Frank Pfenning",
  title = 	 "A Linear Logical Framework",
  editor =	 "E. Clarke",
  booktitle =	 "Proceedings of the Eleventh Annual Symposium on Logic in
                  Computer Science",
  year =	 1996,
  publisher =	 "IEEE Computer Society Press",
  address =	 "New Brunswick, New Jersey",
  month =	 jul,
  pages =	 "264--275",
  keywords =	 "LF, Elf, linear",
  urlpdf =       "http://www.cs.cmu.edu/~fp/papers/lics96.pdf",
}

@InProceedings{Cervesato97lics,
  author = 	 "Iliano Cervesato and Frank Pfenning",
  title = 	 "Linear Higher-Order Pre-Unification",
  editor =	 "Glynn Winskel",
  booktitle =	 "Proceedings of the Twelfth Annual Sumposium on Logic
                  in Computer Science (LICS'97)",
  pages =        "422-433",
  year =	 1997,
  publisher =	 "IEEE Computer Society Press",
  address =	 "Warsaw, Poland",
  month =	 jun,
  keywords =	 "linear, unification, LF, Elf",
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/lics97.pdf",
}

@TechReport{Cervesato97tr,
  author = 	 "Iliano Cervesato and Frank Pfenning",
  title = 	 "A Linear Spine Calculus",
  institution =  "Department of Computer Science, Carnegie Mellon University",
  year = 	 1997,
  number =	 "CMU-CS-97-125",
  month =	 apr,
  keywords =	 "LF, Elf, linear",
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/CMU-CS-97-125.pdf",
}

@InProceedings{Chang02grid,
  author = 	 {Bor-Yuh Evan Chang and Karl Crary and Margaret DeLap and Robert Harper and Jason Liszka and Tom Murphy {VII} and Frank Pfenning},
  title = 	 {Trustless Grid Computing in {ConCert}},
  booktitle = 	 {Proceedings of the 3rd International Workshop on Grid Computing (GRID'02)},
  pages =	 {112--125},
  year =	 2002,
  editor =	 {M. Parashar},
  address =	 {Baltimore, Maryland},
  month =	 nov,
  publisher =	 {Springer-Verlag LNCS 2536},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/grid02.pdf},
}

@TechReport{Chang03tr,
  author = 	 {Boy-Yuh Evan Chang and Kaustuv Chaudhuri and Frank Pfenning},
  title = 	 {A Judgmental Analysis of Linear Logic},
  institution =  {Carnegie Mellon University, Department of Computer Science},
  year = 	 2003,
  number =	 {CMU-CS-03-131R},
  month =	 dec,
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/CMU-CS-03-131R.pdf}
}

@Unpublished{Chaudhuri03un,
  author = 	 {Kaustuv Chaudhuri and Frank Pfenning},
  title = 	 {Resource Management for the Inverse Method in Linear Logic},
  note = 	 {Draft manuscript},
  month =	 jan,
  year =	 2003,
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/rminv03.pdf},
}

@InProceedings{Chaudhuri05cade,
  author = 	 {Kaustuv Chaudhuri and Frank Pfenning},
  title = 	 {A Focusing Inverse Method Prover for First-Order Linear Logic},
  booktitle = 	 {Proceedings of the 20th International Conference on Automated
                  Deduction (CADE-20)},
  pages =	 {69--83},
  year =	 2005,
  editor =	 {R.Nieuwenhuis},
  address =	 {Tallinn, Estonia},
  month =	 jul,
  publisher =	 {Springer Verlag LNCS 3632},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/cade05.pdf},
}

@InProceedings{Chaudhuri05csl,
  author = 	 {Kaustuv Chaudhuri and Frank Pfenning},
  title = 	 {Focusing the Inverse Method for Linear Logic},
  booktitle = 	 {Proceedings of the 14th Annual Conference on Computer Science
                  Logic (CSL'05)},
  pages =	 {200--215},
  year =	 2005,
  editor =	 {L.Ong},
  address =	 {Oxford, England},
  month =	 aug,
  publisher =	 {Springer Verlag LNCS 3634},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/csl05.pdf},
}

@InProceedings{Chaudhuri06ijcar,
  author = 	 {Kaustuv Chaudhuri and Frank Pfenning and Greg Price},
  title = 	 {A Logical Characterization of Forward and Backward Chaining in the Inverse Method},
  booktitle = 	 {Proceedings of the 3rd International Joint Conference on
                  Automated Reasoning (IJCAR'06)},
  pages =	 {97--111},
  year =	 2006,
  editor =	 {U. Furbach and N. Shankar},
  address =	 {Seattle, Washington},
  month =	 aug,
  publisher =	 {Springer LNCS 4130},
  urlpdf =	 {http://www.cs.cmu.edu/~fp/papers/ijcar06.pdf}
}

@Article{Chaudhuri08jar,
  author = 	 {Kaustuv Chaudhuri and Frank Pfenning and Greg Price},
  title = 	 {A Logical Characterization of Forward and Backward Chaining in the Inverse Method},
  journal = 	 {Journal of Automated Reasoning},
  volume =	 40,
  number =	 {2--3},
  pages =	 {133--177},
  year = 	 2008,
  note =	 {Special issue with selected papers from IJCAR 2006},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/fwdbwd07.pdf}
}

@Article{Colby03tcs,
  author = 	 "Christopher Colby and Karl Crary and Robert Harper and
		  Peter Lee and Frank Pfenning",
  title = 	 "Automated Techniques for Provable Safe Mobile Code",
  journal =	 "Theoretical Computer Science",
  year =	 2003,
  volume =       290,
  pages =        "1175--1199",
  note =	 "Special issue on {\em 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.",
  keywords =	 "LF, Elf",
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/tcs00.pdf",
}

@Misc{Crary01nsf,
  author =	 {Karl Crary and Robert Harper and Peter Lee and Frank Pfenning},
  title =	 {Modules Matter Most},
  howpublished = {Position paper presented at the {\em {NSF} Workshop on New Visions for Software Design and Productivity}},
  month =	 dec,
  year =	 2001,
  note =	 {Nashville, Tennessee},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/mmm01.pdf},
}

@Article{Crary05jfp,
  author = 	 {Karl Crary and Aleksey Kliger and Frank Pfenning},
  title = 	 {A Monadic Analysis of Information Flow Security with
                  Mutable State},
  journal = 	 {Journal of Functional Programming},
  year = 	 2005,
  volume =	 15,
  number =	 2,
  pages =	 {249--291},
  month =	 mar,
  note =	 {Preliminary version available as Technical Report CMU-CS-03-164},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/jfp04.pdf},
}

@TechReport{Danvy95,
  author = 	 "Olivier Danvy and Frank Pfenning",
  title = 	 "The Occurrence of Continuation Parameters in {CPS} Terms",
  institution =  "Department of Computer Science, Carnegie Mellon University",
  year = 	 1995,
  number =	 "CMU-CS-95-121",
  month =	 feb,
  keywords =     "LF, Elf",
  urlpdf =       "http://www.cs.cmu.edu/~fp/papers/cpsocc95.pdf"
}

@InProceedings{Danvy99hoots,
  author = 	 "Olivier Danvy and Belmina Dzafic and Frank Pfenning",
  title = 	 "On Proving Syntactic Properties of {CPS} Programs",
  editor =	 "Andrew Gordon and Andrew Pitts",
  booktitle =	 "Proceedings of the Third International Workshop on Higher
		  Order Operational Techniques in Semantics (HOOTS'99)",
  year =	 1999,
  address =	 "Paris",
  month =	 sep,
  note =	 "Electronic Notes in Theoretical Computer
		  Science, Volume 26",
  keywords =     "fp",
  url =          "http://www.elsevier.nl/locate/entcs/volume26.html",
  urlpdf =       "http://www.cs.cmu.edu/~fp/papers/hoots99.pdf",
}

@InProceedings{Davies00icfp,
  author = 	 "Rowan Davies and Frank Pfenning",
  title = 	 "Intersection Types and Computational Effects",
  editor =	 "P. Wadler",
  booktitle =	 "Proceedings of the Fifth International Conference on
		  Functional Programming (ICFP'00)",
  year =	 2000,
  pages =        "198--208",
  publisher =	 "ACM Press",
  address =	 "Montreal, Canada",
  month =	 sep,
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/icfp00.pdf",
}

@Article{Davies01jacm,
  author = 	 "Rowan Davies and Frank Pfenning",
  title = 	 "A Modal Analysis of Staged Computation",
  journal =	 "Journal of the ACM",
  year =	 2001,
  volume =       48,
  number =       3,
  month =        may,
  pages =        "555--604",
  keywords =     "fp, staged",
  urlpdf =       "http://www.cs.cmu.edu/~fp/papers/jacm00.pdf",
}

@InProceedings{Davies96popl,
  author = 	 "Rowan Davies and Frank Pfenning",
  title = 	 "A Modal Analysis of Staged Computation",
  editor =	 "Guy {Steele, Jr.}",
  booktitle =	 "Proceedings of the 23rd Annual Symposium on Principles of
                  Programming Languages",
  year =	 1996,
  publisher =	 "ACM Press",
  address =	 "St. Petersburg Beach, Florida",
  month =	 jan,
  pages =        "258--270",
  annote =	 "Extended version available as Technical Report
		  CMU-CS-95-145, Carnegie Mellon University, May 1995",
  keywords =     "fp, staged",
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/popl96.pdf",
}

@TechReport{DeYoung07tr,
  author = 	 {Henry DeYoung and Deepak Garg and Frank Pfenning},
  title = 	 {An Authorization Logic with Explicit Time},
  institution =  {Carnegie Mellon University, Department of Computer Science},
  year = 	 2007,
  number =	 {CMU-CS-07-166},
  month =	 dec,
  note =	 {Revised February 2008},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/CMU-CS-07-166}
}

@InProceedings{DeYoung09fcs,
  author = 	 {Henry DeYoung and Frank Pfenning},
  title = 	 {Reasoning about the Consequences of Authorization Policies in a Linear Epistemic Logic},
  booktitle = {Workshop on Foundations of Computer Security (FCS'09)},
  year = 	 2009,
  address = 	 {Los Angeles, California},
  month = 	 aug,
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/fcs09.pdf}
}

@InProceedings{Despeyroux97,
  author = 	 "Jo{\"e}lle Despeyroux and Frank Pfenning and Carsten
                  Sch{\"u}rmann",
  title = 	 "Primitive Recursion for Higher-Order Abstract Syntax",
  editor =	 "R. Hindley",
  pages =	 "147--163",
  booktitle =	 "Proceedings of the Third International Conference on
                  Typed Lambda Calculus and Applications (TLCA'97)",
  year =	 1997,
  publisher =	 "Springer-Verlag LNCS 1210",
  address =	 "Nancy, France",
  month =	 apr,
  keywords =	 "misc",
  note =	 "An extended version is available as Technical Report
                  CMU-CS-96-172, Carnegie Mellon University",
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/tlca97.pdf",
}

@InProceedings{Deyoung08csf,
  author = 	 {Henry DeYoung and Deepak Garg and Frank Pfenning},
  title = 	 {An Authorization Logic with Explicit Time},
  booktitle = {Proceedings of the 21st Computer Security Foundations
                  Symposium (CSF-21)},
  pages = 	 {133--145},
  year = 	 2008,
  address = 	 {Pittsburgh, Pennsylvania},
  month = 	 jun,
  publisher = {IEEE Computer Society Press},
  note =	 {Extended version available as Technical Report CMU-CS-07-166, revised February 2008},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/csf08.pdf}
}

@InProceedings{Dietzen89ml,
  author =	"Scott Dietzen and Frank Pfenning",
  title =	"Higher-Order and Modal Logic as a Framework for
		 Explanation-Based Generalization",
  booktitle =	"Sixth International Workshop on Machine Learning",
  note =	"Expanded version available as Technical Report
		 CMU-CS-89-160, Carnegie Mellon University",
  month =	jun,
  year =	1989,
  publisher =	"Morgan Kaufmann Publishers",
  editor =	"Alberto Maria Segre",
  address =	"San Mateo, California",
  pages =	"447--449",
  keywords =	"lambda-Prolog, lp",
  urlpdf =      "http://www.cs.cmu.edu/~fp/www/ml89.pdf"
}

@TechReport{Dietzen89tr,
  author =	"Scott Dietzen and Frank Pfenning",
  title =	"Explanation-Based Learning in Logic Programming",
  institution =	"Carnegie Mellon University",
  type =	"Ergo Report",
  number =	"89--086",
  month =	nov,
  year =	"1989",
  keywords =	"lambda-Prolog, lp" 
}

@InProceedings{Dietzen91ilps,
  author =	"Scott Dietzen and Frank Pfenning",
  title =	"A Declarative Alternative to {assert} in Logic Programming",
  booktitle =	"International Logic Programming Symposium",
  publisher =	"MIT Press",
  editor =	"Vijay Saraswat and Kazunori Ueda",
  pages =	"372--386",
  month =	oct,
  year =	"1991",
  keywords = 	"lambda-Prolog",
  urlpdf =      "http://www.cs.cmu.edu/~fp/papers/ilps91.pdf",
}

@Article{Dietzen92,
  author =	"Scott Dietzen and Frank Pfenning",
  title =	"Higher-Order and Modal Logic as a Framework for
		  Explanation-Based Generalization",
  journal =	"Machine Learning",
  year =	"1992",
  volume =	"9",
  pages =	"23--55",
  keywords = 	"lambda-Prolog"
}

@InProceedings{Dowek96jicslp,
  author = 	 "Gilles Dowek and Th{\'e}r{\`e}se Hardin and Claude Kirchner
                  and Frank Pfenning",
  title = 	 "Unification via Explicit Substitutions: The Case of
                  Higher-Order Patterns",
  booktitle = 	 "Proceedings of the Joint International Conference and
                  Symposium on Logic Programming",
  editor = 	 "M. Maher",
  year = 	 "1996",
  publisher =    "MIT Press",
  address = 	 "Bonn, Germany",
  month = 	 sep,
  pages =        "259--273",
  notes =        "Extended version available as Rapport de Recherche No.~3591,
		  INRIA, December 1998",
  keywords =     "unification",
  urlpdf = 	 "http://www.cs.cmu.edu/~fp/papers/jicslp96.pdf",
}

@TechReport{Dowek98tr,
  author = 	 {Gilles Dowek and Th{\'e}r{\`e}se Hardin and Claude Kirchner
                  and Frank Pfenning},
  title = 	 {Unification via Explicit Substitutions: The Case of
                  Higher-Order Patterns},
  institution =  {INRIA},
  year = 	 1998,
  type =	 {Rapport de Recherche},
  number =	 3591,
  month =	 dec,
  note =	 {Preliminary version appeared at JICSLP'96}
}

@InProceedings{Dunfield03fossacs,
  author = 	 {Joshua Dunfield and Frank Pfenning},
  title = 	 {Type Assignment for Intersections and Unions in Call-by-Value Languages},
  booktitle = 	 {Proceedings of the 6th International Conference on
                  Foundations of Software Science and Computation Structures
                  (FOSSACS'03)},
  year =	 2003,
  editor =	 {A.D. Gordon},
  address =	 {Warsaw, Poland},
  month =	 apr,
  pages =        {250--266},
  publisher =    {Springer-Verlag LNCS 2620},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/fossacs03.pdf},
}

@InProceedings{Dunfield04popl,
  author = 	 {Joshua Dunfield and Frank Pfenning},
  title = 	 {Tridirectional Typechecking},
  booktitle = 	 {Conference Record of the 31st Annual Symposium
                  on Principles of Programming Languages (POPL'04)},
  pages =	 {281--292},
  year =	 2004,
  editor =	 {X.Leroy},
  address =	 {Venice, Italy},
  month =	 jan,
  publisher =	 {ACM Press},
  note =         {Extended version available as Technical Report CMU-CS-04-117,
                  March 2004},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/popl04.pdf},
}

@TechReport{Elliott87,
  author =	"Conal Elliott and Frank Pfenning",
  title =	"A Family of Program Derivations for Higher-Order
		 Unification",
  institution =	"Carnegie Mellon University",
  year =	1987,
  number =	"87--045",
  month =	nov,
  type =	"Ergo Report",
  keywords =	"Ergo",
  urlpdf =      "http://www.cs.cmu.edu/~fp/papers/hou87.pdf"
}

@InCollection{Elliott91,
  author =	"Conal Elliott and Frank Pfenning",
  title =	"A Semi-Functional Implementation of a Higher-Order Logic
		  Programming Language",
  booktitle =	"Topics in Advanced Language Implementation",
  publisher =	"MIT Press",
  year =	"1991",
  pages =	"289--325",
  editor =	"Peter Lee",
  url =  	"http://www.cs.cmu.edu/~fp/papers/elpsml-paper.tar.gz",
  keywords = 	"lambda-Prolog, LF, Elf"
}

@InProceedings{Felty90tutorial,
  author =	"Amy Felty and Elsa Gunter and Dale Miller and
	         Frank Pfenning",
  title =	"Tutorial on {$\lambda$Prolog}",
  booktitle =	"Proceedings of the 10th International Conference on Automated
	         Deduction",
  address =	"Kaiserslautern, Germany",
  editor =	"M.E. Stickel",
  publisher =	"Springer-Verlag LNCS 449",
  month =	jul,
  year =	1990,
  pages =	682,
  note =	"Abstract",
  keywords =	"lambda-Prolog, lp",
  urlpdf =      "http://www.cs.cmu.edu/~fp/papers/cade90lp.pdf"
}

@InProceedings{Freeman91,
  author =	"Tim Freeman and Frank Pfenning",
  title =	"Refinement Types for {ML}",
  booktitle =	"Proceedings of the {SIGPLAN '91} Symposium on Language Design
		  and Implementation",
  address =	"Toronto, Ontario",
  publisher =	"ACM Press",
  month =	jun,
  year =	1991,
  pages =	"268--277",
  urlpdf =      "http://www.cs.cmu.edu/~fp/papers/pldi91.pdf",
  keywords =	"ML, fp"
}

@Proceedings{Gabrielli00ppdp,
  title = 	 "Proceedings of the International Conference on Principles
		  and Practice of Declarative Programming (PPDP'00)",
  year = 	 2000,
  editor =	 "Maurizio Gabrielli and Frank Pfenning",
  publisher =	 "ACM Press",
  address =	 "Ottawa, Canada",
  month =	 sep,
  keywords =     "misc"
}

@InProceedings{Garg05concur,
  author = 	 {Deepak Garg and Frank Pfenning},
  title = 	 {Type-Directed Concurrency},
  booktitle = 	 {Proceedings of the 16th International Conference on Concurrency Theory (CONCUR'05)},
  pages =	 {6--20},
  year =	 2005,
  editor =	 {M.Abadi and L.de Alfaro},
  address =	 {San Francisco, California},
  month =	 aug,
  publisher =	 {Springer Verlag LNCS 3653},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/concur05.pdf},
}

@InProceedings{Garg06csfw,
  author = 	 {Deepak Garg and Frank Pfenning},
  title = 	 {Non-Interference in Constructive Authorization Logic},
  booktitle = 	 {Proceedings of the 19th Computer Security Foundations
                  Workshop (CSFW'06)},
  pages =	 {283--293},
  year = 	 2006,
  editor =	 {J. Guttman},
  address = 	 {Venice, Italy},
  month = 	 jul,
  publisher =	 {IEEE Computer Society Press},
  urlpdf =	 {http://www.cs.cmu.edu/~fp/papers/csfw06.pdf}
}

@InProceedings{Garg06esorics,
  author = 	 {Deepak Garg and Lujo Bauer and Kevin Bowers and Frank Pfenning and Michael Reiter},
  title = 	 {A Linear Logic of Affirmation and Knowledge},
  booktitle = 	 {Proceedings of the 11th European Symposium on Research in Computer Security (ESORICS'06)},
  year = 	 2006,
  editor = 	 {D. Gollman and J. Meier and A. Sabelfeld},
  pages =	 {297--312},
  address = 	 {Hamburg, Germany},
  month = 	 sep,
  publisher =	 {Springer LNCS 4189},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/esorics06.pdf}
}

@TechReport{Garg09trpolicy,
  author = 	 {Deepak Garg and Frank Pfenning and Denis Serenyi and Brian Witten},
  title = 	 {A Logical Representation of Common Rule for Controlling Access to Classified Information},
  institution =  {Carnegie Mellon University},
  year = 	 2009,
  number = 	 {CMU-CS-09-139},
  month = 	 jun,
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/CMU-CS-09-139.pdf}
}

@InProceedings{Garg10oakland,
  author = 	 {Deepak Garg and Frank Pfenning},
  title = 	 {A Proof-Carrying File System},
  booktitle = {Proceedings of the 31st Symposium on Security and Privacy (Oakland 2010)},
  pages =        {},
  year = 	 2010,
  editor = 	 {D.Evans and G.Vigna},
  address = 	 {Berkeley, California},
  month = 	 may,
  organization = {IEEE},
  note = 	 {Extended version available as Technical Report CMU-CS-09-123, June 2009},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/oakland10.pdf}
}

@InProceedings{Hannan92lics,
  author =	"John Hannan and Frank Pfenning",
  title =	"Compiler Verification in {LF}",
  booktitle =	"Seventh Annual {IEEE} Symposium on Logic in Computer Science",
  address =	"Santa Cruz, California",
  month =	jun,
  year =	"1992",
  editor =	"Andre Scedrov",
  pages =	"407--418",
  urlpdf =	"http://www.cs.cmu.edu/~fp/papers/lics92.pdf",
  keywords = 	"LF, Elf"
}

@Article{Harper05tocl,
  author = 	 {Robert Harper and Frank Pfenning},
  title = 	 {On Equivalence and Canonical Forms in the {LF} Type Theory},
  journal = 	 {Transactions on Computational Logic},
  year = 	 2005,
  month =        jan,
  volume =       6,
  issue =        1,
  pages =        {61--101},
  keywords =     {LF, Elf},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/tocl05.pdf},
}

@InCollection{Harper90tr,
  author =	"Robert Harper and Peter Lee and Frank Pfenning",
  title =	"Foundations of Programming: Aspects of Research in
		 {Ergo}",
  booktitle =	"Computer Science Research Review 1988/1989",
  publisher =	"School of Computer Science, Carnegie Mellon
		 University",
  year =	1990,
  pages =	"29--37",
  keywords =	"Ergo"
}

@InProceedings{Harper94ml,
  author =	"Robert Harper and Peter Lee and Frank Pfenning and Eugene
		  Rollins",
  title =	"A Compilation Manager for {Standard} {ML} of {New} {Jersey}",
  booktitle =	"Record of the 1994 {ACM SIGPLAN} Workshop on {ML} and it
		  Applications",
  editor =	"Didier R\'{e}my",
  publisher =	"INRIA Technical Report 2265",
  address =	"Orlando, Florida",
  month =	jun,
  year =	1994,
  pages =	"136--147",
  note =	"Available as Technical Report CMU-CS-94-116",
  keywords =	"ML, fp"
}

@Article{Harper98jlc,
  author = 	 "Robert Harper and Frank Pfenning",
  title = 	 "A Module System for a Programming Language Based on
		  the {LF} Logical Framework",
  journal =	 "Journal of Logic and Computation",
  year =	 1998,
  volume =	 8,
  number =	 1,
  pages =	 "5--31",
  keywords =	 "LF, Elf"
}

@TechReport{Harper98tr,
  author = 	 "Robert Harper and Peter Lee and Frank Pfenning",
  title = 	 "The {Fox} Project: Advanced Language Technology for
		  Extensible Systems",
  institution =  "Department of Computer Science, Carnegie Mellon University",
  year = 	 1998,
  number =	 "CMU-CS-98-107",
  month =	 jan,
  keywords =     "Fox",
  urlpdf =       "http://www.cs.cmu.edu/~fp/papers/CMU-CS-98-107.pdf",
}

@InProceedings{Kohlhase93,
  author =	"Michael Kohlhase and Frank Pfenning",
  title =	"Unification in a {$\lambda$}-Calculus with Intersection
		  Types",
  booktitle =	"Proceedings of the International Logic Programming Symposium",
  editor =	"Dale Miller",
  publisher =	"MIT Press",
  address =	"Vancouver, Canada",
  month =	oct,
  year =	"1993",
  pages =	"488--505",
  urlpdf =	"http://www.cs.cmu.edu/~fp/papers/ilps93.pdf",
  keywords = 	"unification, LF, Elf"
}

@InProceedings{Lee88sde,
  author =	"Peter Lee and Frank Pfenning and Gene Rollins and
		 William Scherlis",
  title =	"The {Ergo Support System}: An Integrated Set of
		 Tools for Prototyping Integrated Environments",
  booktitle =	"Proceedings of the {ACM SIGSOFT/SIGPLAN} Software
		 Engineering Symposium on Practical Software Development
		 Environments",
  publisher =	"ACM Press",
  year =	1988,
  editor =	"Peter Henderson",
  month =	nov,
  pages =	"25--34",
  keywords =	"Ergo",
  urlpdf =      "http://www.cs.cmu.edu/~fp/papers/sde88a.pdf"
}

@TechReport{Lee88tr,
  author =	"Peter Lee and Frank Pfenning and John Reynolds and
		 Gene Rollins and Dana Scott",
  title =	"Research on Semantically Based Program-Design
		 Environments: The {Ergo Project} in 1988",
  institution =	"Carnegie Mellon University",
  type =	"Technical Report",
  number =	"CMU-CS-88-118",
  month =	mar,
  year =	1988,
  keywords =	"Ergo",
  urlpdf =      "http://www.cs.cmu.edu/~fp/papers/CMU-CS-88-118.pdf"
}

@TechReport{Lee89tr,
  author =	"Peter Lee and Mark Leone and Spiro Michaylov and
		 Frank Pfenning",
  title =	"Towards a Practical Programming Language Based on
		 the Polymorphic Lambda Calculus",
  institution =	"School of Computer Science, Carnegie Mellon
		 University",
  type =	"Ergo Report",
  number =	"89--085",
  month =	nov,
  year =	1989,
  keywords =	"fp",
  urlpdf =      "http://www.cs.cmu.edu/~fp/papers/poly89.pdf"
}

@TechReport{LeyWild07tr,
  author = 	 {Ruy Ley-Wild and Frank Pfenning},
  title = 	 {Avoiding Causal Dependencies via Proof Irrelevance in a
                  Concurrent Logical Framework},
  institution =  {Carnegie Mellon University},
  year = 	 2007,
  number =	 {CMU-CS-07-107},
  month =	 feb,
  note =	 {In preparation},
  urlpdf =	 {http://www.cs.cmu.edu/~fp/papers/CMU-CS-07-107.pdf}
}

@InProceedings{Lopez05ppdp,
  author = 	 {Pablo L{\'o}pez and Frank Pfenning and Jeff Polakow and Kevin Watkins},
  title = 	 {Monadic Concurrent Linear Logic Programming},
  booktitle = 	 {Proceedings of the 7th International Symposium on Principles and Practice of
                  Declarative Programming (PPDP'05)},
  pages =	 {35--46},
  year =	 2005,
  editor =	 {A.Felty},
  address =	 {Lisbon, Portugal},
  month =	 jul,
  publisher =	 {ACM Press},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/ppdp05.pdf},
}

@InProceedings{Lovas07lfmtp,
  author = 	 {William Lovas and Frank Pfenning},
  title = 	 {A Bidirectional Refinement Type System for {LF}},
  booktitle = 	 {Proceedings of the Second International Workshop on
                  Logical Frameworks and Meta-Languages: Theory and Practice},
  pages =	 {113--128},
  year =	 2007,
  editor =	 {B. Pientka and C. Sch{\"u}rmann},
  address =	 {Bremen, Germany},
  month =	 jul,
  publisher =    {Electronic Notes in Theoretical Computer Science (ENTCS), vol 196},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/lfmtp07.pdf}
}

@InProceedings{Lovas09tlca,
  author = 	 {William Lovas and Frank Pfenning},
  title = 	 {Refinement Types as Proof Irrelevance},
  booktitle =    {Proceedings of the 9th International Conference on Typed Lambda Calculi and Applications (TLCA 2009)},
  pages = 	 {157--171},
  year = 	 2009,
  editor = 	 {P.-L. Curien},
  address = 	 {Brasilia, Brazil},
  month = 	 jul,
  publisher = {Springer LNCS 5608},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/tlca09.pdf}
}

@Article{Lovas10lmcs,
  author = 	 {William Lovas and Frank Pfenning},
  title = 	 {Refinement Types for Logical Frameworks and Their Interpretation
                  as Proof Irrelevance},
  journal = 	 {Logical Methods in Computer Science},
  year = 	 {2010},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTpages = 	 {},
  month = 	 may,
  note = 	 {To appear},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/lmcs10.pdf}
}

@InProceedings{McLaughlin08lpar,
  author = 	 {Sean McLaughlin and Frank Pfenning},
  title = 	 {Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic},
  booktitle = 	 {Proceedings of the 15th International Conference on Logic for
                  Programming, Artificial Intelligence, and Reasoning (LPAR'08)},
  pages =	 {174--181},
  year =	 2008,
  editor =	 {I.Cervesato and H.Veith and A.Voronkov},
  address =	 {Doha, Qatar},
  month =	 nov,
  publisher =	 {Springer LNCS 5330},
  note =	 {System Description},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/lpar08.pdf}
}

@InProceedings{McLaughlin09cade,
  author = 	 {Sean McLaughlin and Frank Pfenning},
  title = 	 {Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method},
  booktitle = {Proceedings of the 22nd International Conference on Automated Deduction (CADE-22))},
  pages = 	 {230--244},
  year = 	 2009,
  editor = 	 {R.A.Schmidt},
  address = 	 {Montreal, Canada},
  month = 	 aug,
  publisher = {Springer LNCS 5663},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/cade09.pdf}
}

@InProceedings{Michaylov91,
  author =	"Spiro Michaylov and Frank Pfenning",
  title =	"Natural Semantics and Some of its Meta-Theory in {Elf}",
  booktitle =	"Proceedings of the Second International Workshop on
		  Extensions of Logic Programming",
  editor =	"L.-H. Eriksson and L. Halln{\"a}s and P. Schroeder-Heister",
  publisher =	"Springer-Verlag LNAI 596",
  year =	"1991",
  address =	"Stockholm, Sweden",
  month =	jan,
  pages =	"299--344",
  urlpdf =	"http://www.cs.cmu.edu/~fp/papers/elp91.pdf",
  keywords = 	"LF, Elf"
}

@InProceedings{Michaylov91pepm,
  author =	"Spiro Michaylov and Frank Pfenning",
  title =	"Compiling the Polymorphic {$\lambda$}-Calculus",
  booktitle =	"Proceedings of the Symposium on Partial Evaluation and
		  Semantics Based Program Manipulation",
  address =	"New Haven, Connecticut",
  editor =	"Paul Hudak and Neil Jones",
  publisher =	"ACM Press",
  month =	jun,
  year =	"1991",
  pages =	"285--296",
  note =	"Published in {\em SIGPLAN Notices} 26(9), September 1991",
  keywords =	"fp"
}

@InProceedings{Michaylov92,
  author =	"Spiro Michaylov and Frank Pfenning",
  title =	"An Empirical Study of the Runtime Behavior of Higher-Order
		  Logic Programs",
  booktitle =	"Proceedings of the Workshop on the {$\lambda$Prolog}
		  Programming Language",
  editor =	"D. Miller",
  publisher =	"University of Pennsylvania",
  address =	"Philadelphia, Pennsylvania",
  month =	jul,
  year =	"1992",
  note =	"Available as Technical Report MS-CIS-92-86",
  pages =	"257--271",
  urlpdf =	"http://www.cs.cmu.edu/~fp/papers/lpproc92.pdf",
  keywords = 	"LF, Elf"
}

@InProceedings{Michaylov93,
  author =	"Spiro Michaylov and Frank Pfenning",
  title =	"Higher-Order Logic Programming as Constraint Logic
		  Programming",
  booktitle =	"Position Papers for the First Workshop on Principles and
		  Practice of Constraint Programming",
  publisher =	"Brown University",
  address =	"Newport, Rhode Island",
  month =	apr,
  year =	"1993",
  pages =	"221--229",
  urlpdf =	"http://www.cs.cmu.edu/~fp/papers/ppcp93.pdf",
  keywords = 	"LF, Elf"
}

@Article{Miller91apal,
  author =	"Dale Miller and Gopalan Nadathur and Frank Pfenning and
		  Andre Scedrov",
  title =	"Uniform Proofs as a Foundation for Logic Programming",
  journal =	"Annals of Pure and Applied Logic",
  year =	"1991",
  volume =	"51",
  pages =	"125--157",
  keywords = 	"lambda-Prolog"
}

@Article{Momigliano03tocl,
  author = 	 {Alberto Momigliano and Frank Pfenning},
  title = 	 {Higher-Order Pattern Complement and the Strict Lambda-Calculus},
  journal = 	 {Transactions on Computational Logic},
  volume =       4,
  number =       4,
  year = 	 2003,
  month =	 oct,
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/negpat02.pdf},
}

@InProceedings{Momigliano99iclp,
  author = 	 "Alberto Momigliano and Frank Pfenning",
  title = 	 "The Relative Complement Problem for Higher-Order Patterns",
  editor =	 "D. De Schreye",
  booktitle =	 "Proceedings of the International Conference on Logic
		  Programming (ICLP'99)",
  year =	 1999,
  publisher =	 "MIT Press",
  address =	 "Las Cruces, New Mexico",
  month =	 nov,
  pages =        "380--394",
  keywords =     "lp",
  urlpdf =       "http://www.cs.cmu.edu/~fp/papers/iclp99.pdf",
}

@InProceedings{Murphy04lics,
  author = 	 {Tom Murphy~VII and Karl Crary and Robert Harper and Frank Pfenning},
  title = 	 {A Symmetric Modal Lambda Calculus for Distributed Computing},
  booktitle = 	 {Proceedings of the 19th Annual Symposium on Logic in
                  Computer Science (LICS'04)},
  pages =	 {286--295},
  year =	 2004,
  editor =	 {H. Ganzinger},
  address =	 {Turku, Finland},
  month =	 jul,
  publisher =	 {IEEE Computer Society Press},
  note =         {Extended version available as Technical Report
                  CMU-CS-04-105},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/lics04.pdf},
}

@InCollection{Nadathur92,
  author =	"Gopalan Nadathur and Frank Pfenning",
  title =	"The Type System of a Higher-Order Logic Programming Language",
  pages =	"245--283",
  booktitle =	"Types in Logic Programming",
  editor =	"Frank Pfenning",
  year =	1992,
  publisher =	"MIT Press",
  keywords = 	"lambda-Prolog"
}

@InProceedings{Nanevski03merlin,
  author = 	 {Aleksandar Nanevski and Brigitte Pientka and Frank Pfenning},
  title = 	 {A Modal Foundation for Meta-Variables},
  booktitle = 	 {Proceedings of the Second Workshop on Mechanized Reasoning
                  about Languages with Variable Binding (MERLIN'03)},
  year =	 2003,
  address =	 {Uppsala, Sweden},
  month =	 aug,
  publisher =	 {ACM SIGPLAN}
}

@Article{Nanevski05jfp,
  author = 	 {Aleksandar Nanevski and Frank Pfenning},
  title = 	 {Staged Computation with Names and Necessity},
  journal = 	 {Journal of Functional Programming},
  year = 	 2005,
  volume =	 15,
  number =	 6,
  pages =	 {837--891},
  month =	 nov,
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/jfp05.pdf},
}

@Article{Nanevski08tocl,
  author = 	 {Aleksandar Nanevski and Frank Pfenning and Brigitte Pientka},
  title = 	 {Contextual Modal Type Theory},
  journal = 	 {Transactions on Computational Logic},
  year = 	 2008,
  volume =       9,
  number =       3,
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/tocl07.pdf}
}

@InProceedings{Narendran93,
  author =	"Paliath Narendran and Frank Pfenning and Richard Statman",
  title =	"On the Unification Problem for {Cartesian} Closed
		  Categories", 
  booktitle =	"Eighth Annual {IEEE} Symposium on Logic in Computer Science",
  address =	"Montreal, Canada",
  editor =	"Moshe Vardi",
  month =	jun,
  year =	1993,
  pages =	"57--63",
  urlpdf =      "http://www.cs.cmu.edu/~fp/papers/lics93.pdf",
  keywords =	"fp, atp"
}

@Article{Narendran97,
  author =	"Paliath Narendran and Frank Pfenning and Richard Statman",
  title =	"On the Unification Problem for {Cartesian} Closed
		  Categories", 
  journal =	"Journal of Symbolic Logic",
  volume =        62,
  number =        2,
  year =	"1997",
  pages =       "636--647",
  keywords =	"fp, atp"
}

@InProceedings{Nord88,
  author =	"Robert L. Nord and Frank Pfenning",
  title =	"The {Ergo} Attribute System",
  booktitle =	"Proceedings of the {ACM SIGSOFT/SIGPLAN} Software Engineering
		  Symposium on Practical Software Development Environments",
  publisher =	"ACM Press",
  year =	1988,
  editor =	"Peter Henderson",
  month =	nov,
  pages =	"110--120",
  keywords =	"Ergo",
  urlpdf =      "http://www.cs.cmu.edu/~fp/papers/sde88b.pdf"
}

@InProceedings{Park05popl,
  author = 	 {Sungwoo Park and Frank Pfenning and Sebastian Thrun},
  title = 	 {A Probabilistic Language based upon Sampling Functions},
  booktitle = 	 {Conference Record of the 32nd Symposium on Principles of
                  Programming Languages (POPL'05)},
  pages =	 {171--182},
  year =	 2005,
  editor =	 {M.Abadi},
  address =	 {Long Beach, California},
  month =	 jan,
  publisher =	 {ACM Press},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/popl05.pdf},
}

@Article{Park08toplas,
  author = 	 {Sungwoo Park and Frank Pfenning and Sebastian Thrun},
  title = 	 {A Probabilistic Language based upon Sampling Functions},
  journal = 	 {Transactions on Programming Languages and Systems},
  year = 	 2008,
  volume = 	 31,
  number = 	 1,
  month = 	 dec,
  urlpdf =	 {http://www.cs.cmu.edu/~fp/papers/toplas08.pdf}
}

@InProceedings{Petersen03popl,
  author = 	 {Leaf Petersen and Robert Harper and Karl Crary and
                  Frank Pfenning},
  title = 	 {A Type Theory for Memory Allocation and Data Layout},
  booktitle = 	 {Conference Record of the 30th Annual Symposium on Principles of Programming Languages (POPL'03)},
  year =	 2003,
  pages =        {172--184},
  editor =	 {G. Morrisett},
  address =	 {New Orleans, Louisiana},
  month =	 jan,
  publisher =	 {ACM Press},
  note =         {Extended version available as Technical Report CMU-CS-02-171, December 2002},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/popl03.pdf},
}

@Article{Pfenning00ic,
  author = 	 "Frank Pfenning",
  title = 	 "Structural Cut Elimination {I}.  {I}ntuitionistic and
		  Classical Logic",
  journal =	 "Information and Computation",
  year =	 2000,
  volume =	 157,
  number =	 "1/2",
  pages =	 "84--141",
  month =	 mar,
  urlpdf =	 "http://www.idealibrary.com/links/artid/inco.1999.2832/production/pdf",
  keywords =	 "LF, Elf"
}

@InProceedings{Pfenning00pepm,
  author = 	 "Frank Pfenning",
  title = 	 "On the Logical Foundations of Staged Computation",
  editor =	 "Julia Lawall",
  pages =	 33,
  booktitle =	 "Proceedings of the Workshop on Partial Evaluation and
		  Semantics-Based Program Manipulation (PEPM'00)",
  year =	 2000,
  publisher =	 "ACM Press",
  address =	 "Boston, Massachusetts",
  month =	 jan,
  note =	 "Abstract of invited talk",
  keywords =     "staged, logic",
  url =		 "http://www.cs.cmu.edu/~fp/talks/pepm00-talk.ps"
}

@InProceedings{Pfenning00saig,
  author = 	 "Frank Pfenning",
  title = 	 "Reasoning About Staged Computation",
  editor =	 "W. Taha",
  pages =	 "5--6",
  booktitle =	 "Proceedings of the International Workshop on
		  Semantics, Applications, and Implementation of Program
		  Generation (SAIG 2000)",
  year =	 2000,
  publisher =	 "Springer-Verlag LNCS 1924",
  address =	 "Montreal, Canada",
  month =	 sep,
  note =	 "Abstract of invited talk",
  keywords =	 "staged, logic",
  url =		 "http://www.cs.cmu.edu/~fp/talks/saig00-talk.pdf"
}

@Article{Pfenning01alp,
  author = 	 "Frank Pfenning",
  title = 	 "Logical Frameworks at {CMU}",
  journal =	 "ALP Newsletter",
  year =	 2001,
  volume =	 14,
  number =	 2,
  month =	 may,
  keywords =	 "LF, Elf",
  url =		 "http://www.cwi.nl/projects/alp/newsletter/nav/pfenning.html"
}

@InCollection{Pfenning01handbook,
  author = 	 "Frank Pfenning",
  title = 	 "Logical Frameworks",
  booktitle =	 "Handbook of Automated Reasoning",
  chapter =      17,
  pages =        "1063--1147",
  publisher =	 "Elsevier Science and MIT Press",
  year =	 2001,
  editor =	 "Alan Robinson and Andrei Voronkov",
  keywords =	 "LF, Elf, misc",
  urlpdf =       "http://www.cs.cmu.edu/~fp/papers/handbook01.pdf",
}

@InProceedings{Pfenning01lics,
  author = 	 "Frank Pfenning",
  title = 	 "Intensionality, Extensionality, and Proof Irrelevance in
		  Modal Type Theory",
  editor =	 "J. Halpern",
  booktitle =	 "Proceedings of the 16th Annual Symposium on Logic in
		  Computer Science (LICS'01)",
  pages =        "221--230",
  year =	 2001,
  publisher =	 "IEEE Computer Society Press",
  address =	 "Boston, Massachusetts",
  month =	 jun,
  keywords =	 "LF, Elf",
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/lics01.pdf",
}

@Article{Pfenning01mscs,
  author = 	 "Frank Pfenning and Rowan Davies",
  title = 	 "A Judgmental Reconstruction of Modal Logic",
  journal =	 "Mathematical Structures in Computer Science",
  year =	 2001,
  volume =       11,
  pages =        "511--540",
  note =	 "Notes to an invited talk at the {\em Workshop
		  on Intuitionistic Modal Logics and Applications} (IMLA'99),
		  Trento, Italy, July 1999",
  keywords =	 "staged, logic",
  urlpdf =       "http://www.cs.cmu.edu/~fp/papers/mscs00.pdf",
}

@Proceedings{Pfenning02lfm,
  title = 	 {Proceedings of the 3rd International Workshop on Logical Frameworks and Meta-Languages (LFM'02)},
  year = 	 2002,
  editor =	 {Frank Pfenning},
  volume =	 {70(2)},
  series =	 {Electronic Notes in Theoretical Computer Science},
  address =	 {Copenhagen, Denmark},
  month =	 jul,
  url =          {http://www.elsevier.nl/locate/entcs/volume70.html}
}

@InCollection{Pfenning02mdorf,
  author = 	 {Frank Pfenning},
  title = 	 {Logical Frameworks---A Brief Introduction},
  booktitle = 	 {Proof and System-Reliability},
  pages =	 {137--166},
  publisher =	 {Kluwer Academic Publishers},
  year =	 2002,
  editor =	 {H. Schwichtenberg and R. Steinbr{\"u}ggen},
  volume =	 62,
  series =	 {NATO Science Series {II}},
  note =         {Lecture notes from the Marktoberdorf Summer School, July 2001},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/mdorf01.pdf},
}

@Book{Pfenning03gpce,
  editor =	 {Frank Pfenning and Yannis Smaragdakis},
  title = 	 {Proceedings of the Second International Conference on
                  Generative Programming and Component Engineering},
  publisher = 	 {Springer-Verlag LNCS 2830},
  year = 	 2003,
  address =	 {Erfurt, Germany},
  month =	 sep
}

@InProceedings{Pfenning04aplas,
  author = 	 {Frank Pfenning},
  title = 	 {Substructural Operational Semantics and Linear Destination-Passing Style},
  booktitle = 	 {Proceedings of the 2nd Asian Symposium on Programming Languages and Systems (APLAS'04)},
  pages = 	 196,
  year =	 2004,
  editor =	 {W.-N. Chin},
  address =	 {Taipei, Taiwan},
  month =	 nov,
  publisher =	 {Springer-Verlag LNCS 3302},
  note =         {Abstract of invited talk},
  urlpdf =       {http://www.cs.cmu.edu/~fp/talks/aplas04-abs.pdf},
}

@Article{Pfenning04bsl,
  author = 	 {Frank Pfenning},
  title = 	 {Review of ``{Benjamin C.~Pierce}: {Types and programming languages}, {The MIT Proess}, {Cambridge, Massachusetts}, 2002''},
  journal = 	 {Bulletin of Symbolic Logic},
  year = 	 2004,
  volume =	 10,
  pages =	 {213--214},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/pierce03.pdf},
}

@Book{Pfenning05book,
  author = 	 "Frank Pfenning",
  title = 	 "Computation and Deduction",
  publisher = 	 "Cambridge University Press",
  OPTyear = 	 "",
  note =	 "In preparation.  Draft from April 1997 available
		  electronically",
  keywords =	 "LF, Elf",
  url =	         "http://www.cs.cmu.edu/~twelf/notes/cd.ps"
}

@InProceedings{Pfenning05merlin,
  author = 	 {Frank Pfenning},
  title = 	 {Towards a Type Theory of Contexts},
  booktitle = 	 {Proceedings of the 3rd Workshop on Mechanized Reasoning
                  About Languages with Variable Binding (MERLIN'05)},
  pages =	 1,
  year =	 2005,
  address =	 {Tallinn, Estonia},
  month =	 sep,
  publisher =	 {ACM Press},
  note =	 {Abstract for invited talk}
}

@Proceedings{Pfenning06rta,
  title = 	 {Proceedings of the 17th International Conference on Rewriting Techniques
                  and Applications},
  year = 	 2006,
  editor =	 {Frank Pfenning},
  address =	 {Seattle, Washington},
  month =	 aug,
  publisher =	 {Springer Verlag LNCS 4098}
}

@Proceedings{Pfenning07cade,
  title = 	 {Proceedings of the 21st International Conference on Automated Deduction (CADE-21)},
  year = 	 2007,
  editor =	 {F. Pfenning},
  address =	 {Bremen, Germany},
  month =	 jul,
  publisher =	 {Springer LNCS 4603}
}

@InProceedings{Pfenning07icfp,
  author = 	 {Frank Pfenning},
  title = 	 {Subtyping and Intersection Types Revisited},
  booktitle = 	 {Proceedings of the 12th International Symposium on Functional Programming (ICFP 2007)},
  pages =	 219,
  year =	 2007,
  editor =	 {R. Hinze and N. Ramsey},
  address =	 {Freiburg, Germany},
  month =	 oct,
  publisher =	 {ACM Press},
  note =	 {Abstract of invited talk}
}

@InProceedings{Pfenning07tlca,
  author = 	 {Frank Pfenning},
  title = 	 {On a Logical Foundation for Explicit Substitutions},
  booktitle = 	 {Proceedings of the 8th International Conference on Typed
                  Lambda Calculi and Applications (TLCA 2007)},
  pages =	 1,
  year =	 2007,
  editor =	 {S. Ronchi Della Rocca},
  address =	 {Paris, France},
  month =	 jun,
  publisher =	 {Springer LNCS 4583},
  note =	 {Abstract of TLCA/RTA joint invited talk}
}

@InCollection{Pfenning08andrews,
  author =     {Frank Pfenning},
  booktitle =  {Reasoning in Simple Type Theory: Festschrift in Honor of {P}eter {B.} {A}ndrews on His 70th Birthday},
  title =      {Church and {C}urry: Combining Intrinsic and Extrinsic Typing},
  pages =      {303--338},
  publisher =  {College Publications},
  year =       2008,
  series =     {Studies in Logic 17},
  editor =     {C.Benzm{\"u}ller and C.Brown and J.Siekmann and R.Statman},
  urlpdf =     {http://www.cs.cmu.edu/~fp/papers/andrews08.pdf}
}

@Proceedings{Pfenning08lics,
  title = 	 {Proceedings of the 23rd Annual Symposium on Logic in Computer Science (LICS 2008)},
  year = 	 2008,
  editor =	 {F. Pfenning},
  address =	 {Pittsburgh, Pennsylvania},
  month =	 jun,
  publisher =	 {IEEE Computer Society Press}
}

@InProceedings{Pfenning09lics,
  author = 	 {Frank Pfenning and Robert J. Simmons},
  title = 	 {Substructural Operational Semantics as Ordered Logic Programming},
  booktitle = {Proceedings of the 24th Annual Symposium on Logic in Computer Science (LICS 2009)},
  pages = 	 {101--110},
  year = 	 2009,
  address = 	 {Los Angeles, California},
  month = 	 aug,
  publisher = {IEEE Computer Society Press},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/lics09.pdf}
}

@InProceedings{Pfenning10lam,
  author = 	 {Frank Pfenning},
  title = 	 {Possession as Linear Knowledge},
  booktitle = {Proceedings of the 3rd International Workshop on Logics, Agents, and Mobility (LAM 2010)},
  OPTpages = 	 {},
  year = 	 {2010},
  editor = 	 {B.Farwer},
  address = 	 {Edinburgh, Scotland},
  month = 	 jul,
  note = 	 {Abstract of invited talk.  To appear.}
}

@InProceedings{Pfenning10lfmtp,
  author = 	 {Frank Pfenning},
  title = 	 {The Practice and Promise of Substructural Frameworks},
  booktitle = {Proceedings of 5th International Workshop on Logical Frameworks and Meta-Languages:
                  Theory and Practice (LFMTP 2010)},
  OPTpages = 	 {},
  year = 	 {2010},
  editor = 	 {K.Crary and M.Miculan},
  address = 	 {Edinburgh, Scotland},
  month = 	 jul,
  note = 	 {Abstract of invited talk.  To appear.}
}

@InProceedings{Pfenning84,
  author =	"Frank Pfenning",
  title =	"Analytic and Non-Analytic Proofs",
  booktitle =	"Proceedings of the 7th Conference on Automated Deduction",
  address =	"Napa, California",
  publisher =	"Springer-Verlag LNCS 170",
  editor =	"R.E. Shostak",
  month =	may,
  year =	1984,
  pages =	"394--413",
  keywords =	"TPS, atp",
  urlpdf =      "http://www.cs.cmu.edu/~fp/papers/cade84.pdf"
}

@PhdThesis{Pfenning87,
  author =	"Frank Pfenning",
  title =	"Proof Transformations in Higher-Order Logic",
  school =	"Carnegie Mellon University",
  month =	jan,
  year =	1987,
  keywords =	"TPS, atp, logic",
  urlpdf =      "http://www.cs.cmu.edu/~fp/papers/thesis87.pdf"
}

@InProceedings{Pfenning88cade,
  author =	"Frank Pfenning",
  title =	"Single Axioms in the Implicational Propositional Calculus",
  booktitle =	"Proceedings of the 9th International Conference on Automated
		  Deduction",
  address =	"Argonne, Illinois",
  publisher =	"Springer-Verlag LNCS 310",
  month =	may,
  year =	"1988",
  editor =	"Ewing Lusk and Ross Overbeek",
  pages =	"710--713",
  note =	"Problem set",
  keywords =	"atp",
  urlpdf =      "http://www.cs.cmu.edu/~fp/papers/cade88.pdf"
}

@InProceedings{Pfenning88lfp,
  author =	"Frank Pfenning",
  title =	"Partial Polymorphic Type Inference and Higher-Order
		  Unification",
  booktitle =	"Proceedings of the 1988 {ACM} Conference on {Lisp} and
		  Functional Programming",
  publisher =	"ACM Press",
  month =	jul,
  year =	"1988",
  pages =	"153--163",
  address =	"Snowbird, Utah",
  urlpdf =      "http://www.cs.cmu.edu/~fp/papers/lfp88.pdf",
  keywords = 	"lambda-Prolog, unification"
}

@InProceedings{Pfenning88pldi,
  author =	"Frank Pfenning and Conal Elliott",
  title =	"Higher-Order Abstract Syntax",
  booktitle =	"Proceedings of the {ACM SIGPLAN '88} Symposium on Language
		  Design and Implementation",
  address =	"Atlanta, Georgia",
  month =	jun,
  year =	"1988",
  pages =	"199--208",
  urlpdf =	"http://www.cs.cmu.edu/~fp/papers/pldi88.pdf",
  keywords = 	"lambda-Prolog"
}

@Article{Pfenning89jsl,
  author =	"Frank Pfenning",
  title =	"Review of ``{Jean H.~Gallier}: {Logic for
		 Computer Science}, {Harper \& Row}, {New York} 1986''",
  journal =	"Journal of Symbolic Logic",
  volume =	54,
  number =	1,
  month =	mar,
  year =	1989,
  pages =	"288--289",
  keywords =	"misc" 
}

@InProceedings{Pfenning89lics,
  author =	"Frank Pfenning",
  title =	"{Elf}: A Language for Logic Definition and Verified
		  Meta-Programming",
  booktitle =	"Fourth Annual Symposium on Logic in Computer Science",
  address =	"Pacific Grove, California",
  publisher =	"IEEE Computer Society Press",
  month =	jun,
  year =	"1989",
  pages =	"313--322",
  urlpdf =	"http://www.cs.cmu.edu/~fp/papers/lics89.pdf",
  keywords = 	"LF, Elf"
}

@InProceedings{Pfenning89mfps,
  author =	"Frank Pfenning and Christine Paulin-Mohring",
  title =	"Inductively Defined Types in the {Calculus of Constructions}",
  booktitle =	"Proceedings of the Fifth Conference on the Mathematical
		  Foundations of Programming Semantics, Tulane University, New
		  Orleans, Louisiana",
  publisher =	"Springer-Verlag LNCS 442",
  month =	mar,
  year =	1989,
  editor =	"M. Main and A. Melton and M. Mislove and D. Schmidt",
  pages =	"209--228",
  keywords =	"tt",
  urlpdf =      "http://www.cs.cmu.edu/~fp/papers/mfps89.pdf"
}

@InProceedings{Pfenning89tapsoft,
  author =	"Frank Pfenning and Peter Lee",
  title =	"{LEAP}: A Language with Eval and Polymorphism",
  booktitle =	"Proceedings of the International Joint Conference on Theory
		  and Practice in Software Development",
  address =	"Barcelona, Spain",
  publisher =	"Springer-Verlag LNCS 352",
  month =	mar,
  year =	1989,
  pages =	"345--359",
  keywords =	"fp",
  urlpdf =      "http://www.cs.cmu.edu/~fp/papers/tapsoft89.pdf"
}

@InProceedings{Pfenning90cade,
  author =	"Frank Pfenning and Daniel Nesmith",
  title =	"Presenting Intuitive Deductions via Symmetric
		  Simplification",
  booktitle =	"10th International Conference on Automated Deduction",
  address =	"Kaiserslautern, Germany",
  publisher =	"Springer-Verlag LNCS 449",
  month =	jul,
  year =	1990,
  editor =	"M.E. Stickel",
  pages =	"336--350",
  keywords =	"TPS, atp",
  urlpdf =      "http://www.cs.cmu.edu/~fp/papers/cade90.pdf"
}

@Article{Pfenning90cm,
  author =	"Frank Pfenning",
  title =	"Program Development Through Proof Transformation",
  journal =	"Contemporary Mathematics",
  volume =	106,
  year =	1990,
  pages =	"251--262",
  keywords =	"Ergo, fp",
  urlpdf =      "http://www.cs.cmu.edu/~fp/papers/conm90.pdf"
}

@InProceedings{Pfenning90iclp,
  author =	"Frank Pfenning",
  title =	"Types in Logic Programming",
  booktitle =	"Proceedings of the Seventh International Conference on Logic
		  Programming",
  editor =	"David H.D. Warren and Peter Szeredi",
  publisher =	"MIT Press",
  month =	jun,
  year =	1990,
  note =	"Abstract of advanced tutorial",
  keywords =	"lp",
  urlpdf =      "http://www.cs.cmu.edu/~fp/papers/iclp90.pdf"
}

@InProceedings{Pfenning91lf,
  author =	"Frank Pfenning",
  title =	"Logic Programming in the {LF} Logical Framework",
  booktitle =	"Logical Frameworks",
  editor =	"G\'{e}rard Huet and Gordon Plotkin",
  publisher =	"Cambridge University Press",
  pages =	"149--181",
  year =	"1991",
  urlpdf =	"http://www.cs.cmu.edu/~fp/papers/lfproc91.pdf",
  keywords = 	"LF, Elf"
}

@InProceedings{Pfenning91lics,
  author =	"Frank Pfenning",
  title =	"Unification and Anti-Unification in the {Calculus} of
		  {Constructions}",
  booktitle =	"Sixth Annual {IEEE} Symposium on Logic in Computer Science",
  address =	"Amsterdam, The Netherlands",
  month =	jul,
  year =	"1991",
  pages =	"74--85",
  urlpdf =	"http://www.cs.cmu.edu/~fp/papers/lics91.pdf",
  keywords = 	"LF, Elf, unification"
}

@Article{Pfenning91tcs,
  author =	"Frank Pfenning and Peter Lee",
  title =	"Metacircularity in the Polymorphic {$\lambda$}-Calculus",
  journal =	"Theoretical Computer Science",
  volume =	89,
  year =	1991,
  pages =	"137--159",
  keywords =	"fp"
}

@Book{Pfenning92book,
  editor =	"Frank Pfenning",
  title =	"Types in Logic Programming",
  publisher =	"MIT Press",
  address =	"Cambridge, Massachusetts",
  year =	1992,
  keywords =	"logic programming"
}

@InProceedings{Pfenning92cade,
  author =	"Frank Pfenning and Ekkehard Rohwedder",
  title =	"Implementing the Meta-Theory of Deductive Systems",
  booktitle =	"Proceedings of the 11th International Conference on Automated
		  Deduction",
  address =	"Saratoga Springs, New York",
  editor =	"D. Kapur",
  publisher =	"Springer-Verlag LNAI 607",
  month =	jun,
  year =	"1992",
  pages =	"537--551",
  urlpdf =	"http://www.cs.cmu.edu/~fp/papers/cade92.pdf",
  keywords = 	"LF, Elf"
}

@InCollection{Pfenning92tilp,
  author =	"Frank Pfenning",
  title =	"Dependent Types in Logic Programming",
  booktitle =	"Types in Logic Programming",
  editor =	"Frank Pfenning",
  publisher =	"MIT Press",
  address =	"Cambridge, Massachusetts",
  chapter =	"10",
  pages =	"285--311",
  year =	"1992",
  keywords = 	"LF, Elf"
}

@Article{Pfenning93fi,
  author =	"Frank Pfenning",
  title =	"On the Undecidability of Partial Polymorphic Type
		  Reconstruction",
  journal =	"Fundamenta Informaticae",
  volume =	19,
  number =	"1,2",
  year =	1993,
  pages =	"185--199",
  note =	"Preliminary version available as Technical Report
		  CMU-CS-92-105, School of Computer Science, Carnegie Mellon
		  University, January 1992",
  urlpdf =      "http://www.cs.cmu.edu/~fp/papers/CMU-CS-92-105.pdf",
  keywords =	"fp"
}

@InProceedings{Pfenning93types,
  author =	"Frank Pfenning",
  title =	"Refinement Types for Logical Frameworks",
  booktitle =	"Informal Proceedings of the Workshop on Types for Proofs
		  and Programs",
  editor =	"Herman Geuvers",
  address =	"Nijmegen, The Netherlands",
  month =	may,
  year =	"1993",
  pages =	"285--299",
  urlpdf =	"http://www.cs.cmu.edu/~fp/papers/rlf93.pdf",
  keywords = 	"LF, Elf, lambda-Prolog"
}

@InProceedings{Pfenning94cade,
  author =	"Frank Pfenning",
  title =	"Elf: A Meta-Language for Deductive Systems",
  booktitle =	"Proceedings of the 12th International Conference on Automated
		  Deduction",
  editor =	"A. Bundy",
  publisher =	"Springer-Verlag LNAI 814",
  address =	"Nancy, France",
  month =	jun,
  year =	"1994",
  pages =	"811--815",
  note =	"System abstract",
  urlpdf =	"http://www.cs.cmu.edu/~fp/papers/cade94.pdf",
  keywords = 	"LF, Elf"
}

@Proceedings{Pfenning94lpar,
  title = 	 "Logic Programming and Automated Reasoning, 5th International
		  Conference, LPAR'94",
  year = 	 1994,
  editor =	 "Frank Pfenning",
  publisher =	 "Springer-Verlag LNAI 822",
  address =	 "Kiev, Ukraine",
  month =	 jul,
  keywords =     "lp"
}

@TechReport{Pfenning94trb,
  author = 	 "Frank Pfenning",
  title = 	 "Structural Cut Elimination in Linear Logic",
  institution =  "Department of Computer Science, Carnegie Mellon University",
  year = 	 1994,
  number =	 "CMU-CS-94-222",
  month =	 dec,
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/cutlin94.pdf",
  keywords =	 "LF, Elf, linear"
}

@Misc{Pfenning94www,
  author =	 "Frank Pfenning",
  title =	 "Logical Frameworks",
  howpublished = "\href{http://www.cs.cmu.edu/~fp/lfs.html}{Home page
		  and bibliography} on the World-Wide Web",
  year =	 1994,
  month =	 oct,
  keywords =     "LF, Elf"
}

@InProceedings{Pfenning95lics,
  author = 	 "Frank Pfenning",
  title = 	 "Structural Cut Elimination",
  editor =	 "D. Kozen",
  booktitle =	 "Proceedings of the Tenth Annual Symposium on Logic in
		  Computer Science",
  year =	 1995,
  publisher =	 "IEEE Computer Society Press",
  address =	 "San Diego, California",
  month =	 "June",
  pages =	 "156--166",
  keywords =     "LF, Elf, linear",
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/lics95.pdf",
}

@InProceedings{Pfenning95mfps,
  author = 	 "Frank Pfenning and Hao-Chi Wong",
  title = 	 "On a Modal $\lambda$-Calculus for {S4}",
  booktitle =	 "Proceedings of the Eleventh Conference on 
                  Mathematical Foundations of Programming Semantics",
  editor =       "S. Brookes and M. Main",
  year =	 1995,
  address =	 "New Orleans, Louisiana",
  month =	 mar,
  note =	 "{\em Electronic Notes in Theoretical Computer
		  Science}, Volume 1, Elsevier", 
  keywords =     "misc",
  urlpdf =       "http://www.cs.cmu.edu/~fp/papers/mfps95.pdf",
}

@InProceedings{Pfenning96caap,
  author = 	 "Frank Pfenning",
  title = 	 "The Practice of Logical Frameworks",
  booktitle = 	 "Proceedings of the Colloquium on Trees in Algebra and
		  Programming",
  editor =	 "H{\'e}l{\`e}ne Kirchner",
  year =	 1996,
  publisher =	 "Springer-Verlag LNCS 1059",
  address = 	 "Link{\"o}ping, Sweden",
  month =	 apr,
  pages =	 "119--134",
  note =	 "Invited talk",
  keywords =	 "ALF, Automath, Elf, FS0, Isabelle, lambda-Prolog,
		  LF, linear, misc, Pi, rewriting, unification",
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/caap96.pdf",
}

@InProceedings{Pfenning98cade,
  author = 	 "Frank Pfenning",
  title = 	 "Reasoning About Deductions in Linear Logic",
  editor =	 "Claude Kirchner and H{\'e}l{\`e}ne Kirchner",
  pages =	 "1--2",
  booktitle =	 "Proceedings of the 15th International Conference on
		  Automated Deduction (CADE-15)",
  year =	 1998,
  publisher =	 "Springer-Verlag LNCS 1421",
  address =	 "Lindau, Germany",
  month =	 jul,
  note =         "Abstract for invited talk",
  keywords =	 "LF, Elf, linear",
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/cade98inv.pdf",
}

@Manual{Pfenning98guide,
  title = 	 "Twelf User's Guide",
  author = 	 "Frank Pfenning and Carsten Sch{\"u}rmann",
  edition =	 "1.2",
  year =	 1998,
  month =	 sep,
  keywords =	 "LF, Elf",
  note =	 "Available as Technical Report CMU-CS-98-173, Carnegie
		  Mellon University",
  urlhtml =	 "http://www.cs.cmu.edu/~twelf/guide"
}

@InProceedings{Pfenning98types,
  author = 	 "Frank Pfenning and Carsten Sch{\"u}rmann",
  title = 	 "Algorithms for Equality and Unification in the
		  Presence of Notational Definitions",
  editor =	 "T. Altenkirch and W. Naraschewski and B. Reus",
  booktitle =	 "Types for Proofs and Programs",
  month =        mar,
  year =	 1998,
  pages =        "179--193",
  address =      "Kloster Irsee, Germany",
  publisher =	 "Springer-Verlag LNCS 1657",
  keywords =	 "LF, Elf",
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/types98.pdf",
}

@InProceedings{Pfenning99cade,
  author = 	 "Frank Pfenning and Carsten Sch{\"u}rmann",
  title = 	 "System Description: Twelf --- A Meta-Logical Framework for
		  Deductive Systems",
  editor =	 "H. Ganzinger",
  pages =        "202--206",
  booktitle =	 "Proceedings of the 16th International Conference on
		  Automated Deduction (CADE-16)",
  year =	 1999,
  publisher =	 "Springer-Verlag LNAI 1632",
  address =	 "Trento, Italy",
  month =	 jul,
  keywords =	 "LF, Elf",
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/cade99.pdf",
}

@InProceedings{Pfenning99ppdp,
  author = 	 "Frank Pfenning",
  title = 	 "Logical and Meta-Logical Frameworks",
  editor =	 "G. Nadathur",
  pages =        "206",
  booktitle =	 "Proceedings of the International Conference on Principles
		  and Practice of Declarative Programming (PPDP'99)",
  year =	 1999,
  publisher =	 "Springer-Verlag LNCS 1702",
  address =	 "Paris, France",
  month =	 sep,
  note =	 "Abstract of invited talk.",
  keywords =     "LF, Elf"
}

@InProceedings{Pientka00induct,
  author = 	 "Brigitte Pientka and Frank Pfenning",
  title = 	 "Termination and Reduction Checking in the Logical Framework",
  editor = 	 "Carsten Sch{\"u}rmann",
  booktitle =	 "Workshop on Automation of Proofs by Mathematical Induction",
  year =	 2000,
  address =	 "Pittsburgh, Pennsylvania",
  month =	 jun,
  keywords =	 "LF, Elf, rewriting",
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/induct00.pdf",
}

@InProceedings{Pientka03cade,
  author = 	 {Brigitte Pientka and Frank Pfenning},
  title = 	 {Optimizing Higher-Order Pattern Unification},
  booktitle = 	 {Proceedings of the 19th Conference on Automated Deduction
                  (CADE-19)},
  pages = 	 {473--487},
  year =	 2003,
  editor =	 {F. Baader},
  address =	 {Miami Beach, Florida},
  month =	 jul,
  publisher =	 {Springer-Verlag LNAI 2741},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/optunif03.pdf},
}

@InProceedings{Plesko99,
  author = 	 "Mark Plesko and Frank Pfenning",
  title = 	 "A Formalization of the Proof-Carrying Code Architecture in a
		  Linear Logical Framework",
  editor =	 "A. Pnueli and P. Traverso",
  booktitle =	 "Proceedings of the FLoC Workshop on Run-Time Result
		  Verification",
  year =	 1999,
  address =	 "Trento, Italy",
  month =	 jul,
  keywords =	 "PCC, LF, Elf, linear",
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/pccllf99.pdf",
}

@InProceedings{Polakow00lfm,
  author = 	 "Jeff Polakow and Frank Pfenning",
  title = 	 "Properties of Terms in Continuation-Passing Style in
		  an Ordered Logical Framework",
  editor = 	 "Jo{\"e}lle Despeyroux",
  booktitle =	 "2nd Workshop on Logical Frameworks
		  and Meta-languages (LFM'00)",
  year =	 2000,
  address =	 "Santa Barbara, California",
  month =	 jun,
  note =	 "Proceedings available as INRIA Technical Report",
  keywords =	 "LF, Elf, linear",
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/lfm00.pdf",
}

@TechReport{Polakow98tr,
  author = 	 "Jeff Polakow and Frank Pfenning",
  title = 	 "Ordered Linear Logic Programming",
  institution =  "Department of Computer Science, Carnegie Mellon University",
  year = 	 1998,
  number =	 "CMU-CS-98-183",
  month =	 dec,
  urlpdf =       "http://www.cs.cmu.edu/~fp/papers/CMU-CS-98-183.pdf",
  keywords =	 "LF, Elf, linear"
}

@InProceedings{Polakow99mfps,
  author = 	 "Jeff Polakow and Frank Pfenning",
  title = 	 "Relating Natural Deduction and Sequent Calculus for
		  Intuitionistic Non-Commutative Linear Logic",
  editor =	 "Andre Scedrov and Achim Jung",
  booktitle =	 "Proceedings of the 15th Conference on Mathematical
		  Foundations of Programming Semantics",
  pages =        "449--466",
  year =	 1999,
  address =	 "New Orleans, Louisiana",
  month =	 apr,
  note =	 "Electronic Notes in Theoretical Computer Science, Volume 20",
  keywords =	 "LF, Elf, linear",
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/mfps99.pdf",
}

@InProceedings{Polakow99tlca,
  author = 	 "Jeff Polakow and Frank Pfenning",
  title = 	 "Natural Deduction for Intuitionistic Non-Commutative
		  Linear Logic",
  editor =	 "J.-Y. Girard",
  booktitle =	 "Proceedings of the 4th International Conference on
		  Typed Lambda Calculi and Applications (TLCA'99)",
  year =	 1999,
  publisher =	 "Springer-Verlag LNCS 1581",
  address =	 "L'Aquila, Italy",
  month =	 apr,
  pages =        "295--309",
  keywords =	 "LF, Elf, linear",
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/tlca99.pdf",
}

@InProceedings{Reed07m4m,
  author = 	 {Jason Reed and Frank Pfenning},
  title = 	 {Intuitionistic Letcc via Labelled Deduction},
  booktitle = 	 {Proceedings of the 5th Workshop on Methods for Modalities (M4M5 2007)},
  pages =        {91-111},
  year =	 2007,
  address =	 {Cachan, France},
  month =	 nov,
  note =	 {Electronic Notes in Theoretical Computer Science (ENTCS), vol 213, March 2009},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/m4m07.pdf}
}

@Unpublished{Reed10un,
  author = 	 {Jason C. Reed and Frank Pfenning},
  title = 	 {Focus-Preserving Embeddings of Substructural Logics in Intuitionistic Logic},
  note = 	 {Unpublished Manuscript},
  month = 	 jan,
  year = 	 2010,
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/substruct10.pdf}
}

@InProceedings{Rohwedder96esop,
  author = 	 "Ekkehard Rohwedder and Frank Pfenning",
  title = 	 "Mode and Termination Checking for Higher-Order Logic
                  Programs",
  editor =	 "Hanne Riis Nielson",
  booktitle =	 "Proceedings of the European Symposium on Programming",
  year =	 1996,
  publisher =	 "Springer-Verlag LNCS 1058",
  address = 	 "Link{\"o}ping, Sweden",
  month =	 apr,
  pages =        "296--310",
  keywords =	 "LF, Elf",
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/esop96.pdf",
}

@InProceedings{Saranli07icra,
  author = 	 {Ulu{\c{c}} Saranli and Frank Pfenning},
  title = 	 {Using Constrained Intuitionistic Linear Logic for
                  Hybrid Robotic Planning Problems},
  booktitle = 	 {Proceedings of the International Conference on Robotics
                  and Automation (ICRA'07)},
  pages =	 {3705--3710},
  year = 	 2007,
  address = 	 {Rome Italy},
  month = 	 apr,
  publisher =    {IEEE Computer Society Press},
  urlpdf =	 {http://www.cs.cmu.edu/~fp/papers/icra07.pdf}
}

@Article{Schurmann01tcs,
  author = 	 "Carsten Sch{\"u}rmann and Jo{\"e}lle Despeyroux and
                  Frank Pfenning",
  title = 	 "Primitive Recursion for Higher-Order Abstract Syntax",
  journal = 	 "Theoretical Computer Science",
  year = 	 2001,
  volume =	 266,
  pages =	 "1--57",
  keywords =     "LF, misc"
}

@InProceedings{Schurmann03tphols,
  author = 	 {Carsten Sch{\"u}rmann and Frank Pfenning},
  title = 	 {A Coverage Checking Algorithm for {LF}},
  booktitle = 	 {Proceedings of the 16th International Conference on
                  Theorem Proving in Higher Order Logics (TPHOLs 2003)},
  pages =	 {120--135},
  year =	 2003,
  editor =	 {D. Basin and B. Wolff},
  address =	 {Rome, Italy},
  month =	 sep,
  publisher =	 {Springer-Verlag LNCS 2758},
  keywords =     {LF, Elf},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/tphols03.pdf},
}

@InProceedings{Schurmann98cade,
  author = 	 "Carsten Sch{\"u}rmann and Frank Pfenning",
  title = 	 "Automated Theorem Proving in a Simple Meta-Logic for {LF}",
  editor =	 "Claude Kirchner and H{\'e}l{\`e}ne Kirchner",
  pages =	 "286--300",
  booktitle =	 "Proceedings of the 15th International Conference on
		  Automated Deduction (CADE-15)",
  year =	 1998,
  publisher =	 "Springer-Verlag LNCS 1421",
  address =	 "Lindau, Germany",
  month =	 jul,
  keywords =	 "LF, Elf",
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/cade98m2.pdf",
}

@InProceedings{Simmons08icalp,
  author = 	 {Robert J. Simmons and Frank Pfenning},
  title = 	 {Linear Logical Algorithms},
  booktitle = {Proceedings of the 35th International Colloquium
                  on Automata, Languages and Programming (ICALP'08)},
  pages = 	 {336--345},
  year = 	 2008,
  address = 	 {Reykjavik, Iceland},
  month = 	 jul,
  publisher = {Springer LNCS 5126},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/icalp08.pdf}
}

@InProceedings{Simmons09pepm,
  author = 	 {Robert J. Simmons and Frank Pfenning},
  title = 	 {Linear Logical Approximations},
  booktitle = {Proceedings of the Workshop on Partial Evaluation and
                  Program Manipulation},
  pages = 	 {9--20},
  year = 	 {2009},
  editor = 	 {G. Puebla and G. Vidal},
  address = 	 {Savannah, Georgia},
  month = 	 jan,
  organization = {ACM SIGPLAN},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/pepm09.pdf}
}

@Unpublished{Simmons10un,
  author = 	 {Robert J. Simmons and Frank Pfenning},
  title = 	 {Logical Approximation for Program Analysis},
  note = 	 {Submitted to the Journal on Higher-Order and Symbolic Computation},
  month = 	 Mar,
  year = 	 2010,
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/lapa10.pdf}
}

@TechReport{Watkins02tr,
  author = 	 {Kevin Watkins and Iliano Cervesato and Frank Pfenning
                  and David Walker},
  title = 	 {A Concurrent Logical Framework {I}: Judgments and Properties},
  institution =  {Department of Computer Science, Carnegie Mellon University},
  year = 	 2002,
  number =	 {CMU-CS-02-101},
  note =	 {Revised May 2003},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/CMU-CS-02-101.pdf}
}

@InProceedings{Watkins04lfm,
  author = 	 {Kevin Watkins and Iliano Cervesato and Frank Pfenning and
                  David Walker},
  title = 	 {Specifying Properties of Concurrent Computations in {CLF}},
  booktitle = 	 {Proceedings of the 4th International Workshop on Logical
                  Frameworks and Meta-Languages (LFM'04)},
  year =	 2004,
  editor =	 {C.Sch{\"u}rmann},
  address =	 {Cork, Ireland},
  month =	 jul,
  publisher =    {Electronic Notes in Theoretical Computer Science (ENTCS), vol 199, pp. 133--145, 2008},
  keywords =     {LF, Elf, linear},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/lfm04.pdf},
}

@InCollection{Watkins04types,
  author = 	 {Kevin Watkins and Iliano Cervesato and Frank Pfenning and
                  David Walker},
  title = 	 {A Concurrent Logical Framework: The Propositional Fragment},
  booktitle = 	 {Types for Proofs and Programs},
  pages = 	 {355--377},
  publisher =	 {Springer-Verlag LNCS 3085},
  year =	 2004,
  editor = 	 {S. Berardi and M. Coppo and F. Damiani},
  note =	 {Revised selected papers from the {\em Third International Workshop on Types for Proofs and Programs},
                  Torino, Italy, April 2003.},
  keywords =     {LF, linear},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/types03.pdf},
}

@InProceedings{Wickline98pldi,
  author = 	 "Philip Wickline and Peter Lee and Frank Pfenning",
  title = 	 "Run-time Code Generation and Modal-{ML}",
  editor =	 "Keith D. Cooper",
  pages =	 "224--235",
  booktitle =	 "Proceedings of the Conference on Programming Language
		  Design and Implementation (PLDI'98)",
  year =	 1998,
  publisher =	 "ACM Press",
  address =	 "Montreal, Canada",
  month =	 jun,
  urlpdf =       "http://www.cs.cmu.edu/~fp/papers/pldi98ccam.pdf",
  keywords =     "staged, fp"
}

@Article{Wickline98surveys,
  author = 	 "Philip Wickline and Peter Lee and Frank Pfenning and
		  Rowan Davies",
  title = 	 "Modal Types as Staging Specifications for Run-Time
		  Code Generation",
  journal =	 "ACM Computing Surveys",
  volume =       30,
  number =       "3es",
  month =        sep,
  year =	 1998,
  urlpdf =       "http://www.cs.cmu.edu/~fp/papers/sope98.pdf",
  keywords =     "staged, fp"
}

@InProceedings{Xi98pldi,
  author = 	 "Hongwei Xi and Frank Pfenning",
  title = 	 "Eliminating Array Bound Checking Through Dependent Types",
  editor =	 "Keith D. Cooper",
  pages =	 "249--257",
  booktitle =	 "Proceedings of the Conference on Programming Language
		  Design and Implementation (PLDI'98)",
  year =	 1998,
  publisher =	 "ACM Press",
  address =	 "Montreal, Canada",
  month =	 jun,
  urlpdf =       "http://www.cs.cmu.edu/~fp/papers/pldi98dml.pdf",
  keywords =     "fp"
}

@InProceedings{Xi99popl,
  author = 	 "Hongwei Xi and Frank Pfenning",
  title = 	 "Dependent Types in Practical Programming",
  editor =	 "A. Aiken",
  pages =	 "214--227",
  booktitle =	 "Conference Record of the 26th Symposium on Principles of
		  Programming Languages (POPL'99)",
  year =	 1999,
  publisher =    "ACM Press",
  month =	 jan,
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/popl99.pdf",
  keywords =     "fp"
}