cited18.bib

@comment{{This file has been generated by bib2bib 1.99}}
@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
}
@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}
}
@inproceedings{Balzer15agere,
  author = {Stephanie Balzer and Frank Pfenning},
  title = {Objects as Session-Typed Processes},
  booktitle = {Workshop on Programming based on Actors, Agents, and Decentralized
                  Control (AGERE! 2015)},
  year = 2015,
  publisher = {ACM SIGPLAN},
  pages = {13--24},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/agere15.pdf}
}
@inproceedings{Balzer17icfp,
  author = {Stephanie Balzer and Frank Pfenning},
  title = {Manifest Sharing with Session Types},
  booktitle = {International Conference on Functional Programming (ICFP)},
  year = 2017,
  pages = {37:1--37:29},
  month = sep,
  publisher = {ACM},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/icfp17.pdf},
  note = {Extended version available as Technical Report \href{http://www.cs.cmu.edu/~fp/papers/CMU-CS-17-106R.pdf}{CMU-CS-17-106R}, June 2017.}
}
@inproceedings{Balzer18concur,
  author = {Stephanie Balzer and Frank Pfenning and Bernardo Toninho},
  title = {A Universal Session Type for Untyped Asynchronous Communication},
  booktitle = {29th International Conference on Concurrency Theory (CONCUR'18)},
  year = 2018,
  editor = {S. Schewe and L. Zhang},
  pages = {30:1--30:18},
  month = sep,
  address = {Beijing, China},
  publisher = {LIPIcs 118},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/univtype18.pdf}
}
@unpublished{Balzer18un,
  author = {Stephanie Balzer and Bernardo Toninho and Frank Pfenning},
  title = {Manifest Deadlock-Freedom for Shared Session Types},
  note = {Submitted},
  month = nov,
  year = 2018,
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/deadlock18.pdf}
}
@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 Threats},
  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)},
  pages = {222--236},
  year = {2010},
  opteditor = {P.Gastin and F.Laroussinie},
  address = {Paris, France},
  month = aug,
  publisher = {Springer LNCS 6269},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/concur10.pdf}
}
@inproceedings{Caires12tldi,
  author = {Lu{\'\i}s Caires and Frank Pfenning and Bernardo Toninho},
  title = {Towards Concurrent Type Theory},
  booktitle = {Proceedings of the 7th Workshop for Types in Language Design
                  and Implementation},
  pages = {1--12},
  year = 2012,
  editor = {B. Pierce},
  series = {TLDI'12},
  address = {Philadelphia, Pennsylvania},
  month = jan,
  organization = {ACM},
  note = {Notes for an invited talk},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/tdli12.pdf}
}
@inproceedings{Caires13esop,
  author = {Lu{\'\i}s Caires and Jorge A. P{\'e}rez and Frank
                  Pfenning and Bernardo Toninho},
  title = {Behavioral Polymorphism and Parametricity in Session-Based Communication},
  booktitle = {Proceedings of the European Symposium on Programming (ESOP'13)},
  pages = {330--349},
  year = 2013,
  editor = {M.Felleisen and P.Gardner},
  address = {Rome, Italy},
  month = mar,
  publisher = {Springer LNCS 7792},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/esop13b.pdf}
}
@unpublished{Caires14un,
  author = {Lu{\'\i}s Caires and Jorge A. P\'erez and Frank Pfenning and Bernardo Toninho},
  title = {Logic-Based Domain-Aware Session Types},
  note = {Unpublished manuscript},
  year = 2014,
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/hill14.pdf}
}
@article{Caires16mscs,
  author = {Lu{\'\i}s Caires and Frank Pfenning and Bernardo Toninho},
  title = {Linear Logic Propositions as Session Types},
  journal = {Mathematical Structures in Computer Science},
  year = 2016,
  pages = {367--423},
  volume = 26,
  number = 3,
  note = {Special Issue on Behavioural Types.},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/mscs13.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},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/jlc03.pdf}
}
@inproceedings{Cervesato12lfmtp,
  author = {Iliano Cervesato and Frank Pfenning and Jorge Luis Sacchini and Carsten Sch{\"u}rmann and Robert J. Simmons},
  title = {Trace Matching in a Concurrent Logical Framework},
  booktitle = {Proceedings of the 7th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice},
  year = 2012,
  editor = {A. Chlipala and C. Sch{\"u}rmann},
  address = {Copenhagen, Denmark},
  month = sep,
  publisher = {ACM},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/lfmtp12.pdf}
}
@inproceedings{Cervesato12unif,
  author = {Iliano Cervesato and Frank Pfenning and Jorge Luis Sacchini and Carsten Sch{\"u}rmann and Robert J. Simmons},
  title = {On Matching Concurrent Traces},
  booktitle = {Proceedings of the 26th International Workshop on Unification},
  year = 2012,
  editor = {S. Escobar and K. Korovin and V. Rybakov},
  month = jul,
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/unif12.pdf}
}
@unpublished{Cervesato18un,
  author = {Iliano Cervesato and Thomas J. Cortina and Frank Pfenning and Saquib Razak},
  title = {An Approach to Teaching to Write Safe and Correct Imperative Programs
                  --- Even in {C}},
  note = {Unpublished manuscript},
  month = aug,
  year = 2018
}
@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 = {Bor-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}
}
@inproceedings{Cruz12damp,
  author = {Fl{\'a}vio Cruz and Michael Ashley-Rollman and Seth Copen Goldstein inad Ricardo Rocha and Frank Pfenning},
  title = {Bottom-Up Logic Programming for Multicores},
  booktitle = {Proceedings of the Workshop on Declarative Aspects of Multicore Programming},
  year = 2012,
  series = {DAMP'12},
  address = {Philadelphia, PA},
  month = jan,
  publisher = {ACM Press},
  note = {Short paper},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/damp12.pdf}
}
@article{Cruz14iclp,
  author = {Fl{\'a}vio Cruz and Ricardo Rocha and Seth Copen Goldstein and Frank Pfenning},
  title = {A Linear Logic Programming Language for Concurrent Programming over Graph Structures},
  journal = {Theory and Practice of Logic Programming},
  year = 2014,
  volume = 14,
  number = {4--5},
  pages = {493--507},
  month = jul,
  note = {Special issue dedicated to the 30th International Conference on Logic Programming (ICLP'14).
                  Best Paper Award},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/iclp14.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},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/hoots99.pdf}
}
@inproceedings{Das18icfp,
  author = {Ankush Das and Jan Hoffmann and Frank Pfenning},
  title = {Parallel Complexity Analysis with Temporal Session Types},
  booktitle = {Proceedings of International Conference on Functional Programming (ICFP'18)},
  year = {2018},
  editor = {M. Flatt},
  pages = {91:1--91:30},
  month = sep,
  address = {St. Louis, Missouri, USA},
  publisher = {ACM},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/icfp18.pdf}
}
@inproceedings{Das18lics,
  author = {Ankush Das and Jan Hoffmann and Frank Pfenning},
  title = {Work Analysis with Resource-Aware Session Types},
  booktitle = {Proceedings of 33rd Symposium on Logic in Computer Science (LICS'18)},
  editor = {Anuj Dawar and Erich Gr\"adel},
  pages = {305--314},
  month = jul,
  address = {Oxford, UK},
  year = {2018},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/lics18.pdf}
}
@unpublished{Das18un,
  author = {Ankush Das and Stephanie Balzer and Jan Hoffmann and Frank Pfenning},
  title = {Resource-Aware Session Types for Digital Contracts},
  note = {Submitted},
  month = nov,
  year = 2018,
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/contract18.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{DeYoung12csl,
  author = {Henry DeYoung and Lu{\'\i}s Caires and Frank
                  Pfenning and Bernardo Toninho},
  title = {Cut Reduction in Linear Logic as Asynchronous
                  Session-Typed Communication},
  booktitle = {Proceedings of the 21st Conference on Computer
                  Science Logic},
  pages = {228--242},
  year = 2012,
  editor = {P. C{\'e}gielski and A. Durand},
  series = {CSL 2012},
  address = {Fontainebleau, France},
  month = sep,
  publisher = {Leibniz International Proceedings in Informatics},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/csl12.pdf}
}
@inproceedings{DeYoung16aplas,
  author = {Henry DeYoung and Frank Pfenning},
  title = {Substructural Proofs as Automata},
  booktitle = {14th Asian Symposium on Programming Languages and Systems},
  year = 2016,
  editor = {A. Igarashi},
  pages = {3--22},
  month = nov,
  address = {Hanoi, Vietnam},
  publisher = {Springer LNCS 10017},
  note = {Invited talk},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/aplas16.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},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/INRIA-RR-3591.pdf}
}
@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 = {349--364},
  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{Garg10stm,
  author = {Deepak Garg and Frank Pfenning},
  title = {Stateful Authorization Logic --- Proof Theory and a Case Study},
  booktitle = {Proceedings of the 6th International Workshop on Security and
                  Trust Management (STM'10)},
  optpages = {},
  year = 2010,
  editor = {J.Cuellar and J.Lopez},
  address = {Athens, Greece},
  month = sep,
  publisher = {Springer LNCS},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/stm11.pdf}
}
@article{Garg12jcs,
  author = {Deepak Garg and Frank Pfenning},
  title = {Stateful Authorization Logic---Proof Theory and a Case Study},
  journal = {Journal of Computer Security},
  year = 2012,
  volume = 20,
  number = 4,
  pages = {353--391},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/jcs12.pdf}
}
@inproceedings{Gommerstadt18esop,
  author = {Hannah Gommerstadt and Limin Jia and Frank Pfenning},
  title = {Session-Typed Concurrent Contracts},
  booktitle = {European Symposium on Programming (ESOP'18)},
  year = 2018,
  editor = {A. Ahmed},
  pages = {771--798},
  month = apr,
  address = {Thessaloniki, Greece},
  publisher = {Springer LNCS 10801},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/esop18.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},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/ergo90.pdf},
  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{Jia16popl,
  author = {Limin Jia and Hannah Gommerstadt and Frank Pfenning},
  title = {Monitors and Blame Assignment for Higher-Order Session Types},
  booktitle = {43rd Annual Symposium on Principles of Programming Languages},
  year = 2016,
  month = jan,
  pages = {582--594},
  address = {St. Petersburg, Florida},
  publisher = {ACM Press},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/popl16.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,
  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,
  volume = 6,
  number = 4,
  pages = {1--50},
  month = dec,
  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{Morgenstern11stm,
  author = {Jamie Morgenstern and Deepak Garg and Frank Pfenning},
  title = {A Proof-Carrying File System with Revocable and Use-Once Certificates},
  booktitle = {Proceedings of the 7th International Workshop on
                  Security and Trust Management (STM 2011)},
  optpages = {},
  year = 2011,
  editor = {C.Meadows and C.Fernandez-Gago},
  address = {Copenhagen, Denmark},
  month = jun,
  publisher = {Springer LNCS},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/stm11.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},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/merlin03.pdf}
}
@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{Perez12esop,
  author = {Jorge A. P{\'e}rez and Lu{\'\i}s Caires and Frank Pfenning and Bernardo Toninho},
  title = {Termination in Session-Based Concurrency via Linear Logical Relations
},
  booktitle = {22nd European Symposium on Programming},
  pages = {539--558},
  year = 2012,
  editor = {H. Seidl},
  series = {ESOP'12},
  address = {Tallinn, Estonia},
  month = mar,
  publisher = {Springer LNCS 7211},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/esop12.pdf}
}
@article{Perez14ic,
  author = {Jorge A. P\'erez and Lu\'{\i}s Caires and Frank Pfenning and Bernardo Toninho},
  title = {Linear Logical Relations and Observational Equivalences for Session-Based Concurrency},
  journal = {Information and Computation},
  year = 2014,
  volume = 239,
  pages = {254--302},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/linlogrel13.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.cs.cmu.edu/~fp/papers/ic00.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},
  urlpdf = {http://www.cs.cmu.edu/~fp/talks/pepm00-abs.pdf}
}
@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
}
@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},
  year = 1997,
  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},
  urlpdf = {http://www.cs.cmu.edu/~fp/talks/lam10-talk.pdf}
}
@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)},
  pages = {1--2},
  year = {2010},
  editor = {K.Crary and M.Miculan},
  address = {Edinburgh, Scotland},
  month = jul,
  note = {Abstract of invited talk}
}
@inproceedings{Pfenning11cpp,
  author = {Frank Pfenning and Lu{\'\i}s Caires and Bernardo Toninho},
  title = {Proof-Carrying Code in a Session-Typed Process Calculus},
  booktitle = {1st International Conference on Certified Programs and Proofs},
  series = {CPP'11},
  year = 2011,
  pages = {21--36},
  opteditor = {J.-P. Jouannaud and Z. Shao},
  address = {Kenting, Taiwan},
  month = dec,
  publisher = {Springer LNCS 7086},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/cpp11.pdf}
}
@unpublished{Pfenning11un,
  author = {Frank Pfenning and Thomas J. Cortina and William Lovas},
  title = {Teaching Imperative Programming With Contracts at the Freshmen Level},
  note = {Experience report.  Unpublished manuscript},
  month = sep,
  year = 2011,
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/pic11.pdf}
}
@proceedings{Pfenning13fossacs,
  title = {Proceedings of the 16th International Conference on Foundations of Software Science and Computation Structures},
  year = 2013,
  editor = {Frank Pfenning},
  address = {ETAPS 2013, Rome, Italy},
  month = mar,
  publisher = {Springer LNCS 7794}
}
@article{Pfenning14tplp,
  author = {Frank Pfenning},
  title = {{Programming with Higher-Order Logic}, by Dale Miller and Gopalan Nadathur, Cambridge University Press, 2012},
  journal = {Theory and Practice of Logic Programming},
  year = 2014,
  volume = 14,
  number = 2,
  pages = {265--267},
  note = {Book review},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/tplp14.pdf}
}
@inproceedings{Pfenning15fossacs,
  author = {Frank Pfenning and Dennis Griffith},
  title = {Polarized Substructural Session Types},
  booktitle = {Proceedings of the 18th International Conference
                  on Foundations of Software Science and Computation Structures (FoSSaCS 2015)},
  year = {2015},
  editor = {A. Pitts},
  pages = {3--22},
  month = apr,
  address = {London, England},
  publisher = {Springer LNCS 9034},
  note = {Invited talk},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/fossacs15.pdf}
}
@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}
}
@unpublished{Pruiksma18aun,
  author = {Klaas Pruiksma and William Chargin and Frank Pfenning and Jason Reed},
  title = {Adjoint Logic and Its Concurrent Operational Interpretation},
  note = {Unpublished manuscript},
  month = jan,
  year = 2018,
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/adjoint18.pdf}
}
@unpublished{Pruiksma18bun,
  author = {Klaas Pruiksma and Frank Pfenning},
  title = {A Shared-Memory Semantics for Mixed Linear and Non-Linear Session Types},
  note = {Submitted},
  month = nov,
  year = 2018,
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/shmem18.pdf}
}
@unpublished{Pruiksma18un,
  author = {Klaas Pruiksma and William Chargin and Frank Pfenning and Jason Reed},
  title = {Adjoint Logic},
  note = {Unpublished manuscript},
  month = apr,
  url = {http://www.cs.cmu.edu/~fp/papers/adjoint18b.pdf},
  year = 2018
}
@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,
  url = {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{Silva16linearity,
  author = {Miguel Silva and M{\'a}rio Florido and Frank Pfenning},
  title = {Non-Blocking Concurrent Imperative Programming with Session Types},
  booktitle = {Fourth International Workshop on Linearity},
  pages = {64--72},
  year = 2016,
  month = jun,
  publisher = {EPTCS 238},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/nonblocking16.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}
}
@article{Simmons11hosc,
  author = {Robert J. Simmons and Frank Pfenning},
  title = {Logical Approximation for Program Analysis},
  journal = {Higher-Order and Symbolic Computation},
  year = 2011,
  volume = 24,
  number = {1--2},
  pages = {41--80},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/hosc11.pdf}
}
@techreport{Simmons11tr,
  author = {Robert J. Simmons and Frank Pfenning},
  title = {Weak Focusing for Ordered Linear Logic},
  institution = {Carnegie Mellon University},
  year = 2011,
  number = {CMU-CS-10-147},
  note = {Revision of April 2011},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/CMU-CS-10-147.pdf}
}
@unpublished{Simmons11xten,
  author = {Robert J. Simmons and Bernardo Toninho and Frank Pfenning},
  title = {Distributed Deductive Databases, Declaratively},
  note = {Short paper, ACM SIGPLAN X10 Workshop},
  month = jun,
  year = 2011,
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/xten11.pdf}
}
@inproceedings{Toninho11ppdp,
  author = {Bernardo Toninho and Lu{\'\i}s Caires and Frank Pfenning},
  title = {Dependent Session Types via Intuitionistic Linear Type Theory},
  booktitle = {Proceedings of the 13th International Conference on Principles
                  and Practice of Declarative Programming},
  series = {PPDP'11},
  pages = {161--172},
  year = 2011,
  opteditor = {P.Schneider-Kamp and M.Hanus},
  address = {Odense, Denmark},
  month = jul,
  publisher = {ACM},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/ppdp11.pdf}
}
@inproceedings{Toninho12fossacs,
  author = {Bernardo Toninho and Lu{\'\i}s Caires and Frank Pfenning},
  title = {Functions as Session-Typed Processes},
  booktitle = {15th International Conference on Foundations of Software
                  Science and Computation Structures},
  pages = {346--360},
  year = 2012,
  editor = {L. Birkedal},
  series = {FoSSaCS'12},
  address = {Tallinn, Estonia},
  month = mar,
  publisher = {Springer LNCS},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/fossacs12.pdf}
}
@inproceedings{Toninho13esop,
  author = {Bernardo Toninho and Lu{\'\i}s Caires and Frank Pfenning},
  title = {Higher-Order Processes, Functions, and Sessions: A Monadic Integration},
  booktitle = {Proceedings of the European Symposium on Programming (ESOP'13)},
  pages = {350--369},
  year = 2013,
  editor = {M.Felleisen and P.Gardner},
  address = {Rome, Italy},
  month = mar,
  publisher = {Springer LNCS 7792},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/papers/esop13a.pdf}
}
@inproceedings{Toninho14tgc,
  author = {Bernardo Toninho and Lu\'{\i}s Caires and Frank Pfenning},
  title = {Corecursion and Non-Divergence in Session-Typed Processes},
  booktitle = {Proceedings of the 9th International Symposium on Trustworthy Global Computing (TGC 2014)},
  year = 2014,
  editor = {M. Maffei and E. Tuosto},
  pages = {159--175},
  month = sep,
  address = {Rome, Italy},
  publisher = {Springer LNCS 8902},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/tgc14.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{Willsey16linearity,
  author = {Max Willsey and Rokhini Prabhu and Frank Pfenning},
  title = {Design and Implementation of {C}oncurrent {C0}},
  booktitle = {Fourth International Workshop on Linearity},
  pages = {73--82},
  year = 2016,
  month = jun,
  publisher = {EPTCS 238},
  urlpdf = {http://www.cs.cmu.edu/~fp/papers/cc016.pdf}
}
@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}
}

This file was generated by bibtex2html 1.99.