@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/concur18.pdf}
}
@inproceedings{Balzer19esop,
author = {Stephanie Balzer and Bernardo Toninho and Frank Pfenning},
title = {Manifest Deadlock-Freedom for Shared Session Types},
booktitle = {28th European Symposium on Programming (ESOP 2019)},
year = 2019,
editor = {L. Caires},
pages = {611--639},
month = apr,
address = {Prague, Czech Republic},
publisher = {Springer LNCS 11423},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/esop19.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/tldi12.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{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}
}
@inproceedings{Caires19concur,
author = {Lu{\'\i}s Caires and Jorge A. P{\'e}rez and Frank Pfenning and Bernardo Toninho},
title = {Domain-Aware Session Types},
booktitle = {30th International Conference on Concurrency Theory (CONCUR 2019)},
year = 2019,
editor = {W. Fokkink andk R. van Glabbeek},
pages = {39:1--39:17},
month = aug,
address = {Amsterdam, The Netherlands},
publisher = {LIPIcs 140},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/concur19.pdf},
url = {http://arxiv.org/abs/1907.01318},
note = {Extended version at CoRR abs/1907.01318}
}
@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{Cervesato19un,
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 = jan,
year = 2019
}
@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}
}
@inproceedings{Chen23fossacs,
author = {Zhibo Chen and Frank Pfenning},
title = {A Logical Framework with Higher-Order Rational (Circular) Terms},
booktitle = {26th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2023)},
year = 2023,
editor = {O. Kupferman and P. Sobocinski},
pages = {68--88},
month = apr,
address = {Paris, France},
publisher = {Springer LNCS 13992},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/fossacs23.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 2018)},
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 2018)},
editor = {A. Dawar and E. Gr\"adel},
pages = {305--314},
month = jul,
address = {Oxford, UK},
year = {2018},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/lics18.pdf}
}
@inproceedings{Das20concur,
author = {Ankush Das and Frank Pfenning},
title = {Session Types with Arithmetic Refinements},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
year = 2020,
editor = {I. Konnov and L. Kov{\'a}cs},
pages = {13:1--13:18},
month = sep,
address = {Vienna, Austria},
publisher = {LIPIcs 171},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/concur20.pdf}
}
@inproceedings{Das20fscd,
author = {Ankush Das and Frank Pfenning},
title = {Rast: Resource-Aware Session Types with Arithmetic Refinements},
booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
year = 2020,
editor = {Z. Ariola},
pages = {33:1--33:17},
month = jun,
publisher = {LIPIcs 167},
note = {System description},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/fscd20b.pdf}
}
@inproceedings{Das20ppdp,
author = {Ankush Das and Frank Pfenning},
title = {Verified Linear Session-Typed Concurrent Programming},
booktitle = {22nd International Symposium on Principles
and Practice of Declarative Programming (PPDP 2020)},
year = 2020,
pages = {7:1--7:15},
month = sep,
address = {Bologna, Italy},
organization = {ACM},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/ppdp20.pdf}
}
@article{Das21arxiv,
author = {Ankush Das and Henry DeYoung and Andreia Mordido and Frank Pfenning},
title = {Subtyping on Nested Polymorphic Session Types},
journal = {CoRR},
year = 2021,
volume = {abs/2103.15193},
month = mar,
url = {https://arxiv.org/abs/2103.15193},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/arxiv21.pdf},
archiveprefix = {arXiv}
}
@inproceedings{Das21csf,
author = {Ankush Das and Stephanie Balzer and Jan Hoffmann and Frank Pfenning
and Ishani Santurkar},
title = {Resource-Aware Session Types for Digital Contracts},
booktitle = {34th Computer Security Foundations Symposium (CSF 2021)},
year = 2021,
editor = {R. K{\"u}sters and D. Naumann},
pages = {1--16},
month = jun,
address = {Dubrovnik, Croatia},
organization = {IEEE},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/csf21.pdf}
}
@inproceedings{Das21esop,
author = {Ankush Das and Henry DeYoung and Andreia Mordido and Frank Pfenning},
title = {Nested Session Types},
booktitle = {30th European Symposium on Programming},
year = {2021},
editor = {N. Yoshida},
optpages = {178--206},
month = mar,
address = {Luxembourg, Luxembourg},
publisher = {Springer LNCS},
note = {Extended version available as arXiv:2010.06482},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/esop21.pdf},
url = {http://www.cs.cmu.edu/~fp/papers/esop21extd.pdf}
}
@article{Das22lmcs,
author = {Ankush Das and Frank Pfenning},
title = {Rast: A Language for Resource-Aware Session Types},
journal = {Logical Methods in Computer Science},
year = 2022,
volume = 18,
number = 1,
pages = {9:1--9:36},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/lmcs22a.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.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{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 Annual Conference on Computer
Science Logic (CSL 2012)},
pages = {228--242},
year = 2012,
editor = {P. C{\'e}gielski and A. Durand},
address = {Fontainebleau, France},
month = sep,
publisher = {LIPIcs 16},
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{DeYoung20fscd,
author = {Henry DeYoung and Frank Pfenning and Klaas Pruiksma},
title = {Semi-Axiomatic Sequent Calculus},
booktitle = {5th International Conference on Formal Structures for Computation
and Deduction (FSCD 2020)},
year = 2020,
editor = {Z. Ariola},
pages = {29:1--29:22},
month = jun,
address = {Paris, France},
publisher = {LIPIcs 167},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/fscd20a.pdf}
}
@inproceedings{DeYoung22mfps,
author = {Henry DeYoung and Frank Pfenning},
title = {Data Layout from a Type-Theoretic Perspective},
booktitle = {38th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2022)},
year = 2022,
publisher = {Electronic Notes in Theoretical Informatics and Computer Science 1},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/mfps22.pdf},
url = {https://arxiv.org/abs/2212.06321v6},
note = {Invited paper. Extended version available at \url{https://arxiv.org/abs/2212.06321v3.pdf}}
}
@article{DeYoung23arxiv,
author = {Henry DeYoung and Andreia Mordido and Frank Pfenning and Ankush Das},
title = {Parametric Subtyping for Structural Parametric Polymorphism},
journal = {CoRR},
year = 2023,
volume = {abs/2307.13661},
month = jul,
url = {https://arxiv.org/abs/2307.13661},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/paramsubtp23.pdf},
note = {Submitted},
archiveprefix = {arXiv}
}
@article{Derakhshan20arxiv,
author = {Farzaneh Derakhshan and Frank Pfenning},
title = {Circular Proofs in First-Order Linear Logic with Least and Greatest Fixed Points},
journal = {CoRR},
year = 2020,
volume = {abs/2001.05132},
month = jan,
urlpdf = {http://www.cs.cmu.edu/~fp/papers/progress20.pdf},
url = {http://arxiv.org/abs/2001.05132}
}
@article{Derakhshan22lmcs,
author = {Farzaneh Derakhshan and Frank Pfenning},
title = {Circular Proofs as Session-Typed Processes: A Local Validity Condition},
journal = {Logical Methods in Computer Science},
year = 2022,
volume = 18,
number = 2,
pages = {8:1--8:51},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/lmcs22b.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{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/papers/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 = {Jana 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 = {Jana 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}
}
@article{Gommerstadt22jlamp,
author = {Hannah Gommerstadt and Limin Jia and Frank Pfenning},
title = {Session-Typed Concurrent Contracts},
journal = {Journal of Logical and Algebraic Methods in Programming},
year = 2022,
volume = 124,
number = 100731,
month = jan,
urlpdf = {http://www.cs.cmu.edu/~fp/papers/jlamp22.pdf},
note = {Special issue on \emph{Programming Language Approaches to Concurrency and Communication-Centric Software} (PLACES 2020)}
}
@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{Lakhani22esop,
author = {Zeeshan Lakhani and Ankush Das and Henry DeYoung and Andreia Mordido and Frank Pfenning},
title = {Polarized Subtyping},
booktitle = {31st European Symposium on Programming (ESOP 2022)},
year = 2022,
editor = {Ilya Sergey},
pages = {431--461},
month = apr,
address = {Munich, Germany},
publisher = {Springer LNCS 13240},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/esop22.pdf}
}
@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}
}
@unpublished{Mclaughlin10un,
author = {Sean McLaughlin and Frank Pfenning},
title = {The Focused Constraint Inverse Method for Intuitionistic Modal Logics},
note = {Draft manuscript},
month = jan,
year = 2010,
urlpdf = {http://www.cs.cmu.edu/~fp/papers/inviml10.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 = {https://dtai.cs.kuleuven.be/projects/ALP/newsletter/may01/}
}
@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{Pfenning23coordination,
author = {Frank Pfenning and Klaas Pruiksma},
title = {Relating Message Passing and Shared Memory, Proof-Theoretically},
booktitle = {25th International Conference on Coordination Models and Languages (COORDINATION 2023)},
year = 2023,
editor = {S. Jongmans and A. Lopes},
pages = {3--27},
month = jun,
address = {Lisbon, Portugal},
publisher = {Springer LNCS 13908},
note = {Notes to an invited talk},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/coordination23.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{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{Pruiksma19places,
author = {Klaas Pruiksma and Frank Pfenning},
title = {A Message-Passing Interpretation of Adjoint Logic},
booktitle = {Workshop on Programming Language Approaches to Concurrency and Communication-Centric Software (PLACES)},
year = 2019,
editor = {F. Martins and D. Orchard},
pages = {60--79},
month = apr,
address = {Prague, Czech Republic},
publisher = {EPTCS 291},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/places19.pdf}
}
@article{Pruiksma21jlamp,
author = {Klaas Pruiksma and Frank Pfenning},
title = {A Message-Passing Interpretation of Adjoint Logic},
journal = {Journal of Logical and Algebraic Methods in Programming},
year = 2021,
volume = 120,
number = 100637,
urlpdf = {http://www.cs.cmu.edu/~fp/papers/jlamp21.pdf}
}
@article{Pruiksma22jfp,
author = {Klaas Pruiksma and Frank Pfenning},
title = {Back to Futures},
journal = {Journal of Functional Programming},
year = 2022,
volume = 32,
pages = {e6},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/jfp22.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,
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{Sa23ppdp,
author = {Luiz de S{\'a} and Bernardo Toninho and Frank Pfenning},
title = {Intuitionistic Metric Temporal Logic},
optcrossref = {},
optkey = {},
booktitle = {25th International Symposium on Principles and Practice of Declarative Programming (PPDP 2023)},
year = 2023,
editor = {S. Escobar},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = oct,
address = {Cascais, Portugal},
optorganization = {},
optpublisher = {},
note = {To appear},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/ppdp23.pdf},
optannote = {}
}
@inproceedings{Sano21coordination,
author = {Chuta Sano and Stephanie Balzer and Frank Pfenning},
title = {Manifestly Phased Communication via Shared Session Types},
booktitle = {23rd International Conference on Coordination Models and Languages (COORDINATION 2021)},
year = 2021,
editor = {F. Damiani and O. Dardha},
pages = {23--40},
month = jun,
address = {Valletta, Malta},
publisher = {Springer LNCS 12717},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/coordination21.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{Somayyajula23mfps,
author = {Siva Somayyajula and Frank Pfenning},
title = {Dependent Type Refinements for Futures},
booktitle = {39th International Conference on Mathematical Foundations of Programming Semantics (MFPS 2023)},
year = 2023,
editor = {M. Kerjean and P. Levy},
month = jun,
address = {Bloomington, Indiana, USA},
note = {Preliminary version},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/mfps23.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/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}
}
@inproceedings{Toninho21ppdp,
author = {Bernardo Toninho and Lu{\'\i}s Caires and Frank Pfenning},
title = {A Decade of Dependent Session Types},
booktitle = {23rd International Symposium on Principles and Practice of Declarative Programming (PPDP 2021)},
year = 2021,
editor = {N. Veltri and N. Benton and S. Ghilezan},
pages = {3:1--3:3},
month = sep,
address = {Tallinn, Estonia},
organization = {ACM},
urlpdf = {http://www.cs.cmu.edu/~fp/papers/ppdp21.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.