@inproceedings{CervesatoP97,
  title = {Linear Higher-Order Pre-Unification},
  author = {Iliano Cervesato and Frank Pfenning},
  year = {1997},
  url = {http://www.computer.org/proceedings/lics/7925/79250422abs.htm},
  researchr = {https://researchr.org/publication/CervesatoP97},
  cites = {0},
  citedby = {0},
  pages = {422-433},
  booktitle = {lics},
}

@inproceedings{PfenningE88,
  title = {Higher-Order Abstract Syntax},
  author = {Frank Pfenning and Conal Elliott},
  year = {1988},
  doi = {10.1145/960116.54010},
  url = {https://doi.org/10.1145/960116.54010},
  tags = {abstract syntax},
  researchr = {https://researchr.org/publication/PfenningE88},
  cites = {0},
  citedby = {0},
  pages = {199-208},
  booktitle = {PLDI},
}

@inproceedings{MorgensternGP11,
  title = {A Proof-Carrying File System with Revocable and Use-Once Certificates},
  author = {Jamie Morgenstern and Deepak Garg and Frank Pfenning},
  year = {2011},
  doi = {10.1007/978-3-642-29963-6_5},
  url = {http://dx.doi.org/10.1007/978-3-642-29963-6_5},
  researchr = {https://researchr.org/publication/MorgensternGP11},
  cites = {0},
  citedby = {0},
  pages = {40-55},
  booktitle = {STM},
}

@inproceedings{PientkaP03,
  title = {Optimizing Higher-Order Pattern Unification},
  author = {Brigitte Pientka and Frank Pfenning},
  year = {2003},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2741&spage=473},
  tags = {optimization},
  researchr = {https://researchr.org/publication/PientkaP03},
  cites = {0},
  citedby = {0},
  pages = {473-487},
  booktitle = {cade},
}

@article{SimmonsP11,
  title = {Logical approximation for program analysis},
  author = {Robert J. Simmons and Frank Pfenning},
  year = {2011},
  doi = {10.1007/s10990-011-9071-2},
  url = {http://dx.doi.org/10.1007/s10990-011-9071-2},
  researchr = {https://researchr.org/publication/SimmonsP11},
  cites = {0},
  citedby = {0},
  journal = {lisp},
  volume = {24},
  number = {1-2},
  pages = {41-80},
}

@inproceedings{DietzenP91,
  title = {A Declarative Alternative to  Assert  in Logic Programming},
  author = {Scott Dietzen and Frank Pfenning},
  year = {1991},
  tags = {logic programming, programming, logic},
  researchr = {https://researchr.org/publication/DietzenP91},
  cites = {0},
  citedby = {0},
  pages = {372-386},
  booktitle = {SLP},
}

@inproceedings{NarendranPS93,
  title = {On the Unification Problem for Cartesian Closed Categories},
  author = {Paliath Narendran and Frank Pfenning and Richard Statman},
  year = {1993},
  researchr = {https://researchr.org/publication/NarendranPS93},
  cites = {0},
  citedby = {0},
  pages = {57-63},
  booktitle = {lics},
}

@article{NarendranPS97,
  title = {On the Unification Problem for Cartesian Closed Categories},
  author = {Paliath Narendran and Frank Pfenning and Richard Statman},
  year = {1997},
  researchr = {https://researchr.org/publication/NarendranPS97},
  cites = {0},
  citedby = {0},
  journal = {JSYML},
  volume = {62},
  number = {2},
  pages = {636-647},
}

@inproceedings{MichaylovP91,
  title = {Natural Semantics and Some of Its Meta-Theory in Elf},
  author = {Spiro Michaylov and Frank Pfenning},
  year = {1991},
  tags = {semantics, meta-model, Meta-Environment, meta-objects},
  researchr = {https://researchr.org/publication/MichaylovP91},
  cites = {0},
  citedby = {0},
  pages = {299-344},
  booktitle = {elp},
}

@article{GargP12,
  title = {Stateful authorization logic - Proof theory and a case study},
  author = {Deepak Garg and Frank Pfenning},
  year = {2012},
  doi = {10.3233/JCS-2012-0456},
  url = {http://dx.doi.org/10.3233/JCS-2012-0456},
  researchr = {https://researchr.org/publication/GargP12},
  cites = {0},
  citedby = {0},
  journal = {jcs},
  volume = {20},
  number = {4},
  pages = {353-391},
}

@inproceedings{FeltyGMP90,
  title = {Tutorial on Lambda-Prolog},
  author = {Amy P. Felty and Elsa L. Gunter and Dale Miller and Frank Pfenning},
  year = {1990},
  tags = {Prolog},
  researchr = {https://researchr.org/publication/FeltyGMP90},
  cites = {0},
  citedby = {0},
  pages = {682},
  booktitle = {cade},
}

@inproceedings{PfenningS99,
  title = {System Description: Twelf - A Meta-Logical Framework for Deductive Systems},
  author = {Frank Pfenning and Carsten Schürmann},
  year = {1999},
  url = {http://link.springer.de/link/service/series/0558/bibs/1632/16320202.htm},
  tags = {meta-model, Meta-Environment, meta-objects},
  researchr = {https://researchr.org/publication/PfenningS99},
  cites = {0},
  citedby = {0},
  pages = {202-206},
  booktitle = {cade},
}

@inproceedings{SimmonsP08,
  title = {Linear Logical Algorithms},
  author = {Robert J. Simmons and Frank Pfenning},
  year = {2008},
  doi = {10.1007/978-3-540-70583-3_28},
  url = {http://dx.doi.org/10.1007/978-3-540-70583-3_28},
  researchr = {https://researchr.org/publication/SimmonsP08},
  cites = {0},
  citedby = {0},
  pages = {336-347},
  booktitle = {icalp},
}

@article{ParkPT08,
  title = {A probabilistic language based on sampling functions},
  author = {Sungwoo Park and Frank Pfenning and Sebastian Thrun},
  year = {2008},
  doi = {10.1145/1452044.1452048},
  url = {http://doi.acm.org/10.1145/1452044.1452048},
  tags = {rule-based},
  researchr = {https://researchr.org/publication/ParkPT08},
  cites = {0},
  citedby = {0},
  journal = {TOPLAS},
  volume = {31},
  number = {1},
}

@inproceedings{Pfenning05,
  title = {Towards a type theory of contexts},
  author = {Frank Pfenning},
  year = {2005},
  doi = {10.1145/1088454.1088455},
  url = {http://doi.acm.org/10.1145/1088454.1088455},
  tags = {context-aware, type theory},
  researchr = {https://researchr.org/publication/Pfenning05},
  cites = {0},
  citedby = {0},
  pages = {1},
  booktitle = {ICFP},
}

@incollection{Pfenning01,
  title = {Logical Frameworks},
  author = {Frank Pfenning},
  year = {2001},
  researchr = {https://researchr.org/publication/Pfenning01},
  cites = {0},
  citedby = {0},
  pages = {1063-1147},
  booktitle = {Handbook of Automated Reasoning (in 2 volumes)},
  editor = {John Alan Robinson and Andrei Voronkov},
  publisher = {Elsevier and MIT Press},
  isbn = {0-444-50813-9},
}

@article{PerezCPT14,
  title = {Linear logical relations and observational equivalences for session-based concurrency},
  author = {Jorge A. Pérez and Luís Caires and Frank Pfenning and Bernardo Toninho},
  year = {2014},
  doi = {10.1016/j.ic.2014.08.001},
  url = {http://dx.doi.org/10.1016/j.ic.2014.08.001},
  researchr = {https://researchr.org/publication/PerezCPT14},
  cites = {0},
  citedby = {0},
  journal = {iandc},
  volume = {239},
  pages = {254-302},
}

@inproceedings{MichaylovP91:0,
  title = {Compiling the Polymorphic Lambda-Calculus},
  author = {Spiro Michaylov and Frank Pfenning},
  year = {1991},
  tags = {compiler},
  researchr = {https://researchr.org/publication/MichaylovP91%3A0},
  cites = {0},
  citedby = {0},
  pages = {285-296},
  booktitle = {PEPM},
}

@article{MomiglianoP03:0,
  title = {Higher-order pattern complement and the strict lambda-calculus},
  author = {Alberto Momigliano and Frank Pfenning},
  year = {2003},
  doi = {10.1145/937555.937559},
  url = {http://doi.acm.org/10.1145/937555.937559},
  researchr = {https://researchr.org/publication/MomiglianoP03%3A0},
  cites = {0},
  citedby = {0},
  journal = {tocl},
  volume = {4},
  number = {4},
  pages = {493-529},
}

@inproceedings{Pfenning88,
  title = {Single Axioms in the Implicational Propositional Calculus},
  author = {Frank Pfenning},
  year = {1988},
  researchr = {https://researchr.org/publication/Pfenning88},
  cites = {0},
  citedby = {0},
  pages = {710-713},
  booktitle = {cade},
}

@article{LovasP08,
  title = {A Bidirectional Refinement Type System for LF},
  author = {William Lovas and Frank Pfenning},
  year = {2008},
  doi = {10.1016/j.entcs.2007.09.021},
  url = {http://dx.doi.org/10.1016/j.entcs.2007.09.021},
  tags = {refinement, type system},
  researchr = {https://researchr.org/publication/LovasP08},
  cites = {0},
  citedby = {0},
  journal = {ENTCS},
  volume = {196},
  pages = {113-128},
}

@inproceedings{DaviesP00,
  title = {Intersection types and computational effects},
  author = {Rowan Davies and Frank Pfenning},
  year = {2000},
  doi = {10.1145/351240.351259},
  url = {http://doi.acm.org/10.1145/351240.351259},
  researchr = {https://researchr.org/publication/DaviesP00},
  cites = {0},
  citedby = {0},
  pages = {198-208},
  booktitle = {ICFP},
}

@inproceedings{GargBBPR06,
  title = {A Linear Logic of Authorization and Knowledge},
  author = {Deepak Garg and Lujo Bauer and Kevin D. Bowers and Frank Pfenning and Michael K. Reiter},
  year = {2006},
  doi = {10.1007/11863908_19},
  url = {http://dx.doi.org/10.1007/11863908_19},
  tags = {logic},
  researchr = {https://researchr.org/publication/GargBBPR06},
  cites = {0},
  citedby = {0},
  pages = {297-312},
  booktitle = {esorics},
}

@inproceedings{GommerstadtJP18,
  title = {Session-Typed Concurrent Contracts},
  author = {Hannah Gommerstadt and Limin Jia and Frank Pfenning},
  year = {2018},
  doi = {10.1007/978-3-319-89884-1_27},
  url = {https://doi.org/10.1007/978-3-319-89884-1_27},
  researchr = {https://researchr.org/publication/GommerstadtJP18},
  cites = {0},
  citedby = {0},
  pages = {771-798},
  booktitle = {ESOP},
}

@inproceedings{Pfenning96,
  title = {The Practice of Logical Frameworks},
  author = {Frank Pfenning},
  year = {1996},
  researchr = {https://researchr.org/publication/Pfenning96},
  cites = {0},
  citedby = {0},
  pages = {119-134},
  booktitle = {caap},
}

@inproceedings{RohwedderP96,
  title = {Mode and Termination Checking for Higher-Order Logic Programs},
  author = {Ekkehard Rohwedder and Frank Pfenning},
  year = {1996},
  tags = {termination, logic programming, logic},
  researchr = {https://researchr.org/publication/RohwedderP96},
  cites = {0},
  citedby = {0},
  pages = {296-310},
  booktitle = {ESOP},
}

@inproceedings{GargP05,
  title = {Type-Directed Concurrency},
  author = {Deepak Garg and Frank Pfenning},
  year = {2005},
  doi = {10.1007/11539452_5},
  url = {http://dx.doi.org/10.1007/11539452_5},
  researchr = {https://researchr.org/publication/GargP05},
  cites = {0},
  citedby = {0},
  pages = {6-20},
  booktitle = {concur},
}

@inproceedings{Pfenning00,
  title = {Reasoning about Staged Computation},
  author = {Frank Pfenning},
  year = {2000},
  url = {http://link.springer.de/link/service/series/0558/bibs/1924/19240005.htm},
  tags = {staged computation},
  researchr = {https://researchr.org/publication/Pfenning00},
  cites = {0},
  citedby = {0},
  pages = {5-6},
  booktitle = {saig},
}

@inproceedings{LeePRS88,
  title = {The Ergo Support System: An Integrated Set of Tools for Prototyping Integrated Environments},
  author = {Peter Lee and Frank Pfenning and Gene Rollins and William L. Scherlis},
  year = {1988},
  tags = {Meta-Environment},
  researchr = {https://researchr.org/publication/LeePRS88},
  cites = {0},
  citedby = {0},
  pages = {25-34},
  booktitle = {SDE},
}

@inproceedings{MomiglianoP99,
  title = {The Relative Complement Problem for Higher-Order Patterns},
  author = {Alberto Momigliano and Frank Pfenning},
  year = {1999},
  researchr = {https://researchr.org/publication/MomiglianoP99},
  cites = {0},
  citedby = {0},
  pages = {497-512},
  booktitle = {agp},
}

@inproceedings{BalzerTP19,
  title = {Manifest Deadlock-Freedom for Shared Session Types},
  author = {Stephanie Balzer and Bernardo Toninho and Frank Pfenning},
  year = {2019},
  doi = {10.1007/978-3-030-17184-1_22},
  url = {https://doi.org/10.1007/978-3-030-17184-1_22},
  researchr = {https://researchr.org/publication/BalzerTP19},
  cites = {0},
  citedby = {0},
  pages = {611-639},
  booktitle = {ESOP},
}

@inproceedings{CairesPPT13,
  title = {Behavioral Polymorphism and Parametricity in Session-Based Communication},
  author = {Luís Caires and Jorge A. Pérez and Frank Pfenning and Bernardo Toninho},
  year = {2013},
  doi = {10.1007/978-3-642-37036-6_19},
  url = {http://dx.doi.org/10.1007/978-3-642-37036-6_19},
  researchr = {https://researchr.org/publication/CairesPPT13},
  cites = {0},
  citedby = {0},
  pages = {330-349},
  booktitle = {ESOP},
}

@inproceedings{Pfenning99,
  title = {Logical and Meta-Logical Frameworks (Abstract)},
  author = {Frank Pfenning},
  year = {1999},
  tags = {meta-model, Meta-Environment, meta-objects},
  researchr = {https://researchr.org/publication/Pfenning99},
  cites = {0},
  citedby = {0},
  pages = {206},
  booktitle = {ppdp},
}

@inproceedings{GargP10-0,
  title = {Stateful Authorization Logic: - Proof Theory and a Case Study},
  author = {Deepak Garg and Frank Pfenning},
  year = {2010},
  doi = {10.1007/978-3-642-22444-7_14},
  url = {http://dx.doi.org/10.1007/978-3-642-22444-7_14},
  researchr = {https://researchr.org/publication/GargP10-0},
  cites = {0},
  citedby = {0},
  pages = {210-225},
  booktitle = {STM},
}

@article{CervesatoHP00,
  title = {Efficient resource management for linear logic proof search},
  author = {Iliano Cervesato and Joshua S. Hodas and Frank Pfenning},
  year = {2000},
  doi = {10.1016/S0304-3975(99)00173-5},
  url = {http://dx.doi.org/10.1016/S0304-3975(99)00173-5},
  tags = {logic, search},
  researchr = {https://researchr.org/publication/CervesatoHP00},
  cites = {0},
  citedby = {0},
  journal = {TCS},
  volume = {232},
  number = {1-2},
  pages = {133-163},
}

@inproceedings{CairesP10,
  title = {Session Types as Intuitionistic Linear Propositions},
  author = {Luís Caires and Frank Pfenning},
  year = {2010},
  doi = {10.1007/978-3-642-15375-4_16},
  url = {http://dx.doi.org/10.1007/978-3-642-15375-4_16},
  researchr = {https://researchr.org/publication/CairesP10},
  cites = {0},
  citedby = {0},
  pages = {222-236},
  booktitle = {concur},
}

@inproceedings{PfenningS09,
  title = {Substructural Operational Semantics as Ordered Logic Programming},
  author = {Frank Pfenning and Robert J. Simmons},
  year = {2009},
  doi = {10.1109/LICS.2009.8},
  url = {http://dx.doi.org/10.1109/LICS.2009.8},
  tags = {semantics, logic programming, programming, operational semantics, logic},
  researchr = {https://researchr.org/publication/PfenningS09},
  cites = {0},
  citedby = {0},
  pages = {101-110},
  booktitle = {lics},
}

@inproceedings{VIICHP04,
  title = {A Symmetric Modal Lambda Calculus for Distributed Computing},
  author = {Tom Murphy VII and Karl Crary and Robert Harper and Frank Pfenning},
  year = {2004},
  url = {http://csdl.computer.org/comp/proceedings/lics/2004/2192/00/21920286abs.htm},
  researchr = {https://researchr.org/publication/VIICHP04},
  cites = {0},
  citedby = {0},
  pages = {286-295},
  booktitle = {lics},
}

@article{AndrewsBPBIX04,
  title = {ETPS: A System to Help Students Write Formal Proofs},
  author = {Peter B. Andrews and Chad E. Brown and Frank Pfenning and Matthew Bishop and Sunil Issar and Hongwei Xi},
  year = {2004},
  doi = {10.1023/B:JARS.0000021871.18776.94},
  url = {http://dx.doi.org/10.1023/B:JARS.0000021871.18776.94},
  researchr = {https://researchr.org/publication/AndrewsBPBIX04},
  cites = {0},
  citedby = {0},
  journal = {JAR},
  volume = {32},
  number = {1},
  pages = {75-92},
}

@inproceedings{MomiglianoP99:0,
  title = {The Relative Complement Problem for Higher-Order Patterns},
  author = {Alberto Momigliano and Frank Pfenning},
  year = {1999},
  researchr = {https://researchr.org/publication/MomiglianoP99%3A0},
  cites = {0},
  citedby = {0},
  pages = {380-394},
  booktitle = {ICLP},
}

@article{HarperP98,
  title = {A Module System for a Programming Language Based on the LF Logical Framework},
  author = {Robert Harper and Frank Pfenning},
  year = {1998},
  tags = {programming languages, rule-based, programming},
  researchr = {https://researchr.org/publication/HarperP98},
  cites = {0},
  citedby = {0},
  journal = {logcom},
  volume = {8},
  number = {1},
  pages = {5-31},
}

@article{AndrewsBINPX96,
  title = {TPS: A Theorem-Proving System for Classical Type Theory},
  author = {Peter B. Andrews and Matthew Bishop and Sunil Issar and Dan Nesmith and Frank Pfenning and Hongwei Xi},
  year = {1996},
  tags = {type system, type theory},
  researchr = {https://researchr.org/publication/AndrewsBINPX96},
  cites = {0},
  citedby = {0},
  journal = {JAR},
  volume = {16},
  number = {3},
  pages = {321-353},
}

@article{DietzenP92,
  title = {Higher-Order and Modal Logic as a Framework for Explanation-Based Generalization},
  author = {Scott Dietzen and Frank Pfenning},
  year = {1992},
  tags = {rule-based, modal logic, logic},
  researchr = {https://researchr.org/publication/DietzenP92},
  cites = {0},
  citedby = {0},
  journal = {ml},
  volume = {9},
  pages = {23-55},
}

@inproceedings{DaviesP96,
  title = {A Modal Analysis of Staged Computation},
  author = {Rowan Davies and Frank Pfenning},
  year = {1996},
  doi = {10.1145/237721.237788},
  url = {http://doi.acm.org/10.1145/237721.237788},
  tags = {analysis, staged computation},
  researchr = {https://researchr.org/publication/DaviesP96},
  cites = {0},
  citedby = {0},
  pages = {258-270},
  booktitle = {POPL},
}

@inproceedings{Pfenning15,
  title = {Proof theory and its role in programming language research},
  author = {Frank Pfenning},
  year = {2015},
  doi = {10.1145/2792434.2792438},
  url = {http://doi.acm.org/10.1145/2792434.2792438},
  researchr = {https://researchr.org/publication/Pfenning15},
  cites = {0},
  citedby = {0},
  pages = {4},
  booktitle = {POPL},
}

@inproceedings{SchurmannP98,
  title = {Automated Theorem Proving in a Simple Meta-Logic for LF},
  author = {Carsten Schürmann and Frank Pfenning},
  year = {1998},
  url = {http://link.springer.de/link/service/series/0558/bibs/1421/14210286.htm},
  tags = {meta-model, logic, Meta-Environment, meta-objects},
  researchr = {https://researchr.org/publication/SchurmannP98},
  cites = {0},
  citedby = {0},
  pages = {286-300},
  booktitle = {cade},
}

@inproceedings{Pfenning10,
  title = {Possession as Linear Knowledge},
  author = {Frank Pfenning},
  year = {2010},
  url = {http://www.easychair.org/publications/?page=73216885},
  researchr = {https://researchr.org/publication/Pfenning10},
  cites = {0},
  citedby = {0},
  pages = {1},
  booktitle = {lics},
}

@inproceedings{Pfenning89,
  title = {Elf: A Language for Logic Definition and Verified Metaprogramming},
  author = {Frank Pfenning},
  year = {1989},
  tags = {logic},
  researchr = {https://researchr.org/publication/Pfenning89},
  cites = {0},
  citedby = {0},
  pages = {313-322},
  booktitle = {lics},
}

@inproceedings{SchurmannP03,
  title = {A Coverage Checking Algorithm for LF},
  author = {Carsten Schürmann and Frank Pfenning},
  year = {2003},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2758&spage=120},
  tags = {coverage},
  researchr = {https://researchr.org/publication/SchurmannP03},
  cites = {0},
  citedby = {0},
  pages = {120-135},
  booktitle = {tphol},
}

@article{Pfenning93,
  title = {On the Undecidability of Partial Polymorphic Type Reconstruction},
  author = {Frank Pfenning},
  year = {1993},
  researchr = {https://researchr.org/publication/Pfenning93},
  cites = {0},
  citedby = {0},
  journal = {FUIN},
  volume = {19},
  number = {1/2},
  pages = {185-199},
}

@inproceedings{McLaughlinP08,
  title = {Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic},
  author = {Sean McLaughlin and Frank Pfenning},
  year = {2008},
  doi = {10.1007/978-3-540-89439-1_12},
  url = {http://dx.doi.org/10.1007/978-3-540-89439-1_12},
  tags = {logic},
  researchr = {https://researchr.org/publication/McLaughlinP08},
  cites = {0},
  citedby = {0},
  pages = {174-181},
  booktitle = {lpar},
}

@inproceedings{PfenningL89,
  title = {LEAP: A Language with Eval And Polymorphism},
  author = {Frank Pfenning and Peter Lee},
  year = {1989},
  researchr = {https://researchr.org/publication/PfenningL89},
  cites = {0},
  citedby = {0},
  pages = {345-359},
  booktitle = {tapsoft},
}

@inproceedings{ChaudhuriP05,
  title = {A Focusing Inverse Method Theorem Prover for First-Order Linear Logic},
  author = {Kaustuv Chaudhuri and Frank Pfenning},
  year = {2005},
  doi = {10.1007/11532231_6},
  url = {http://dx.doi.org/10.1007/11532231_6},
  tags = {logic},
  researchr = {https://researchr.org/publication/ChaudhuriP05},
  cites = {0},
  citedby = {0},
  pages = {69-83},
  booktitle = {cade},
}

@inproceedings{ParkPT05,
  title = {A probabilistic language based upon sampling functions},
  author = {Sungwoo Park and Frank Pfenning and Sebastian Thrun},
  year = {2005},
  doi = {10.1145/1040305.1040320},
  url = {http://doi.acm.org/10.1145/1040305.1040320},
  tags = {rule-based},
  researchr = {https://researchr.org/publication/ParkPT05},
  cites = {0},
  citedby = {0},
  pages = {171-182},
  booktitle = {POPL},
}

@inproceedings{ToninhoCP14,
  title = {Corecursion and Non-divergence in Session-Typed Processes},
  author = {Bernardo Toninho and Luís Caires and Frank Pfenning},
  year = {2014},
  doi = {10.1007/978-3-662-45917-1_11},
  url = {http://dx.doi.org/10.1007/978-3-662-45917-1_11},
  researchr = {https://researchr.org/publication/ToninhoCP14},
  cites = {0},
  citedby = {0},
  pages = {159-175},
  booktitle = {tgc},
}

@inproceedings{CervesatoP96,
  title = {A Linear Logical Framework},
  author = {Iliano Cervesato and Frank Pfenning},
  year = {1996},
  researchr = {https://researchr.org/publication/CervesatoP96},
  cites = {0},
  citedby = {0},
  pages = {264-275},
  booktitle = {lics},
}

@inproceedings{GargP06,
  title = {Non-Interference in Constructive Authorization Logic},
  author = {Deepak Garg and Frank Pfenning},
  year = {2006},
  doi = {10.1109/CSFW.2006.18},
  url = {http://doi.ieeecomputersociety.org/10.1109/CSFW.2006.18},
  tags = {logic},
  researchr = {https://researchr.org/publication/GargP06},
  cites = {0},
  citedby = {0},
  pages = {283-296},
  booktitle = {csfw},
}

@incollection{Pfenning92:5,
  title = {Dependent Types in Logic Programming},
  author = {Frank Pfenning},
  year = {1992},
  tags = {logic programming, programming, logic},
  researchr = {https://researchr.org/publication/Pfenning92%3A5},
  cites = {0},
  citedby = {0},
  pages = {285-311},
  booktitle = {Types in Logic Programming},
}

@inproceedings{Pfenning98,
  title = {Reasoning About Deductions in Linear Logic (Abstract of Invited Talk)},
  author = {Frank Pfenning},
  year = {1998},
  url = {http://link.springer.de/link/service/series/0558/bibs/1421/14210001.htm},
  tags = {logic},
  researchr = {https://researchr.org/publication/Pfenning98},
  cites = {0},
  citedby = {0},
  pages = {1-2},
  booktitle = {cade},
}

@article{PfenningD01,
  title = {A judgmental reconstruction of modal logic},
  author = {Frank Pfenning and Rowan Davies},
  year = {2001},
  tags = {modal logic, logic},
  researchr = {https://researchr.org/publication/PfenningD01},
  cites = {0},
  citedby = {0},
  journal = {mscs},
  volume = {11},
  number = {4},
  pages = {511-540},
}

@article{ColbyCHLP03,
  title = {Automated techniques for provably safe mobile code},
  author = {Christopher Colby and Karl Crary and Robert Harper and Peter Lee and Frank Pfenning},
  year = {2003},
  tags = {mobile code, mobile},
  researchr = {https://researchr.org/publication/ColbyCHLP03},
  cites = {0},
  citedby = {0},
  journal = {TCS},
  volume = {290},
  number = {2},
  pages = {1175-1199},
}

@inproceedings{AndrewsBINPX93,
  title = {TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory},
  author = {Peter B. Andrews and Matthew Bishop and Sunil Issar and Dan Nesmith and Frank Pfenning and Hongwei Xi},
  year = {1993},
  tags = {type theory},
  researchr = {https://researchr.org/publication/AndrewsBINPX93},
  cites = {0},
  citedby = {0},
  pages = {366-370},
  booktitle = {tphol},
}

@inproceedings{AndrewsINP90,
  title = {The TPS Theorem Proving System},
  author = {Peter B. Andrews and Sunil Issar and Dan Nesmith and Frank Pfenning},
  year = {1990},
  researchr = {https://researchr.org/publication/AndrewsINP90},
  cites = {0},
  citedby = {0},
  pages = {641-642},
  booktitle = {cade},
}

@inproceedings{SimmonsP09,
  title = {Linear logical approximations},
  author = {Robert J. Simmons and Frank Pfenning},
  year = {2009},
  doi = {10.1145/1480945.1480949},
  url = {http://doi.acm.org/10.1145/1480945.1480949},
  researchr = {https://researchr.org/publication/SimmonsP09},
  cites = {0},
  citedby = {0},
  pages = {9-20},
  booktitle = {PEPM},
}

@inproceedings{DeYoungGP08,
  title = {An Authorization Logic With Explicit Time},
  author = {Henry DeYoung and Deepak Garg and Frank Pfenning},
  year = {2008},
  doi = {10.1109/CSF.2008.15},
  url = {http://doi.ieeecomputersociety.org/10.1109/CSF.2008.15},
  tags = {logic},
  researchr = {https://researchr.org/publication/DeYoungGP08},
  cites = {0},
  citedby = {0},
  pages = {133-145},
  booktitle = {csfw},
}

@inproceedings{AndrewsINP88,
  title = {The TPS Theorem Proving System},
  author = {Peter B. Andrews and Sunil Issar and Daniel Nesmith and Frank Pfenning},
  year = {1988},
  researchr = {https://researchr.org/publication/AndrewsINP88},
  cites = {0},
  citedby = {0},
  pages = {760-761},
  booktitle = {cade},
}

@article{ChaudhuriPP08,
  title = {A Logical Characterization of Forward and Backward Chaining in the Inverse Method},
  author = {Kaustuv Chaudhuri and Frank Pfenning and Greg Price},
  year = {2008},
  doi = {10.1007/s10817-007-9091-0},
  url = {http://dx.doi.org/10.1007/s10817-007-9091-0},
  researchr = {https://researchr.org/publication/ChaudhuriPP08},
  cites = {0},
  citedby = {0},
  journal = {JAR},
  volume = {40},
  number = {2-3},
  pages = {133-177},
}

@inproceedings{Pfenning95,
  title = {Structural Cut Elimination},
  author = {Frank Pfenning},
  year = {1995},
  researchr = {https://researchr.org/publication/Pfenning95},
  cites = {0},
  citedby = {0},
  pages = {156-166},
  booktitle = {lics},
}

@inproceedings{BalzerP15,
  title = {Objects as session-typed processes},
  author = {Stephanie Balzer and Frank Pfenning},
  year = {2015},
  doi = {10.1145/2824815.2824817},
  url = {http://doi.acm.org/10.1145/2824815.2824817},
  researchr = {https://researchr.org/publication/BalzerP15},
  cites = {0},
  citedby = {0},
  pages = {13-24},
  booktitle = {agere},
}

@article{Das0P18-0,
  title = {Parallel complexity analysis with temporal session types},
  author = {Ankush Das and Jan Hoffmann 0002 and Frank Pfenning},
  year = {2018},
  doi = {10.1145/3236786},
  url = {https://doi.org/10.1145/3236786},
  researchr = {https://researchr.org/publication/Das0P18-0},
  cites = {0},
  citedby = {0},
  journal = {PACMPL},
  volume = {2},
  number = {ICFP},
}

@article{MillerNPS91,
  title = {Uniform Proofs as a Foundation for Logic Programming},
  author = {Dale Miller and Gopalan Nadathur and Frank Pfenning and Andre Scedrov},
  year = {1991},
  tags = {logic programming, programming, logic},
  researchr = {https://researchr.org/publication/MillerNPS91},
  cites = {0},
  citedby = {0},
  journal = {APAL},
  volume = {51},
  number = {1-2},
  pages = {125-157},
}

@article{BalzerP17,
  title = {Manifest sharing with session types},
  author = {Stephanie Balzer and Frank Pfenning},
  year = {2017},
  doi = {10.1145/3110281},
  url = {http://doi.acm.org/10.1145/3110281},
  researchr = {https://researchr.org/publication/BalzerP17},
  cites = {0},
  citedby = {0},
  journal = {PACMPL},
  volume = {1},
  number = {ICFP},
}

@inproceedings{PfenningH92,
  title = {Compiler Verification in LF},
  author = {John Hannan and Frank Pfenning},
  year = {1992},
  tags = {compiler},
  researchr = {https://researchr.org/publication/PfenningH92},
  cites = {0},
  citedby = {0},
  pages = {407-418},
  booktitle = {lics},
}

@article{CervesatoP03,
  title = {A Linear Spine Calculus},
  author = {Iliano Cervesato and Frank Pfenning},
  year = {2003},
  doi = {10.1093/logcom/13.5.639},
  url = {http://dx.doi.org/10.1093/logcom/13.5.639},
  researchr = {https://researchr.org/publication/CervesatoP03},
  cites = {0},
  citedby = {0},
  journal = {logcom},
  volume = {13},
  number = {5},
  pages = {639-688},
}

@inproceedings{XiP99,
  title = {Dependent Types in Practical Programming},
  author = {Hongwei Xi and Frank Pfenning},
  year = {1999},
  doi = {10.1145/292540.292560},
  url = {http://doi.acm.org/10.1145/292540.292560},
  tags = {programming},
  researchr = {https://researchr.org/publication/XiP99},
  cites = {0},
  citedby = {0},
  pages = {214-227},
  booktitle = {POPL},
}

@inproceedings{Pfenning91,
  title = {Unification and Anti-Unification in the Calculus of Constructions},
  author = {Frank Pfenning},
  year = {1991},
  researchr = {https://researchr.org/publication/Pfenning91},
  cites = {0},
  citedby = {0},
  pages = {74-85},
  booktitle = {lics},
}

@inproceedings{Pfenning90,
  title = {Types in Logic Programming},
  author = {Frank Pfenning},
  year = {1990},
  tags = {logic programming, programming, logic},
  researchr = {https://researchr.org/publication/Pfenning90},
  cites = {0},
  citedby = {0},
  pages = {786},
  booktitle = {ICLP},
}

@article{SiegP98,
  title = {Note by the Guest Editors},
  author = {Wilfried Sieg and Frank Pfenning},
  year = {1998},
  researchr = {https://researchr.org/publication/SiegP98},
  cites = {0},
  citedby = {0},
  journal = {sLogica},
  volume = {60},
  number = {1},
  pages = {1},
}

@article{GramlichKP00,
  title = {Editorial: Strategies in Automated Deduction},
  author = {Bernhard Gramlich and Hélène Kirchner and Frank Pfenning},
  year = {2000},
  researchr = {https://researchr.org/publication/GramlichKP00},
  cites = {0},
  citedby = {0},
  journal = {AMAI},
  volume = {29},
  number = {1-4},
}

@inproceedings{BalzerPT18,
  title = {A Universal Session Type for Untyped Asynchronous Communication},
  author = {Stephanie Balzer and Frank Pfenning and Bernardo Toninho},
  year = {2018},
  doi = {10.4230/LIPIcs.CONCUR.2018.30},
  url = {https://doi.org/10.4230/LIPIcs.CONCUR.2018.30},
  researchr = {https://researchr.org/publication/BalzerPT18},
  cites = {0},
  citedby = {0},
  booktitle = {concur},
}

@article{CruzRGP14,
  title = {A Linear Logic Programming Language for Concurrent Programming over Graph Structures},
  author = {Flávio Cruz and Ricardo Rocha and Seth Copen Goldstein and Frank Pfenning},
  year = {2014},
  doi = {10.1017/S1471068414000167},
  url = {http://dx.doi.org/10.1017/S1471068414000167},
  researchr = {https://researchr.org/publication/CruzRGP14},
  cites = {0},
  citedby = {0},
  journal = {tplp},
  volume = {14},
  number = {4-5},
  pages = {493-507},
}

@inproceedings{BowersBGPR07,
  title = {Consumable Credentials in Linear-Logic-Based Access-Control Systems},
  author = {Kevin D. Bowers and Lujo Bauer and Deepak Garg and Frank Pfenning and Michael K. Reiter},
  year = {2007},
  url = {http://www.isoc.org/isoc/conferences/ndss/07/papers/consumable_credentials.pdf},
  tags = {control systems, rule-based, logic, access control, role-based access control},
  researchr = {https://researchr.org/publication/BowersBGPR07},
  cites = {0},
  citedby = {0},
  booktitle = {ndss},
}

@inproceedings{PfenningG15,
  title = {Polarized Substructural Session Types},
  author = {Frank Pfenning and Dennis Griffith},
  year = {2015},
  doi = {10.1007/978-3-662-46678-0_1},
  url = {http://dx.doi.org/10.1007/978-3-662-46678-0_1},
  researchr = {https://researchr.org/publication/PfenningG15},
  cites = {0},
  citedby = {0},
  pages = {3-22},
  booktitle = {fossacs},
}

@article{DanvyDP99,
  title = {On proving syntactic properties of CPS programs},
  author = {Olivier Danvy and Belmina Dzafic and Frank Pfenning},
  year = {1999},
  url = {http://www.elsevier.com/gej-ng/31/29/23/50/23/show/Products/notes/index.htt#003},
  researchr = {https://researchr.org/publication/DanvyDP99},
  cites = {0},
  citedby = {0},
  journal = {ENTCS},
  volume = {26},
  pages = {21-33},
}

@article{Pfenning14,
  title = {Programming with Higher-Order Logic, by Dale Miller and Gopalan Nadathur, Cambridge University Press, 2012, Hardcover, ISBN-10: 052187940X, xiv + 306 pp},
  author = {Frank Pfenning},
  year = {2014},
  doi = {10.1017/S1471068414000027},
  url = {http://dx.doi.org/10.1017/S1471068414000027},
  researchr = {https://researchr.org/publication/Pfenning14},
  cites = {0},
  citedby = {0},
  journal = {tplp},
  volume = {14},
  number = {2},
  pages = {265-267},
}

@inproceedings{Pfenning07,
  title = {On a Logical Foundation for Explicit Substitutions},
  author = {Frank Pfenning},
  year = {2007},
  doi = {10.1007/978-3-540-73449-9_3},
  url = {http://dx.doi.org/10.1007/978-3-540-73449-9_3},
  researchr = {https://researchr.org/publication/Pfenning07},
  cites = {0},
  citedby = {0},
  pages = {19},
  booktitle = {RTA},
}

@inproceedings{DowekHKP96,
  title = {Unification via Explicit Substitutions: The Case of Higher-Order Patterns},
  author = {Gilles Dowek and Thérèse Hardin and Claude Kirchner and Frank Pfenning},
  year = {1996},
  researchr = {https://researchr.org/publication/DowekHKP96},
  cites = {0},
  citedby = {0},
  pages = {259-273},
  booktitle = {ICLP},
}

@article{Pfenning00:0,
  title = {Structural Cut Elimination: I. Intuitionistic and Classical Logic},
  author = {Frank Pfenning},
  year = {2000},
  tags = {logic},
  researchr = {https://researchr.org/publication/Pfenning00%3A0},
  cites = {0},
  citedby = {0},
  journal = {iandc},
  volume = {157},
  number = {1-2},
  pages = {84-141},
}

@inproceedings{PetersenHCP03,
  title = {A type theory for memory allocation and data layout},
  author = {Leaf Petersen and Robert Harper and Karl Crary and Frank Pfenning},
  year = {2003},
  doi = {10.1145/640128.604147},
  url = {http://doi.acm.org/10.1145/640128.604147},
  tags = {layout, data-flow, type theory},
  researchr = {https://researchr.org/publication/PetersenHCP03},
  cites = {0},
  citedby = {0},
  pages = {172-184},
  booktitle = {POPL},
}

@inproceedings{CairesPT12,
  title = {Towards concurrent type theory},
  author = {Luís Caires and Frank Pfenning and Bernardo Toninho},
  year = {2012},
  doi = {10.1145/2103786.2103788},
  url = {http://doi.acm.org/10.1145/2103786.2103788},
  researchr = {https://researchr.org/publication/CairesPT12},
  cites = {0},
  citedby = {0},
  pages = {1-12},
  booktitle = {tldi},
}

@inproceedings{JiaGP16,
  title = {Monitors and blame assignment for higher-order session types},
  author = {Limin Jia and Hannah Gommerstadt and Frank Pfenning},
  year = {2016},
  doi = {10.1145/2837614.2837662},
  url = {http://doi.acm.org/10.1145/2837614.2837662},
  researchr = {https://researchr.org/publication/JiaGP16},
  cites = {0},
  citedby = {0},
  pages = {582-594},
  booktitle = {POPL},
}

@inproceedings{ToninhoCP12,
  title = {Functions as Session-Typed Processes},
  author = {Bernardo Toninho and Luís Caires and Frank Pfenning},
  year = {2012},
  doi = {10.1007/978-3-642-28729-9_23},
  url = {http://dx.doi.org/10.1007/978-3-642-28729-9_23},
  researchr = {https://researchr.org/publication/ToninhoCP12},
  cites = {0},
  citedby = {0},
  pages = {346-360},
  booktitle = {fossacs},
}

@inproceedings{WatkinsCPW03,
  title = {A Concurrent Logical Framework: The Propositional Fragment},
  author = {Kevin Watkins and Iliano Cervesato and Frank Pfenning and David Walker},
  year = {2003},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3085&spage=355},
  researchr = {https://researchr.org/publication/WatkinsCPW03},
  cites = {0},
  citedby = {0},
  pages = {355-377},
  booktitle = {TYPES},
}

@inproceedings{DespeyrouxPS97,
  title = {Primitive Recursion for Higher-Order Abstract Syntax},
  author = {Joëlle Despeyroux and Frank Pfenning and Carsten Schürmann},
  year = {1997},
  tags = {abstract syntax},
  researchr = {https://researchr.org/publication/DespeyrouxPS97},
  cites = {0},
  citedby = {0},
  pages = {147-163},
  booktitle = {tlca},
}

@inproceedings{ChangCDHLVP02,
  title = {Trustless Grid Computing in ConCert},
  author = {Bor-Yuh Evan Chang and Karl Crary and Margaret DeLap and Robert Harper and Jason Liszka and Tom Murphy VII and Frank Pfenning},
  year = {2002},
  url = {http://link.springer.de/link/service/series/0558/bibs/2536/25360112.htm},
  researchr = {https://researchr.org/publication/ChangCDHLVP02},
  cites = {0},
  citedby = {0},
  pages = {112-125},
  booktitle = {ccgrid},
}

@article{AbadiLP02,
  title = {Editorial},
  author = {Martín Abadi and Leonid Libkin and Frank Pfenning},
  year = {2002},
  doi = {10.1145/507382.507383},
  url = {http://doi.acm.org/10.1145/507382.507383},
  researchr = {https://researchr.org/publication/AbadiLP02},
  cites = {0},
  citedby = {0},
  journal = {tocl},
  volume = {3},
  number = {3},
  pages = {335},
}

@inproceedings{DunfieldP04,
  title = {Tridirectional typechecking},
  author = {Joshua Dunfield and Frank Pfenning},
  year = {2004},
  doi = {10.1145/964001.964025},
  url = {http://doi.acm.org/10.1145/964001.964025},
  researchr = {https://researchr.org/publication/DunfieldP04},
  cites = {0},
  citedby = {0},
  pages = {281-292},
  booktitle = {POPL},
}

@inproceedings{ChaudhuriPP06,
  title = {A Logical Characterization of Forward and Backward Chaining in the Inverse Method},
  author = {Kaustuv Chaudhuri and Frank Pfenning and Greg Price},
  year = {2006},
  doi = {10.1007/11814771_9},
  url = {http://dx.doi.org/10.1007/11814771_9},
  researchr = {https://researchr.org/publication/ChaudhuriPP06},
  cites = {0},
  citedby = {0},
  pages = {97-111},
  booktitle = {cade},
}

@article{DaviesP01,
  title = {A modal analysis of staged computation},
  author = {Rowan Davies and Frank Pfenning},
  year = {2001},
  doi = {10.1145/382780.382785},
  url = {http://doi.acm.org/10.1145/382780.382785},
  tags = {analysis, staged computation},
  researchr = {https://researchr.org/publication/DaviesP01},
  cites = {0},
  citedby = {0},
  journal = {JACM},
  volume = {48},
  number = {3},
  pages = {555-604},
}

@inproceedings{AndersonP04:0,
  title = {Verifying Uniqueness in a Logical Framework},
  author = {Penny Anderson and Frank Pfenning},
  year = {2004},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3223&spage=18},
  researchr = {https://researchr.org/publication/AndersonP04%3A0},
  cites = {0},
  citedby = {0},
  pages = {18-33},
  booktitle = {tphol},
}

@inproceedings{Pfenning94,
  title = {Elf: A Meta-Language for Deductive Systems (System Descrition)},
  author = {Frank Pfenning},
  year = {1994},
  tags = {meta-model, Meta-Environment, meta-objects},
  researchr = {https://researchr.org/publication/Pfenning94},
  cites = {0},
  citedby = {0},
  pages = {811-815},
  booktitle = {cade},
}

@incollection{NadathurP92,
  title = {The Type System of a Higher-Order Logic Programming Language},
  author = {Gopalan Nadathur and Frank Pfenning},
  year = {1992},
  tags = {programming languages, type system, logic programming, programming, logic},
  researchr = {https://researchr.org/publication/NadathurP92},
  cites = {0},
  citedby = {0},
  pages = {245-283},
  booktitle = {Types in Logic Programming},
}

@inproceedings{Pfenning00:1,
  title = {On the Logical Foundations of Staged Computation (Abstract of Invited Talk)},
  author = {Frank Pfenning},
  year = {2000},
  doi = {10.1145/328690.328696},
  url = {http://doi.acm.org/10.1145/328690.328696},
  tags = {staged computation},
  researchr = {https://researchr.org/publication/Pfenning00%3A1},
  cites = {0},
  citedby = {0},
  pages = {33},
  booktitle = {PEPM},
}

@inproceedings{Pfenning04,
  title = {Substructural Operational Semantics and Linear Destination-Passing Style (Invited Talk)},
  author = {Frank Pfenning},
  year = {2004},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3302&spage=196},
  tags = {semantics, operational semantics},
  researchr = {https://researchr.org/publication/Pfenning04},
  cites = {0},
  citedby = {0},
  pages = {196},
  booktitle = {aplas},
}

@inproceedings{DunfieldP03,
  title = {Type Assignment for Intersections and Unions in Call-by-Value Languages},
  author = {Joshua Dunfield and Frank Pfenning},
  year = {2003},
  url = {http://link.springer.de/link/service/series/0558/bibs/2620/26200250.htm},
  researchr = {https://researchr.org/publication/DunfieldP03},
  cites = {0},
  citedby = {0},
  pages = {250-266},
  booktitle = {fossacs},
}

@inproceedings{Pfenning07:0,
  title = {Subtyping and intersection types revisited},
  author = {Frank Pfenning},
  year = {2007},
  doi = {10.1145/1291151.1291153},
  url = {http://doi.acm.org/10.1145/1291151.1291153},
  tags = {subtyping},
  researchr = {https://researchr.org/publication/Pfenning07%3A0},
  cites = {0},
  citedby = {0},
  pages = {219},
  booktitle = {ICFP},
}

@inproceedings{NordP88,
  title = {The Ergo Attribute System},
  author = {Robert L. Nord and Frank Pfenning},
  year = {1988},
  researchr = {https://researchr.org/publication/NordP88},
  cites = {0},
  citedby = {0},
  pages = {110-120},
  booktitle = {SDE},
}

@inproceedings{Pfenning88:0,
  title = {Partial Polymorphic Type Inference and Higher-Order Unification},
  author = {Frank Pfenning},
  year = {1988},
  doi = {10.1145/62678.62697},
  url = {http://doi.acm.org/10.1145/62678.62697},
  tags = {type inference},
  researchr = {https://researchr.org/publication/Pfenning88%3A0},
  cites = {0},
  citedby = {0},
  pages = {153-163},
  booktitle = {lfp},
}

@inproceedings{NanevskiPP03,
  title = {A modal foundation for meta-variables},
  author = {Aleksandar Nanevski and Brigitte Pientka and Frank Pfenning},
  year = {2003},
  doi = {10.1145/976571.976582},
  url = {http://doi.acm.org/10.1145/976571.976582},
  tags = {meta-model, Meta-Environment, meta-objects},
  researchr = {https://researchr.org/publication/NanevskiPP03},
  cites = {0},
  citedby = {0},
  booktitle = {ICFP},
}

@inproceedings{KohlhaseP93,
  title = {Unification in a Lambda-Calculus with Intersection Types},
  author = {Michael Kohlhase and Frank Pfenning},
  year = {1993},
  researchr = {https://researchr.org/publication/KohlhaseP93},
  cites = {0},
  citedby = {0},
  pages = {488-505},
  booktitle = {SLP},
}

@inproceedings{ThrunGPBSL03,
  title = {A Learning Algorithm for Localizing People Based on Wireless Signal Strength that Uses Labeled and Unlabeled Data},
  author = {Sebastian Thrun and Geoffrey J. Gordon and Frank Pfenning and Mary Berna and Brennan Sellner and Brad Lisien},
  year = {2003},
  tags = {rule-based},
  researchr = {https://researchr.org/publication/ThrunGPBSL03},
  cites = {0},
  citedby = {0},
  pages = {1427-1428},
  booktitle = {IJCAI},
}

@inproceedings{FreemanP91,
  title = {Refinement Types for ML},
  author = {Tim Freeman and Frank Pfenning},
  year = {1991},
  tags = {refinement},
  researchr = {https://researchr.org/publication/FreemanP91},
  cites = {0},
  citedby = {0},
  pages = {268-277},
  booktitle = {PLDI},
}

@article{SchurmannDP01,
  title = {Primitive recursion for higher-order abstract syntax},
  author = {Carsten Schürmann and Joëlle Despeyroux and Frank Pfenning},
  year = {2001},
  doi = {10.1016/S0304-3975(00)00418-7},
  url = {http://dx.doi.org/10.1016/S0304-3975(00)00418-7},
  tags = {abstract syntax},
  researchr = {https://researchr.org/publication/SchurmannDP01},
  cites = {0},
  citedby = {0},
  journal = {TCS},
  volume = {266},
  number = {1-2},
  pages = {1-57},
}

@article{NanevskiPP08,
  title = {Contextual modal type theory},
  author = {Aleksandar Nanevski and Frank Pfenning and Brigitte Pientka},
  year = {2008},
  doi = {10.1145/1352582.1352591},
  url = {http://doi.acm.org/10.1145/1352582.1352591},
  tags = {type theory},
  researchr = {https://researchr.org/publication/NanevskiPP08},
  cites = {0},
  citedby = {0},
  journal = {tocl},
  volume = {9},
  number = {3},
}

@inproceedings{ToninhoCP13,
  title = {Higher-Order Processes, Functions, and Sessions: A Monadic Integration},
  author = {Bernardo Toninho and Luís Caires and Frank Pfenning},
  year = {2013},
  doi = {10.1007/978-3-642-37036-6_20},
  url = {http://dx.doi.org/10.1007/978-3-642-37036-6_20},
  researchr = {https://researchr.org/publication/ToninhoCP13},
  cites = {0},
  citedby = {0},
  pages = {350-369},
  booktitle = {ESOP},
}

@inproceedings{PfenningS98:0,
  title = {Algorithms for Equality and Unification in the Presence of Notational Definitions},
  author = {Frank Pfenning and Carsten Schürmann},
  year = {1998},
  url = {http://link.springer.de/link/service/series/0558/bibs/1657/16570179.htm},
  researchr = {https://researchr.org/publication/PfenningS98%3A0},
  cites = {0},
  citedby = {0},
  pages = {179-193},
  booktitle = {TYPES},
}

@article{PfenningS98,
  title = {Algorithms for Equality and Unification in the Presence of Notational Definitions},
  author = {Frank Pfenning and Carsten Schürmann},
  year = {1998},
  url = {http://www.elsevier.com/gej-ng/31/29/23/41/23/show/Products/notes/index.htt#006},
  researchr = {https://researchr.org/publication/PfenningS98},
  cites = {0},
  citedby = {0},
  journal = {ENTCS},
  volume = {17},
  pages = {1-13},
}

@inproceedings{DeYoungCPT12,
  title = {Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication},
  author = {Henry DeYoung and Luís Caires and Frank Pfenning and Bernardo Toninho},
  year = {2012},
  doi = {10.4230/LIPIcs.CSL.2012.228},
  url = {http://dx.doi.org/10.4230/LIPIcs.CSL.2012.228},
  researchr = {https://researchr.org/publication/DeYoungCPT12},
  cites = {0},
  citedby = {0},
  pages = {228-242},
  booktitle = {csl},
}

@inproceedings{DeYoungP16,
  title = {Substructural Proofs as Automata},
  author = {Henry DeYoung and Frank Pfenning},
  year = {2016},
  doi = {10.1007/978-3-319-47958-3_1},
  url = {http://dx.doi.org/10.1007/978-3-319-47958-3_1},
  researchr = {https://researchr.org/publication/DeYoungP16},
  cites = {0},
  citedby = {0},
  pages = {3-22},
  booktitle = {aplas},
}

@inproceedings{McLaughlinP09,
  title = {Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method},
  author = {Sean McLaughlin and Frank Pfenning},
  year = {2009},
  doi = {10.1007/978-3-642-02959-2_19},
  url = {http://dx.doi.org/10.1007/978-3-642-02959-2_19},
  researchr = {https://researchr.org/publication/McLaughlinP09},
  cites = {0},
  citedby = {0},
  pages = {230-244},
  booktitle = {cade},
}

@article{ReedP09,
  title = {Intuitionistic Letcc via Labelled Deduction},
  author = {Jason Reed and Frank Pfenning},
  year = {2009},
  doi = {10.1016/j.entcs.2009.02.031},
  url = {http://dx.doi.org/10.1016/j.entcs.2009.02.031},
  researchr = {https://researchr.org/publication/ReedP09},
  cites = {0},
  citedby = {0},
  journal = {ENTCS},
  volume = {231},
  pages = {91-111},
}

@inproceedings{GargP10,
  title = {A Proof-Carrying File System},
  author = {Deepak Garg and Frank Pfenning},
  year = {2010},
  doi = {10.1109/SP.2010.28},
  url = {http://doi.ieeecomputersociety.org/10.1109/SP.2010.28},
  researchr = {https://researchr.org/publication/GargP10},
  cites = {0},
  citedby = {0},
  pages = {349-364},
  booktitle = {sp},
}

@article{NanevskiP05,
  title = {Staged computation with names and necessity},
  author = {Aleksandar Nanevski and Frank Pfenning},
  year = {2005},
  doi = {10.1017/S095679680500568X},
  url = {http://dx.doi.org/10.1017/S095679680500568X},
  tags = {staged computation},
  researchr = {https://researchr.org/publication/NanevskiP05},
  cites = {0},
  citedby = {0},
  journal = {JFP},
  volume = {15},
  number = {5},
  pages = {893-939},
}

@inproceedings{PfenningN90,
  title = {Presenting Intuitive Deductions via Symmetric Simplification},
  author = {Frank Pfenning and Dan Nesmith},
  year = {1990},
  researchr = {https://researchr.org/publication/PfenningN90},
  cites = {0},
  citedby = {0},
  pages = {336-350},
  booktitle = {cade},
}

@article{HarperP05,
  title = {On equivalence and canonical forms in the LF type theory},
  author = {Robert Harper and Frank Pfenning},
  year = {2005},
  doi = {10.1145/1042038.1042041},
  url = {http://doi.acm.org/10.1145/1042038.1042041},
  tags = {type theory},
  researchr = {https://researchr.org/publication/HarperP05},
  cites = {0},
  citedby = {0},
  journal = {tocl},
  volume = {6},
  number = {1},
  pages = {61-101},
}

@inproceedings{MichaylovP93,
  title = {Higher-Order Logic Programming as Constraint Logic Programming},
  author = {Spiro Michaylov and Frank Pfenning},
  year = {1993},
  tags = {constraints, logic programming, programming, logic},
  researchr = {https://researchr.org/publication/MichaylovP93},
  cites = {0},
  citedby = {0},
  pages = {210-218},
  booktitle = {ppcp},
}

@article{CervesatoP02,
  title = {A Linear Logical Framework},
  author = {Iliano Cervesato and Frank Pfenning},
  year = {2002},
  doi = {10.1006/inco.2001.2951},
  url = {http://dx.doi.org/10.1006/inco.2001.2951},
  researchr = {https://researchr.org/publication/CervesatoP02},
  cites = {0},
  citedby = {0},
  journal = {iandc},
  volume = {179},
  number = {1},
  pages = {19-75},
}

@article{WicklineLPD98,
  title = {Modal Types as Staging Specifications for Run-Time Code Generation},
  author = {Philip Wickline and Peter Lee and Frank Pfenning and Rowan Davies},
  year = {1998},
  doi = {10.1145/289121.289129},
  url = {http://doi.acm.org/10.1145/289121.289129},
  tags = {code generation},
  researchr = {https://researchr.org/publication/WicklineLPD98},
  cites = {0},
  citedby = {0},
  journal = {ACM Comput. Surv.},
  volume = {30},
  number = {3es},
  pages = {8},
}

@inproceedings{WicklineLP98,
  title = {Run-time Code Generation and Modal-ML},
  author = {Philip Wickline and Peter Lee and Frank Pfenning},
  year = {1998},
  tags = {code generation},
  researchr = {https://researchr.org/publication/WicklineLP98},
  cites = {0},
  citedby = {0},
  pages = {224-235},
  booktitle = {PLDI},
}

@article{WatkinsCPW08,
  title = {Specifying Properties of Concurrent Computations in CLF},
  author = {Kevin Watkins and Iliano Cervesato and Frank Pfenning and David Walker},
  year = {2008},
  doi = {10.1016/j.entcs.2007.11.013},
  url = {http://dx.doi.org/10.1016/j.entcs.2007.11.013},
  researchr = {https://researchr.org/publication/WatkinsCPW08},
  cites = {0},
  citedby = {0},
  journal = {ENTCS},
  volume = {199},
  pages = {67-87},
}

@article{Pfenning02,
  title = {Preface},
  author = {Frank Pfenning},
  year = {2002},
  url = {http://www.elsevier.com/gej-ng/31/29/23/125/50/show/Products/notes/index.htt#001},
  researchr = {https://researchr.org/publication/Pfenning02},
  cites = {0},
  citedby = {0},
  journal = {ENTCS},
  volume = {70},
  number = {2},
  pages = {146},
}

@article{PolokowP99,
  title = {Relating Natural Deduction and Sequent Calculus for Intuitionistic Non-Commutative Linear Logic},
  author = {J. Polokow and Frank Pfenning},
  year = {1999},
  url = {http://www.elsevier.com/gej-ng/31/29/23/44/23/show/Products/notes/index.htt#026},
  tags = {logic},
  researchr = {https://researchr.org/publication/PolokowP99},
  cites = {0},
  citedby = {0},
  journal = {ENTCS},
  volume = {20},
  pages = {449-466},
}

@inproceedings{Pfenning07:1,
  title = {On a Logical Foundation for Explicit Substitutions},
  author = {Frank Pfenning},
  year = {2007},
  doi = {10.1007/978-3-540-73228-0_1},
  url = {http://dx.doi.org/10.1007/978-3-540-73228-0_1},
  researchr = {https://researchr.org/publication/Pfenning07%3A1},
  cites = {0},
  citedby = {0},
  pages = {1},
  booktitle = {tlca},
}

@inproceedings{PfenningCT11,
  title = {Proof-Carrying Code in a Session-Typed Process Calculus},
  author = {Frank Pfenning and Luís Caires and Bernardo Toninho},
  year = {2011},
  doi = {10.1007/978-3-642-25379-9_4},
  url = {http://dx.doi.org/10.1007/978-3-642-25379-9_4},
  researchr = {https://researchr.org/publication/PfenningCT11},
  cites = {0},
  citedby = {0},
  pages = {21-36},
  booktitle = {CPP},
}

@inproceedings{PfenningP89,
  title = {Inductively Defined Types in the Calculus of Constructions},
  author = {Frank Pfenning and Christine Paulin-Mohring},
  year = {1989},
  researchr = {https://researchr.org/publication/PfenningP89},
  cites = {0},
  citedby = {0},
  pages = {209-228},
  booktitle = {mfps},
}

@inproceedings{CervesatoHP96,
  title = {Efficient Resource Management for Linear Logic Proof Search},
  author = {Iliano Cervesato and Joshua S. Hodas and Frank Pfenning},
  year = {1996},
  tags = {logic, search},
  researchr = {https://researchr.org/publication/CervesatoHP96},
  cites = {0},
  citedby = {0},
  pages = {67-81},
  booktitle = {elp},
}

@article{Pfenning02a,
  title = {Invited talk: Tri-Directional Type Checking},
  author = {Frank Pfenning},
  year = {2002},
  url = {http://www1.elsevier.com/gej-ng/31/29/23/125/51/show/Products/notes/index.htt#012},
  tags = {type checking},
  researchr = {https://researchr.org/publication/Pfenning02a},
  cites = {0},
  citedby = {0},
  journal = {ENTCS},
  volume = {70},
  number = {1},
}

@inproceedings{PfenningR92,
  title = {Implementing the Meta-Theory of Deductive Systems},
  author = {Frank Pfenning and Ekkehard Rohwedder},
  year = {1992},
  tags = {meta-model, Meta-Environment, meta-objects},
  researchr = {https://researchr.org/publication/PfenningR92},
  cites = {0},
  citedby = {0},
  pages = {537-551},
  booktitle = {cade},
}

@inproceedings{PolakowP99,
  title = {Natural Deduction for Intuitionistic Non-communicative Linear Logic},
  author = {Jeff Polakow and Frank Pfenning},
  year = {1999},
  url = {http://link.springer.de/link/service/series/0558/bibs/1581/15810295.htm},
  tags = {logic},
  researchr = {https://researchr.org/publication/PolakowP99},
  cites = {0},
  citedby = {0},
  pages = {295-309},
  booktitle = {tlca},
}

@inproceedings{AndrewsPIK86,
  title = {The TPS Theorem Proving System},
  author = {Peter B. Andrews and Frank Pfenning and Sunil Issar and C. P. Klapper},
  year = {1986},
  tags = {C++},
  researchr = {https://researchr.org/publication/AndrewsPIK86},
  cites = {0},
  citedby = {0},
  pages = {663-664},
  booktitle = {cade},
}

@inproceedings{Das0P18,
  title = {Work Analysis with Resource-Aware Session Types},
  author = {Ankush Das and Jan Hoffmann 0002 and Frank Pfenning},
  year = {2018},
  doi = {10.1145/3209108.3209146},
  url = {http://doi.acm.org/10.1145/3209108.3209146},
  researchr = {https://researchr.org/publication/Das0P18},
  cites = {0},
  citedby = {0},
  pages = {305-314},
  booktitle = {lics},
}

@inproceedings{XiP98,
  title = {Eliminating Array Bound Checking Through Dependent Types},
  author = {Hongwei Xi and Frank Pfenning},
  year = {1998},
  tags = {type checking},
  researchr = {https://researchr.org/publication/XiP98},
  cites = {0},
  citedby = {0},
  pages = {249-257},
  booktitle = {PLDI},
}

@inproceedings{DietzenP89,
  title = {Higher-Order and Modal Logic as a Framework for Explanation-Based Generalization},
  author = {Scott Dietzen and Frank Pfenning},
  year = {1989},
  tags = {rule-based, modal logic, logic},
  researchr = {https://researchr.org/publication/DietzenP89},
  cites = {0},
  citedby = {0},
  pages = {447-449},
  booktitle = {icml},
}

@inproceedings{LopezPPW05,
  title = {Monadic concurrent linear logic programming},
  author = {Pablo López and Frank Pfenning and Jeff Polakow and Kevin Watkins},
  year = {2005},
  doi = {10.1145/1069774.1069778},
  url = {http://doi.acm.org/10.1145/1069774.1069778},
  tags = {logic programming, programming, logic},
  researchr = {https://researchr.org/publication/LopezPPW05},
  cites = {0},
  citedby = {0},
  pages = {35-46},
  booktitle = {ppdp},
}

@article{CairesPT16,
  title = {Linear logic propositions as session types},
  author = {Luís Caires and Frank Pfenning and Bernardo Toninho},
  year = {2016},
  doi = {10.1017/S0960129514000218},
  url = {http://dx.doi.org/10.1017/S0960129514000218},
  researchr = {https://researchr.org/publication/CairesPT16},
  cites = {0},
  citedby = {0},
  journal = {mscs},
  volume = {26},
  number = {3},
  pages = {367-423},
}

@inproceedings{ToninhoCP11,
  title = {Dependent session types via intuitionistic linear type theory},
  author = {Bernardo Toninho and Luís Caires and Frank Pfenning},
  year = {2011},
  doi = {10.1145/2003476.2003499},
  url = {http://doi.acm.org/10.1145/2003476.2003499},
  researchr = {https://researchr.org/publication/ToninhoCP11},
  cites = {0},
  citedby = {0},
  pages = {161-172},
  booktitle = {ppdp},
}

@article{PfenningW95,
  title = {On a modal lambda calculus for S4},
  author = {Frank Pfenning and Hao Chi Wong},
  year = {1995},
  url = {http://www.elsevier.com/gej-ng/31/29/23/26/23/show/Products/notes/index.htt#029},
  researchr = {https://researchr.org/publication/PfenningW95},
  cites = {0},
  citedby = {0},
  journal = {ENTCS},
  volume = {1},
  pages = {515-534},
}

@article{PfenningL91,
  title = {Metacircularity in the Polymorphic lambda-Calculus},
  author = {Frank Pfenning and Peter Lee},
  year = {1991},
  researchr = {https://researchr.org/publication/PfenningL91},
  cites = {0},
  citedby = {0},
  journal = {TCS},
  volume = {89},
  number = {1},
  pages = {137-159},
}

@inproceedings{LovasP09,
  title = {Refinement Types as Proof Irrelevance},
  author = {William Lovas and Frank Pfenning},
  year = {2009},
  doi = {10.1007/978-3-642-02273-9_13},
  url = {http://dx.doi.org/10.1007/978-3-642-02273-9_13},
  tags = {refinement},
  researchr = {https://researchr.org/publication/LovasP09},
  cites = {0},
  citedby = {0},
  pages = {157-171},
  booktitle = {tlca},
}

@inproceedings{Pfenning84,
  title = {Analytic and Non-analytic Proofs},
  author = {Frank Pfenning},
  year = {1984},
  researchr = {https://researchr.org/publication/Pfenning84},
  cites = {0},
  citedby = {0},
  pages = {394-413},
  booktitle = {cade},
}

@inproceedings{PerezCPT12,
  title = {Linear Logical Relations for Session-Based Concurrency},
  author = {Jorge A. Pérez and Luís Caires and Frank Pfenning and Bernardo Toninho},
  year = {2012},
  doi = {10.1007/978-3-642-28869-2_27},
  url = {http://dx.doi.org/10.1007/978-3-642-28869-2_27},
  researchr = {https://researchr.org/publication/PerezCPT12},
  cites = {0},
  citedby = {0},
  pages = {539-558},
  booktitle = {ESOP},
}

@inproceedings{SaranliP07,
  title = {Using Constrained Intuitionistic Linear Logic for Hybrid Robotic Planning Problems},
  author = {Uluc Saranli and Frank Pfenning},
  year = {2007},
  doi = {10.1109/ROBOT.2007.364046},
  url = {http://dx.doi.org/10.1109/ROBOT.2007.364046},
  tags = {logic},
  researchr = {https://researchr.org/publication/SaranliP07},
  cites = {0},
  citedby = {0},
  pages = {3705-3710},
  booktitle = {icra},
}

@article{CraryKP05,
  title = {A monadic analysis of information flow security with mutable state},
  author = {Karl Crary and Aleksey Kliger and Frank Pfenning},
  year = {2005},
  doi = {10.1017/S0956796804005441},
  url = {http://dx.doi.org/10.1017/S0956796804005441},
  tags = {analysis, data-flow, security, data-flow analysis},
  researchr = {https://researchr.org/publication/CraryKP05},
  cites = {0},
  citedby = {0},
  journal = {JFP},
  volume = {15},
  number = {2},
  pages = {249-291},
}

@inproceedings{ChaudhuriP05:0,
  title = {Focusing the Inverse Method for Linear Logic},
  author = {Kaustuv Chaudhuri and Frank Pfenning},
  year = {2005},
  doi = {10.1007/11538363_15},
  url = {http://dx.doi.org/10.1007/11538363_15},
  tags = {logic},
  researchr = {https://researchr.org/publication/ChaudhuriP05%3A0},
  cites = {0},
  citedby = {0},
  pages = {200-215},
  booktitle = {csl},
}

@inproceedings{Pfenning01:0,
  title = {Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory},
  author = {Frank Pfenning},
  year = {2001},
  tags = {type theory},
  researchr = {https://researchr.org/publication/Pfenning01%3A0},
  cites = {0},
  citedby = {0},
  pages = {221-230},
  booktitle = {lics},
}
@proceedings{lpar:1994,
  title = {Logic Programming and Automated Reasoning, 5th International Conference, LPAR 94, Kiev, Ukraine, July 16-22, 1994, Proceedings},
  year = {1994},
  tags = {logic programming, programming, logic},
  researchr = {https://researchr.org/publication/lpar%3A1994},
  cites = {0},
  citedby = {0},
  booktitle = {Logic Programming and Automated Reasoning, 5th International Conference, LPAR 94, Kiev, Ukraine, July 16-22, 1994, Proceedings},
  conference = {lpar},
  editor = {Frank Pfenning},
  volume = {822},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-58216-9},
}

@proceedings{rta:2006,
  title = {Term Rewriting and Applications, 17th International Conference, RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings},
  year = {2006},
  tags = {term rewriting, graph-rewriting, rewriting},
  researchr = {https://researchr.org/publication/rta%3A2006},
  cites = {0},
  citedby = {0},
  booktitle = {Term Rewriting and Applications, 17th International Conference, RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings},
  conference = {RTA},
  editor = {Frank Pfenning},
  volume = {4098},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-36834-5},
}

@proceedings{ppdp-2000,
  title = {Proceedings of the 2nd international ACM SIGPLAN conference on on Principles and practice of declarative programming, Montreal, Canada, September 20-23, 2000},
  year = {2000},
  doi = {10.1145/351268},
  url = {https://doi.org/10.1145/351268},
  researchr = {https://researchr.org/publication/ppdp-2000},
  cites = {0},
  citedby = {0},
  booktitle = {Proceedings of the 2nd international ACM SIGPLAN conference on on Principles and practice of declarative programming, Montreal, Canada, September 20-23, 2000},
  conference = {ppdp},
  editor = {Maurizio Gabbrielli and Frank Pfenning},
  publisher = {ACM},
  isbn = {1-58113-265-4},
}

@proceedings{gpce:2003,
  title = {Generative Programming and Component Engineering, Second International Conference, GPCE 2003, Erfurt, Germany, September 22-25, 2003, Proceedings},
  year = {2003},
  tags = {generative programming, programming},
  researchr = {https://researchr.org/publication/gpce%3A2003},
  cites = {0},
  citedby = {0},
  booktitle = {Generative Programming and Component Engineering, Second International Conference, GPCE 2003, Erfurt, Germany, September 22-25, 2003, Proceedings},
  conference = {GPCE},
  editor = {Frank Pfenning and Yannis Smaragdakis},
  volume = {2830},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-20102-5},
}

@proceedings{cade:2007,
  title = {Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings},
  year = {2007},
  researchr = {https://researchr.org/publication/cade%3A2007},
  cites = {0},
  citedby = {0},
  booktitle = {Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings},
  conference = {cade},
  editor = {Frank Pfenning},
  volume = {4603},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-540-73594-6},
}

@proceedings{fossacs-2013,
  title = {Foundations of Software Science and Computation Structures - 16th International Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings},
  year = {2013},
  doi = {10.1007/978-3-642-37075-5},
  url = {http://dx.doi.org/10.1007/978-3-642-37075-5},
  researchr = {https://researchr.org/publication/fossacs-2013},
  cites = {0},
  citedby = {0},
  booktitle = {Foundations of Software Science and Computation Structures - 16th International Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings},
  conference = {fossacs},
  editor = {Frank Pfenning},
  volume = {7794},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-37074-8},
}