@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.*