@InProceedings{Abel01ptp,
author = "Andreas Abel and Bor-Yuh Evan Chang and Frank Pfenning",
title = "Human-Readable, Machine-Verifiable Proofs for Teaching
Constructive Logic",
booktitle = "Proceedings of the Workshop on Proof Transformations, Proof
Presentations and Complexity of Proofs (PTP'01)",
year = 2001,
address = "Siena, Italy",
month = jun,
urlpdf = "http://www.cs.cmu.edu/~fp/papers/ptp01.pdf",
}
@InProceedings{Anderson04tphols,
author = {Penny Anderson and Frank Pfenning},
title = {Verifying Uniqueness in a Logical Framework},
booktitle = {Proceedings of the 17th International Conference on
Theorem Proving in Higher Order Logics (TPHOLs'04)},
pages = {18--33},
year = 2004,
editor = {K.Slind and A.Bunker and G.Gopalakrishnan},
address = {Park City, Utah},
month = sep,
publisher = {Springer LNCS 3223},
keywords = {LF, Elf},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/tphols04.pdf},
}
@Article{Andrews04jar,
author = {Peter B. Andrews and Matthew Bishop and Chad E. Brown and
Sunil Issar and Frank Pfenning and Hongwei Xi},
title = {{ETPS}: A System to Help Students Write Formal Proofs},
journal = {Journal of Automated Reasoning},
volume = 32,
number = 1,
pages = {75--92},
year = 2004,
url = {http://journals.kluweronline.com/article.asp?PIPS=5264938}
}
@Article{Andrews84,
author = "Peter B. Andrews and Dale Miller and Eve Cohen and Frank
Pfenning",
title = "Automating Higher-Order Logic",
journal = "Contemporary Mathematics",
volume = 29,
month = aug,
year = 1984,
pages = "169--192",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/conm84.pdf",
keywords = "TPS, atp"
}
@InProceedings{Andrews90,
author = "Peter B. Andrews and Sunil Issar and Dan Nesmith and Frank
Pfenning",
title = "The {TPS} Theorem Proving System",
booktitle = "10th International Conference on Automated Deduction",
address = "Kaiserslautern, Germany",
editor = "M.E. Stickel",
publisher = "Springer-Verlag LNCS 449",
month = jul,
year = 1990,
pages = "641--642",
note = "System abstract",
keywords = "TPS, atp",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/cade90tps.pdf"
}
@InProceedings{Andrews94,
author = "Peter B. Andrews and Matthew Bishop and Sunil Issar and Dan
Nesmith and Frank Pfenning and Hongwei Xi",
title = "{TPS}: An Interactive and Automatic Tool for Proving Theorems
of Type Theory",
booktitle = "Proceedings of the 6th International Workshop on Higher Order
Logic Theorem Proving and Its Applications",
address = "Vancouver, B.C., Canada",
editor = "Jeffrey J. Joyce and Carl-Johan H. Seger",
publisher = "Springer-Verlag LNCS 780",
month = aug,
year = 1993,
pages = "366--370",
keywords = "TPS, atp"
}
@Article{Andrews96,
author = "Peter B. Andrews and Matthew Bishop and Sunil Issar and Dan
Nesmith and Frank Pfenning and Hongwei Xi",
title = "{TPS}: A Theorem Proving System for Classical Type Theory",
journal = "Journal of Automated Reasoning",
volume = 16,
number = 3,
month = jun,
pages = "321--353",
year = "1996",
keywords = "TPS, atp"
}
@InCollection{Bauer07isr,
author = {Lujo Bauer and Frank Pfenning and Michael K. Reiter},
title = {Distributed System Security via Logical Frameworks},
booktitle = {Information Security Research: New Methods for Protecting Against Cyber Threads},
pages = {108--115},
publisher = {Department of Defense, Wiley Publishing},
year = 2007
}
@InProceedings{Berna03ijcai,
author = {M. Berna and B. Lisien and B. Sellner and G. Gordon and
F. Pfenning and and S. Thrun},
title = {A Learning Algorithm for Localizing People Based on Wireless
Signal Strength that Uses Labeled and Unlabeled Data},
booktitle = {Proceedings of the 18th International Joint Conference on
Artificial Intelligence (IJCAI'03)},
year = 2003,
address = {Acapulco, Mexico},
month = aug,
note = {Poster},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/ijcai03.pdf}
}
@InProceedings{Bowers07ndss,
author = {Kevin D. Bowers and Lujo Bauer and Deepak Garg and
Frank Pfenning and Michael K. Reiter},
title = {Consumable Credentials in Logic-Based Access-Control Systems},
booktitle = {Proceedings of the 14th Annual Network and Distributed
System Security Symposium (NDSS'07)},
pages = {143--157},
year = 2007,
address = {San Diego, California},
month = feb,
publisher = {Internet Society},
note = {Preliminary version available as
Technical Report CMU-CYLAB-06-002, Carnegie Mellon University, February 2006},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/ndss07.pdf}
}
@InProceedings{Caires10concur,
author = {Lu{\'\i}s Caires and Frank Pfenning},
title = {Session Types as Intuitionistic Linear Propositions},
booktitle = {Proceedings of the 21st International Conference on Concurrency Theory (CONCUR 2010)},
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}
}
@Article{Caires13mscs,
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 = {2013},
OPTkey = {},
OPTvolume = {},
OPTnumber = {},
OPTpages = {},
OPTmonth = {},
note = {To appear. Special Issue on Behavioural Types.},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/mscs13.pdf},
OPTannote = {}
}
@Article{Cervesato00tcs,
author = "Iliano Cervesato and Joshua S. Hodas and Frank Pfenning",
title = "Efficient Resource Management for Linear Logic Proof Search",
journal = "Theoretical Computer Science",
year = 2000,
volume = 232,
number = "1--2",
month = feb,
pages = "133--163",
note = "Special issue on Proof Search in
Type-Theoretic Languages, D. Galmiche and D. Pym, editors",
keywords = "LF, Elf, linear",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/erm97.pdf",
}
@Article{Cervesato02ic,
title = "A Linear Logical Framework",
author = "Iliano Cervesato and Frank Pfenning",
journal = "Information \& Computation",
volume = 179,
number = 1,
pages = "19--75",
year = 2002,
month = nov,
urlpdf = "http://www.cs.cmu.edu/~fp/papers/llf00.pdf",
note = "Revised and expanded version of an extended abstract,
LICS 1996, pp. 264-275"
}
@TechReport{Cervesato02tr,
author = {Iliano Cervesato and Frank Pfenning and David Walker
and Kevin Watkins},
title = {A Concurrent Logical Framework {II}: Examples and Applications},
institution = {Department of Computer Science, Carnegie Mellon University},
year = 2002,
number = {CMU-CS-02-102},
note = {Revised May 2003},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/CMU-CS-02-102.pdf}
}
@article{Cervesato03jlc,
author = {Iliano Cervesato and Frank Pfenning},
title = {A Linear Spine Calculus},
journal = {Journal of Logic and Computation},
year = 2003,
volume = 13,
number = 5,
pages = {639--688}
}
@InProceedings{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}
}
@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},
url = {http://www.cs.cmu.edu/~fp/papers/damp12.pdf}
}
@TechReport{Danvy95,
author = "Olivier Danvy and Frank Pfenning",
title = "The Occurrence of Continuation Parameters in {CPS} Terms",
institution = "Department of Computer Science, Carnegie Mellon University",
year = 1995,
number = "CMU-CS-95-121",
month = feb,
keywords = "LF, Elf",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/cpsocc95.pdf"
}
@InProceedings{Danvy99hoots,
author = "Olivier Danvy and Belmina Dzafic and Frank Pfenning",
title = "On Proving Syntactic Properties of {CPS} Programs",
editor = "Andrew Gordon and Andrew Pitts",
booktitle = "Proceedings of the Third International Workshop on Higher
Order Operational Techniques in Semantics (HOOTS'99)",
year = 1999,
address = "Paris",
month = sep,
note = "Electronic Notes in Theoretical Computer
Science, Volume 26",
keywords = "fp",
url = "http://www.elsevier.nl/locate/entcs/volume26.html",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/hoots99.pdf",
}
@InProceedings{Davies00icfp,
author = "Rowan Davies and Frank Pfenning",
title = "Intersection Types and Computational Effects",
editor = "P. Wadler",
booktitle = "Proceedings of the Fifth International Conference on
Functional Programming (ICFP'00)",
year = 2000,
pages = "198--208",
publisher = "ACM Press",
address = "Montreal, Canada",
month = sep,
urlpdf = "http://www.cs.cmu.edu/~fp/papers/icfp00.pdf",
}
@Article{Davies01jacm,
author = "Rowan Davies and Frank Pfenning",
title = "A Modal Analysis of Staged Computation",
journal = "Journal of the ACM",
year = 2001,
volume = 48,
number = 3,
month = may,
pages = "555--604",
keywords = "fp, staged",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/jacm00.pdf",
}
@InProceedings{Davies96popl,
author = "Rowan Davies and Frank Pfenning",
title = "A Modal Analysis of Staged Computation",
editor = "Guy {Steele, Jr.}",
booktitle = "Proceedings of the 23rd Annual Symposium on Principles of
Programming Languages",
year = 1996,
publisher = "ACM Press",
address = "St. Petersburg Beach, Florida",
month = jan,
pages = "258--270",
annote = "Extended version available as Technical Report
CMU-CS-95-145, Carnegie Mellon University, May 1995",
keywords = "fp, staged",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/popl96.pdf",
}
@TechReport{DeYoung07tr,
author = {Henry DeYoung and Deepak Garg and Frank Pfenning},
title = {An Authorization Logic with Explicit Time},
institution = {Carnegie Mellon University, Department of Computer Science},
year = 2007,
number = {CMU-CS-07-166},
month = dec,
note = {Revised February 2008},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/CMU-CS-07-166}
}
@InProceedings{DeYoung09fcs,
author = {Henry DeYoung and Frank Pfenning},
title = {Reasoning about the Consequences of Authorization Policies in a Linear Epistemic Logic},
booktitle = {Workshop on Foundations of Computer Security (FCS'09)},
year = 2009,
address = {Los Angeles, California},
month = aug,
urlpdf = {http://www.cs.cmu.edu/~fp/papers/fcs09.pdf}
}
@InProceedings{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{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{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{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}
}
@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}
}
@Unpublished{Perez13un,
author = {Jorge A. P{\'e}rez and Lu\'{\i}s Caires and Frank Pfenning and Bernardo Toninho},
title = {Linear Logical Relations and Observational Equivalences for Session-Based Concurrency},
note = {Submitted},
month = oct,
year = 2013,
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.idealibrary.com/links/artid/inco.1999.2832/production/pdf",
keywords = "LF, Elf"
}
@InProceedings{Pfenning00pepm,
author = "Frank Pfenning",
title = "On the Logical Foundations of Staged Computation",
editor = "Julia Lawall",
pages = 33,
booktitle = "Proceedings of the Workshop on Partial Evaluation and
Semantics-Based Program Manipulation (PEPM'00)",
year = 2000,
publisher = "ACM Press",
address = "Boston, Massachusetts",
month = jan,
note = "Abstract of invited talk",
keywords = "staged, logic",
url = "http://www.cs.cmu.edu/~fp/talks/pepm00-talk.ps"
}
@InProceedings{Pfenning00saig,
author = "Frank Pfenning",
title = "Reasoning About Staged Computation",
editor = "W. Taha",
pages = "5--6",
booktitle = "Proceedings of the International Workshop on
Semantics, Applications, and Implementation of Program
Generation (SAIG 2000)",
year = 2000,
publisher = "Springer-Verlag LNCS 1924",
address = "Montreal, Canada",
month = sep,
note = "Abstract of invited talk",
keywords = "staged, logic",
url = "http://www.cs.cmu.edu/~fp/talks/saig00-talk.pdf"
}
@Article{Pfenning01alp,
author = "Frank Pfenning",
title = "Logical Frameworks at {CMU}",
journal = "ALP Newsletter",
year = 2001,
volume = 14,
number = 2,
month = may,
keywords = "LF, Elf",
url = "http://www.cwi.nl/projects/alp/newsletter/nav/pfenning.html"
}
@InCollection{Pfenning01handbook,
author = "Frank Pfenning",
title = "Logical Frameworks",
booktitle = "Handbook of Automated Reasoning",
chapter = 17,
pages = "1063--1147",
publisher = "Elsevier Science and MIT Press",
year = 2001,
editor = "Alan Robinson and Andrei Voronkov",
keywords = "LF, Elf, misc",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/handbook01.pdf",
}
@InProceedings{Pfenning01lics,
author = "Frank Pfenning",
title = "Intensionality, Extensionality, and Proof Irrelevance in
Modal Type Theory",
editor = "J. Halpern",
booktitle = "Proceedings of the 16th Annual Symposium on Logic in
Computer Science (LICS'01)",
pages = "221--230",
year = 2001,
publisher = "IEEE Computer Society Press",
address = "Boston, Massachusetts",
month = jun,
keywords = "LF, Elf",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/lics01.pdf",
}
@Article{Pfenning01mscs,
author = "Frank Pfenning and Rowan Davies",
title = "A Judgmental Reconstruction of Modal Logic",
journal = "Mathematical Structures in Computer Science",
year = 2001,
volume = 11,
pages = "511--540",
note = "Notes to an invited talk at the {\em Workshop
on Intuitionistic Modal Logics and Applications} (IMLA'99),
Trento, Italy, July 1999",
keywords = "staged, logic",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/mscs00.pdf",
}
@Proceedings{Pfenning02lfm,
title = {Proceedings of the 3rd International Workshop on Logical Frameworks and Meta-Languages (LFM'02)},
year = 2002,
editor = {Frank Pfenning},
volume = {70(2)},
series = {Electronic Notes in Theoretical Computer Science},
address = {Copenhagen, Denmark},
month = jul,
url = {http://www.elsevier.nl/locate/entcs/volume70.html}
}
@InCollection{Pfenning02mdorf,
author = {Frank Pfenning},
title = {Logical Frameworks---A Brief Introduction},
booktitle = {Proof and System-Reliability},
pages = {137--166},
publisher = {Kluwer Academic Publishers},
year = 2002,
editor = {H. Schwichtenberg and R. Steinbr{\"u}ggen},
volume = 62,
series = {NATO Science Series {II}},
note = {Lecture notes from the Marktoberdorf Summer School, July 2001},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/mdorf01.pdf},
}
@Book{Pfenning03gpce,
editor = {Frank Pfenning and Yannis Smaragdakis},
title = {Proceedings of the Second International Conference on
Generative Programming and Component Engineering},
publisher = {Springer-Verlag LNCS 2830},
year = 2003,
address = {Erfurt, Germany},
month = sep
}
@InProceedings{Pfenning04aplas,
author = {Frank Pfenning},
title = {Substructural Operational Semantics and Linear Destination-Passing Style},
booktitle = {Proceedings of the 2nd Asian Symposium on Programming Languages and Systems (APLAS'04)},
pages = 196,
year = 2004,
editor = {W.-N. Chin},
address = {Taipei, Taiwan},
month = nov,
publisher = {Springer-Verlag LNCS 3302},
note = {Abstract of invited talk},
urlpdf = {http://www.cs.cmu.edu/~fp/talks/aplas04-abs.pdf},
}
@Article{Pfenning04bsl,
author = {Frank Pfenning},
title = {Review of ``{Benjamin C.~Pierce}: {Types and programming languages}, {The MIT Proess}, {Cambridge, Massachusetts}, 2002''},
journal = {Bulletin of Symbolic Logic},
year = 2004,
volume = 10,
pages = {213--214},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/pierce03.pdf},
}
@Book{Pfenning05book,
author = "Frank Pfenning",
title = "Computation and Deduction",
publisher = "Cambridge University Press",
OPTyear = "",
note = "In preparation. Draft from April 1997 available
electronically",
keywords = "LF, Elf",
url = "http://www.cs.cmu.edu/~twelf/notes/cd.ps"
}
@InProceedings{Pfenning05merlin,
author = {Frank Pfenning},
title = {Towards a Type Theory of Contexts},
booktitle = {Proceedings of the 3rd Workshop on Mechanized Reasoning
About Languages with Variable Binding (MERLIN'05)},
pages = 1,
year = 2005,
address = {Tallinn, Estonia},
month = sep,
publisher = {ACM Press},
note = {Abstract for invited talk}
}
@Proceedings{Pfenning06rta,
title = {Proceedings of the 17th International Conference on Rewriting Techniques
and Applications},
year = 2006,
editor = {Frank Pfenning},
address = {Seattle, Washington},
month = aug,
publisher = {Springer Verlag LNCS 4098}
}
@Proceedings{Pfenning07cade,
title = {Proceedings of the 21st International Conference on Automated Deduction (CADE-21)},
year = 2007,
editor = {F. Pfenning},
address = {Bremen, Germany},
month = jul,
publisher = {Springer LNCS 4603}
}
@InProceedings{Pfenning07icfp,
author = {Frank Pfenning},
title = {Subtyping and Intersection Types Revisited},
booktitle = {Proceedings of the 12th International Symposium on Functional Programming (ICFP 2007)},
pages = 219,
year = 2007,
editor = {R. Hinze and N. Ramsey},
address = {Freiburg, Germany},
month = oct,
publisher = {ACM Press},
note = {Abstract of invited talk}
}
@InProceedings{Pfenning07tlca,
author = {Frank Pfenning},
title = {On a Logical Foundation for Explicit Substitutions},
booktitle = {Proceedings of the 8th International Conference on Typed
Lambda Calculi and Applications (TLCA 2007)},
pages = 1,
year = 2007,
editor = {S. Ronchi Della Rocca},
address = {Paris, France},
month = jun,
publisher = {Springer LNCS 4583},
note = {Abstract of TLCA/RTA joint invited talk}
}
@InCollection{Pfenning08andrews,
author = {Frank Pfenning},
booktitle = {Reasoning in Simple Type Theory: Festschrift in Honor of {P}eter {B.} {A}ndrews on His 70th Birthday},
title = {Church and {C}urry: Combining Intrinsic and Extrinsic Typing},
pages = {303--338},
publisher = {College Publications},
year = 2008,
series = {Studies in Logic 17},
editor = {C.Benzm{\"u}ller and C.Brown and J.Siekmann and R.Statman},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/andrews08.pdf}
}
@Proceedings{Pfenning08lics,
title = {Proceedings of the 23rd Annual Symposium on Logic in Computer Science (LICS 2008)},
year = 2008,
editor = {F. Pfenning},
address = {Pittsburgh, Pennsylvania},
month = jun,
publisher = {IEEE Computer Society Press}
}
@InProceedings{Pfenning09lics,
author = {Frank Pfenning and Robert J. Simmons},
title = {Substructural Operational Semantics as Ordered Logic Programming},
booktitle = {Proceedings of the 24th Annual Symposium on Logic in Computer Science (LICS 2009)},
pages = {101--110},
year = 2009,
address = {Los Angeles, California},
month = aug,
publisher = {IEEE Computer Society Press},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/lics09.pdf}
}
@InProceedings{Pfenning10lam,
author = {Frank Pfenning},
title = {Possession as Linear Knowledge},
booktitle = {Proceedings of the 3rd International Workshop on Logics, Agents, and Mobility (LAM 2010)},
OPTpages = {},
year = {2010},
editor = {B.Farwer},
address = {Edinburgh, Scotland},
month = jul,
note = {Abstract of invited talk},
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},
urlpdf = {http://www.springer.com/computer/theoretical+computer+science/book/978-3-642-37075-5}
}
@InProceedings{Pfenning84,
author = "Frank Pfenning",
title = "Analytic and Non-Analytic Proofs",
booktitle = "Proceedings of the 7th Conference on Automated Deduction",
address = "Napa, California",
publisher = "Springer-Verlag LNCS 170",
editor = "R.E. Shostak",
month = may,
year = 1984,
pages = "394--413",
keywords = "TPS, atp",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/cade84.pdf"
}
@PhdThesis{Pfenning87,
author = "Frank Pfenning",
title = "Proof Transformations in Higher-Order Logic",
school = "Carnegie Mellon University",
month = jan,
year = 1987,
keywords = "TPS, atp, logic",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/thesis87.pdf"
}
@InProceedings{Pfenning88cade,
author = "Frank Pfenning",
title = "Single Axioms in the Implicational Propositional Calculus",
booktitle = "Proceedings of the 9th International Conference on Automated
Deduction",
address = "Argonne, Illinois",
publisher = "Springer-Verlag LNCS 310",
month = may,
year = "1988",
editor = "Ewing Lusk and Ross Overbeek",
pages = "710--713",
note = "Problem set",
keywords = "atp",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/cade88.pdf"
}
@InProceedings{Pfenning88lfp,
author = "Frank Pfenning",
title = "Partial Polymorphic Type Inference and Higher-Order
Unification",
booktitle = "Proceedings of the 1988 {ACM} Conference on {Lisp} and
Functional Programming",
publisher = "ACM Press",
month = jul,
year = "1988",
pages = "153--163",
address = "Snowbird, Utah",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/lfp88.pdf",
keywords = "lambda-Prolog, unification"
}
@InProceedings{Pfenning88pldi,
author = "Frank Pfenning and Conal Elliott",
title = "Higher-Order Abstract Syntax",
booktitle = "Proceedings of the {ACM SIGPLAN '88} Symposium on Language
Design and Implementation",
address = "Atlanta, Georgia",
month = jun,
year = "1988",
pages = "199--208",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/pldi88.pdf",
keywords = "lambda-Prolog"
}
@Article{Pfenning89jsl,
author = "Frank Pfenning",
title = "Review of ``{Jean H.~Gallier}: {Logic for
Computer Science}, {Harper \& Row}, {New York} 1986''",
journal = "Journal of Symbolic Logic",
volume = 54,
number = 1,
month = mar,
year = 1989,
pages = "288--289",
keywords = "misc"
}
@InProceedings{Pfenning89lics,
author = "Frank Pfenning",
title = "{Elf}: A Language for Logic Definition and Verified
Meta-Programming",
booktitle = "Fourth Annual Symposium on Logic in Computer Science",
address = "Pacific Grove, California",
publisher = "IEEE Computer Society Press",
month = jun,
year = "1989",
pages = "313--322",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/lics89.pdf",
keywords = "LF, Elf"
}
@InProceedings{Pfenning89mfps,
author = "Frank Pfenning and Christine Paulin-Mohring",
title = "Inductively Defined Types in the {Calculus of Constructions}",
booktitle = "Proceedings of the Fifth Conference on the Mathematical
Foundations of Programming Semantics, Tulane University, New
Orleans, Louisiana",
publisher = "Springer-Verlag LNCS 442",
month = mar,
year = 1989,
editor = "M. Main and A. Melton and M. Mislove and D. Schmidt",
pages = "209--228",
keywords = "tt",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/mfps89.pdf"
}
@InProceedings{Pfenning89tapsoft,
author = "Frank Pfenning and Peter Lee",
title = "{LEAP}: A Language with Eval and Polymorphism",
booktitle = "Proceedings of the International Joint Conference on Theory
and Practice in Software Development",
address = "Barcelona, Spain",
publisher = "Springer-Verlag LNCS 352",
month = mar,
year = 1989,
pages = "345--359",
keywords = "fp",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/tapsoft89.pdf"
}
@InProceedings{Pfenning90cade,
author = "Frank Pfenning and Daniel Nesmith",
title = "Presenting Intuitive Deductions via Symmetric
Simplification",
booktitle = "10th International Conference on Automated Deduction",
address = "Kaiserslautern, Germany",
publisher = "Springer-Verlag LNCS 449",
month = jul,
year = 1990,
editor = "M.E. Stickel",
pages = "336--350",
keywords = "TPS, atp",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/cade90.pdf"
}
@Article{Pfenning90cm,
author = "Frank Pfenning",
title = "Program Development Through Proof Transformation",
journal = "Contemporary Mathematics",
volume = 106,
year = 1990,
pages = "251--262",
keywords = "Ergo, fp",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/conm90.pdf"
}
@InProceedings{Pfenning90iclp,
author = "Frank Pfenning",
title = "Types in Logic Programming",
booktitle = "Proceedings of the Seventh International Conference on Logic
Programming",
editor = "David H.D. Warren and Peter Szeredi",
publisher = "MIT Press",
month = jun,
year = 1990,
note = "Abstract of advanced tutorial",
keywords = "lp",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/iclp90.pdf"
}
@InProceedings{Pfenning91lf,
author = "Frank Pfenning",
title = "Logic Programming in the {LF} Logical Framework",
booktitle = "Logical Frameworks",
editor = "G\'{e}rard Huet and Gordon Plotkin",
publisher = "Cambridge University Press",
pages = "149--181",
year = "1991",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/lfproc91.pdf",
keywords = "LF, Elf"
}
@InProceedings{Pfenning91lics,
author = "Frank Pfenning",
title = "Unification and Anti-Unification in the {Calculus} of
{Constructions}",
booktitle = "Sixth Annual {IEEE} Symposium on Logic in Computer Science",
address = "Amsterdam, The Netherlands",
month = jul,
year = "1991",
pages = "74--85",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/lics91.pdf",
keywords = "LF, Elf, unification"
}
@Article{Pfenning91tcs,
author = "Frank Pfenning and Peter Lee",
title = "Metacircularity in the Polymorphic {$\lambda$}-Calculus",
journal = "Theoretical Computer Science",
volume = 89,
year = 1991,
pages = "137--159",
keywords = "fp"
}
@Book{Pfenning92book,
editor = "Frank Pfenning",
title = "Types in Logic Programming",
publisher = "MIT Press",
address = "Cambridge, Massachusetts",
year = 1992,
keywords = "logic programming"
}
@InProceedings{Pfenning92cade,
author = "Frank Pfenning and Ekkehard Rohwedder",
title = "Implementing the Meta-Theory of Deductive Systems",
booktitle = "Proceedings of the 11th International Conference on Automated
Deduction",
address = "Saratoga Springs, New York",
editor = "D. Kapur",
publisher = "Springer-Verlag LNAI 607",
month = jun,
year = "1992",
pages = "537--551",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/cade92.pdf",
keywords = "LF, Elf"
}
@InCollection{Pfenning92tilp,
author = "Frank Pfenning",
title = "Dependent Types in Logic Programming",
booktitle = "Types in Logic Programming",
editor = "Frank Pfenning",
publisher = "MIT Press",
address = "Cambridge, Massachusetts",
chapter = "10",
pages = "285--311",
year = "1992",
keywords = "LF, Elf"
}
@Article{Pfenning93fi,
author = "Frank Pfenning",
title = "On the Undecidability of Partial Polymorphic Type
Reconstruction",
journal = "Fundamenta Informaticae",
volume = 19,
number = "1,2",
year = 1993,
pages = "185--199",
note = "Preliminary version available as Technical Report
CMU-CS-92-105, School of Computer Science, Carnegie Mellon
University, January 1992",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/CMU-CS-92-105.pdf",
keywords = "fp"
}
@InProceedings{Pfenning93types,
author = "Frank Pfenning",
title = "Refinement Types for Logical Frameworks",
booktitle = "Informal Proceedings of the Workshop on Types for Proofs
and Programs",
editor = "Herman Geuvers",
address = "Nijmegen, The Netherlands",
month = may,
year = "1993",
pages = "285--299",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/rlf93.pdf",
keywords = "LF, Elf, lambda-Prolog"
}
@InProceedings{Pfenning94cade,
author = "Frank Pfenning",
title = "Elf: A Meta-Language for Deductive Systems",
booktitle = "Proceedings of the 12th International Conference on Automated
Deduction",
editor = "A. Bundy",
publisher = "Springer-Verlag LNAI 814",
address = "Nancy, France",
month = jun,
year = "1994",
pages = "811--815",
note = "System abstract",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/cade94.pdf",
keywords = "LF, Elf"
}
@Proceedings{Pfenning94lpar,
title = "Logic Programming and Automated Reasoning, 5th International
Conference, LPAR'94",
year = 1994,
editor = "Frank Pfenning",
publisher = "Springer-Verlag LNAI 822",
address = "Kiev, Ukraine",
month = jul,
keywords = "lp"
}
@TechReport{Pfenning94trb,
author = "Frank Pfenning",
title = "Structural Cut Elimination in Linear Logic",
institution = "Department of Computer Science, Carnegie Mellon University",
year = 1994,
number = "CMU-CS-94-222",
month = dec,
urlpdf = "http://www.cs.cmu.edu/~fp/papers/cutlin94.pdf",
keywords = "LF, Elf, linear"
}
@Misc{Pfenning94www,
author = "Frank Pfenning",
title = "Logical Frameworks",
howpublished = "\href{http://www.cs.cmu.edu/~fp/lfs.html}{Home page
and bibliography} on the World-Wide Web",
year = 1994,
month = oct,
keywords = "LF, Elf"
}
@InProceedings{Pfenning95lics,
author = "Frank Pfenning",
title = "Structural Cut Elimination",
editor = "D. Kozen",
booktitle = "Proceedings of the Tenth Annual Symposium on Logic in
Computer Science",
year = 1995,
publisher = "IEEE Computer Society Press",
address = "San Diego, California",
month = "June",
pages = "156--166",
keywords = "LF, Elf, linear",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/lics95.pdf",
}
@InProceedings{Pfenning95mfps,
author = "Frank Pfenning and Hao-Chi Wong",
title = "On a Modal $\lambda$-Calculus for {S4}",
booktitle = "Proceedings of the Eleventh Conference on
Mathematical Foundations of Programming Semantics",
editor = "S. Brookes and M. Main",
year = 1995,
address = "New Orleans, Louisiana",
month = mar,
note = "{\em Electronic Notes in Theoretical Computer
Science}, Volume 1, Elsevier",
keywords = "misc",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/mfps95.pdf",
}
@InProceedings{Pfenning96caap,
author = "Frank Pfenning",
title = "The Practice of Logical Frameworks",
booktitle = "Proceedings of the Colloquium on Trees in Algebra and
Programming",
editor = "H{\'e}l{\`e}ne Kirchner",
year = 1996,
publisher = "Springer-Verlag LNCS 1059",
address = "Link{\"o}ping, Sweden",
month = apr,
pages = "119--134",
note = "Invited talk",
keywords = "ALF, Automath, Elf, FS0, Isabelle, lambda-Prolog,
LF, linear, misc, Pi, rewriting, unification",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/caap96.pdf",
}
@InProceedings{Pfenning98cade,
author = "Frank Pfenning",
title = "Reasoning About Deductions in Linear Logic",
editor = "Claude Kirchner and H{\'e}l{\`e}ne Kirchner",
pages = "1--2",
booktitle = "Proceedings of the 15th International Conference on
Automated Deduction (CADE-15)",
year = 1998,
publisher = "Springer-Verlag LNCS 1421",
address = "Lindau, Germany",
month = jul,
note = "Abstract for invited talk",
keywords = "LF, Elf, linear",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/cade98inv.pdf",
}
@Manual{Pfenning98guide,
title = "Twelf User's Guide",
author = "Frank Pfenning and Carsten Sch{\"u}rmann",
edition = "1.2",
year = 1998,
month = sep,
keywords = "LF, Elf",
note = "Available as Technical Report CMU-CS-98-173, Carnegie
Mellon University",
urlhtml = "http://www.cs.cmu.edu/~twelf/guide"
}
@InProceedings{Pfenning98types,
author = "Frank Pfenning and Carsten Sch{\"u}rmann",
title = "Algorithms for Equality and Unification in the
Presence of Notational Definitions",
editor = "T. Altenkirch and W. Naraschewski and B. Reus",
booktitle = "Types for Proofs and Programs",
month = mar,
year = 1998,
pages = "179--193",
address = "Kloster Irsee, Germany",
publisher = "Springer-Verlag LNCS 1657",
keywords = "LF, Elf",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/types98.pdf",
}
@InProceedings{Pfenning99cade,
author = "Frank Pfenning and Carsten Sch{\"u}rmann",
title = "System Description: Twelf --- A Meta-Logical Framework for
Deductive Systems",
editor = "H. Ganzinger",
pages = "202--206",
booktitle = "Proceedings of the 16th International Conference on
Automated Deduction (CADE-16)",
year = 1999,
publisher = "Springer-Verlag LNAI 1632",
address = "Trento, Italy",
month = jul,
keywords = "LF, Elf",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/cade99.pdf",
}
@InProceedings{Pfenning99ppdp,
author = "Frank Pfenning",
title = "Logical and Meta-Logical Frameworks",
editor = "G. Nadathur",
pages = "206",
booktitle = "Proceedings of the International Conference on Principles
and Practice of Declarative Programming (PPDP'99)",
year = 1999,
publisher = "Springer-Verlag LNCS 1702",
address = "Paris, France",
month = sep,
note = "Abstract of invited talk.",
keywords = "LF, Elf"
}
@InProceedings{Pientka00induct,
author = "Brigitte Pientka and Frank Pfenning",
title = "Termination and Reduction Checking in the Logical Framework",
editor = "Carsten Sch{\"u}rmann",
booktitle = "Workshop on Automation of Proofs by Mathematical Induction",
year = 2000,
address = "Pittsburgh, Pennsylvania",
month = jun,
keywords = "LF, Elf, rewriting",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/induct00.pdf",
}
@InProceedings{Pientka03cade,
author = {Brigitte Pientka and Frank Pfenning},
title = {Optimizing Higher-Order Pattern Unification},
booktitle = {Proceedings of the 19th Conference on Automated Deduction
(CADE-19)},
pages = {473--487},
year = 2003,
editor = {F. Baader},
address = {Miami Beach, Florida},
month = jul,
publisher = {Springer-Verlag LNAI 2741},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/optunif03.pdf},
}
@InProceedings{Plesko99,
author = "Mark Plesko and Frank Pfenning",
title = "A Formalization of the Proof-Carrying Code Architecture in a
Linear Logical Framework",
editor = "A. Pnueli and P. Traverso",
booktitle = "Proceedings of the FLoC Workshop on Run-Time Result
Verification",
year = 1999,
address = "Trento, Italy",
month = jul,
keywords = "PCC, LF, Elf, linear",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/pccllf99.pdf",
}
@InProceedings{Polakow00lfm,
author = "Jeff Polakow and Frank Pfenning",
title = "Properties of Terms in Continuation-Passing Style in
an Ordered Logical Framework",
editor = "Jo{\"e}lle Despeyroux",
booktitle = "2nd Workshop on Logical Frameworks
and Meta-languages (LFM'00)",
year = 2000,
address = "Santa Barbara, California",
month = jun,
note = "Proceedings available as INRIA Technical Report",
keywords = "LF, Elf, linear",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/lfm00.pdf",
}
@TechReport{Polakow98tr,
author = "Jeff Polakow and Frank Pfenning",
title = "Ordered Linear Logic Programming",
institution = "Department of Computer Science, Carnegie Mellon University",
year = 1998,
number = "CMU-CS-98-183",
month = dec,
urlpdf = "http://www.cs.cmu.edu/~fp/papers/CMU-CS-98-183.pdf",
keywords = "LF, Elf, linear"
}
@InProceedings{Polakow99mfps,
author = "Jeff Polakow and Frank Pfenning",
title = "Relating Natural Deduction and Sequent Calculus for
Intuitionistic Non-Commutative Linear Logic",
editor = "Andre Scedrov and Achim Jung",
booktitle = "Proceedings of the 15th Conference on Mathematical
Foundations of Programming Semantics",
pages = "449--466",
year = 1999,
address = "New Orleans, Louisiana",
month = apr,
note = "Electronic Notes in Theoretical Computer Science, Volume 20",
keywords = "LF, Elf, linear",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/mfps99.pdf",
}
@InProceedings{Polakow99tlca,
author = "Jeff Polakow and Frank Pfenning",
title = "Natural Deduction for Intuitionistic Non-Commutative
Linear Logic",
editor = "J.-Y. Girard",
booktitle = "Proceedings of the 4th International Conference on
Typed Lambda Calculi and Applications (TLCA'99)",
year = 1999,
publisher = "Springer-Verlag LNCS 1581",
address = "L'Aquila, Italy",
month = apr,
pages = "295--309",
keywords = "LF, Elf, linear",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/tlca99.pdf",
}
@InProceedings{Reed07m4m,
author = {Jason Reed and Frank Pfenning},
title = {Intuitionistic Letcc via Labelled Deduction},
booktitle = {Proceedings of the 5th Workshop on Methods for Modalities (M4M5 2007)},
pages = {91-111},
year = 2007,
address = {Cachan, France},
month = nov,
note = {Electronic Notes in Theoretical Computer Science (ENTCS), vol 213, March 2009},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/m4m07.pdf}
}
@Unpublished{Reed10un,
author = {Jason C. Reed and Frank Pfenning},
title = {Focus-Preserving Embeddings of Substructural Logics in Intuitionistic Logic},
note = {Unpublished Manuscript},
month = jan,
year = 2010,
urlpdf = {http://www.cs.cmu.edu/~fp/papers/substruct10.pdf}
}
@InProceedings{Rohwedder96esop,
author = "Ekkehard Rohwedder and Frank Pfenning",
title = "Mode and Termination Checking for Higher-Order Logic
Programs",
editor = "Hanne Riis Nielson",
booktitle = "Proceedings of the European Symposium on Programming",
year = 1996,
publisher = "Springer-Verlag LNCS 1058",
address = "Link{\"o}ping, Sweden",
month = apr,
pages = "296--310",
keywords = "LF, Elf",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/esop96.pdf",
}
@InProceedings{Saranli07icra,
author = {Ulu{\c{c}} Saranli and Frank Pfenning},
title = {Using Constrained Intuitionistic Linear Logic for
Hybrid Robotic Planning Problems},
booktitle = {Proceedings of the International Conference on Robotics
and Automation (ICRA'07)},
pages = {3705--3710},
year = 2007,
address = {Rome Italy},
month = apr,
publisher = {IEEE Computer Society Press},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/icra07.pdf}
}
@Article{Schurmann01tcs,
author = "Carsten Sch{\"u}rmann and Jo{\"e}lle Despeyroux and
Frank Pfenning",
title = "Primitive Recursion for Higher-Order Abstract Syntax",
journal = "Theoretical Computer Science",
year = 2001,
volume = 266,
pages = "1--57",
keywords = "LF, misc"
}
@InProceedings{Schurmann03tphols,
author = {Carsten Sch{\"u}rmann and Frank Pfenning},
title = {A Coverage Checking Algorithm for {LF}},
booktitle = {Proceedings of the 16th International Conference on
Theorem Proving in Higher Order Logics (TPHOLs 2003)},
pages = {120--135},
year = 2003,
editor = {D. Basin and B. Wolff},
address = {Rome, Italy},
month = sep,
publisher = {Springer-Verlag LNCS 2758},
keywords = {LF, Elf},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/tphols03.pdf},
}
@InProceedings{Schurmann98cade,
author = "Carsten Sch{\"u}rmann and Frank Pfenning",
title = "Automated Theorem Proving in a Simple Meta-Logic for {LF}",
editor = "Claude Kirchner and H{\'e}l{\`e}ne Kirchner",
pages = "286--300",
booktitle = "Proceedings of the 15th International Conference on
Automated Deduction (CADE-15)",
year = 1998,
publisher = "Springer-Verlag LNCS 1421",
address = "Lindau, Germany",
month = jul,
keywords = "LF, Elf",
urlpdf = "http://www.cs.cmu.edu/~fp/papers/cade98m2.pdf",
}
@InProceedings{Simmons08icalp,
author = {Robert J. Simmons and Frank Pfenning},
title = {Linear Logical Algorithms},
booktitle = {Proceedings of the 35th International Colloquium
on Automata, Languages and Programming (ICALP'08)},
pages = {336--345},
year = 2008,
address = {Reykjavik, Iceland},
month = jul,
publisher = {Springer LNCS 5126},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/icalp08.pdf}
}
@InProceedings{Simmons09pepm,
author = {Robert J. Simmons and Frank Pfenning},
title = {Linear Logical Approximations},
booktitle = {Proceedings of the Workshop on Partial Evaluation and
Program Manipulation},
pages = {9--20},
year = {2009},
editor = {G. Puebla and G. Vidal},
address = {Savannah, Georgia},
month = jan,
organization = {ACM SIGPLAN},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/pepm09.pdf}
}
@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}
}
@TechReport{Watkins02tr,
author = {Kevin Watkins and Iliano Cervesato and Frank Pfenning
and David Walker},
title = {A Concurrent Logical Framework {I}: Judgments and Properties},
institution = {Department of Computer Science, Carnegie Mellon University},
year = 2002,
number = {CMU-CS-02-101},
note = {Revised May 2003},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/CMU-CS-02-101.pdf}
}
@InProceedings{Watkins04lfm,
author = {Kevin Watkins and Iliano Cervesato and Frank Pfenning and
David Walker},
title = {Specifying Properties of Concurrent Computations in {CLF}},
booktitle = {Proceedings of the 4th International Workshop on Logical
Frameworks and Meta-Languages (LFM'04)},
year = 2004,
editor = {C.Sch{\"u}rmann},
address = {Cork, Ireland},
month = jul,
publisher = {Electronic Notes in Theoretical Computer Science (ENTCS), vol 199, pp. 133--145, 2008},
keywords = {LF, Elf, linear},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/lfm04.pdf},
}
@InCollection{Watkins04types,
author = {Kevin Watkins and Iliano Cervesato and Frank Pfenning and
David Walker},
title = {A Concurrent Logical Framework: The Propositional Fragment},
booktitle = {Types for Proofs and Programs},
pages = {355--377},
publisher = {Springer-Verlag LNCS 3085},
year = 2004,
editor = {S. Berardi and M. Coppo and F. Damiani},
note = {Revised selected papers from the {\em Third International Workshop on Types for Proofs and Programs},
Torino, Italy, April 2003.},
keywords = {LF, linear},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/types03.pdf},
}
@InProceedings{Wickline98pldi,
author = "Philip Wickline and Peter Lee and Frank Pfenning",
title = "Run-time Code Generation and Modal-{ML}",
editor = "Keith D. Cooper",
pages = "224--235",
booktitle = "Proceedings of the Conference on Programming Language
Design and Implementation (PLDI'98)",
year = 1998,
publisher = "ACM Press",
address = "Montreal, Canada",
month = jun,
urlpdf = "http://www.cs.cmu.edu/~fp/papers/pldi98ccam.pdf",
keywords = "staged, fp"
}
@Article{Wickline98surveys,
author = "Philip Wickline and Peter Lee and Frank Pfenning and
Rowan Davies",
title = "Modal Types as Staging Specifications for Run-Time
Code Generation",
journal = "ACM Computing Surveys",
volume = 30,
number = "3es",
month = sep,
year = 1998,
urlpdf = "http://www.cs.cmu.edu/~fp/papers/sope98.pdf",
keywords = "staged, fp"
}
@InProceedings{Xi98pldi,
author = "Hongwei Xi and Frank Pfenning",
title = "Eliminating Array Bound Checking Through Dependent Types",
editor = "Keith D. Cooper",
pages = "249--257",
booktitle = "Proceedings of the Conference on Programming Language
Design and Implementation (PLDI'98)",
year = 1998,
publisher = "ACM Press",
address = "Montreal, Canada",
month = jun,
urlpdf = "http://www.cs.cmu.edu/~fp/papers/pldi98dml.pdf",
keywords = "fp"
}
@InProceedings{Xi99popl,
author = "Hongwei Xi and Frank Pfenning",
title = "Dependent Types in Practical Programming",
editor = "A. Aiken",
pages = "214--227",
booktitle = "Conference Record of the 26th Symposium on Principles of
Programming Languages (POPL'99)",
year = 1999,
publisher = "ACM Press",
month = jan,
urlpdf = "http://www.cs.cmu.edu/~fp/papers/popl99.pdf",
keywords = "fp"
}