BibTeX records: Frank Pfenning

download as .bib file

@article{DBLP:journals/pacmpl/BalzerP17,
  author    = {Stephanie Balzer and
               Frank Pfenning},
  title     = {Manifest sharing with session types},
  journal   = {{PACMPL}},
  volume    = {1},
  number    = {{ICFP}},
  pages     = {37:1--37:29},
  year      = {2017},
  url       = {http://doi.acm.org/10.1145/3110281},
  doi       = {10.1145/3110281},
  timestamp = {Tue, 12 Sep 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/pacmpl/BalzerP17},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/mscs/CairesPT16,
  author    = {Lu{\'{\i}}s Caires and
               Frank Pfenning and
               Bernardo Toninho},
  title     = {Linear logic propositions as session types},
  journal   = {Mathematical Structures in Computer Science},
  volume    = {26},
  number    = {3},
  pages     = {367--423},
  year      = {2016},
  url       = {https://doi.org/10.1017/S0960129514000218},
  doi       = {10.1017/S0960129514000218},
  timestamp = {Sun, 28 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/mscs/CairesPT16},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/aplas/DeYoungP16,
  author    = {Henry DeYoung and
               Frank Pfenning},
  title     = {Substructural Proofs as Automata},
  booktitle = {Programming Languages and Systems - 14th Asian Symposium, {APLAS}
               2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings},
  pages     = {3--22},
  year      = {2016},
  crossref  = {DBLP:conf/aplas/2016},
  url       = {https://doi.org/10.1007/978-3-319-47958-3_1},
  doi       = {10.1007/978-3-319-47958-3_1},
  timestamp = {Fri, 19 May 2017 01:25:54 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/aplas/DeYoungP16},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/popl/JiaGP16,
  author    = {Limin Jia and
               Hannah Gommerstadt and
               Frank Pfenning},
  title     = {Monitors and blame assignment for higher-order session types},
  booktitle = {Proceedings of the 43rd Annual {ACM} {SIGPLAN-SIGACT} Symposium on
               Principles of Programming Languages, {POPL} 2016, St. Petersburg,
               FL, USA, January 20 - 22, 2016},
  pages     = {582--594},
  year      = {2016},
  crossref  = {DBLP:conf/popl/2016},
  url       = {http://doi.acm.org/10.1145/2837614.2837662},
  doi       = {10.1145/2837614.2837662},
  timestamp = {Wed, 09 Mar 2016 08:11:59 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/popl/JiaGP16},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:journals/corr/AcayP17,
  author    = {Cosku Acay and
               Frank Pfenning},
  title     = {Intersections and Unions of Session Types},
  booktitle = {Proceedings Eighth Workshop on Intersection Types and Related Systems,
               {ITRS} 2016, Porto, Portugal, 26th June 2016.},
  pages     = {4--19},
  year      = {2016},
  crossref  = {DBLP:journals/corr/Kobayashi17},
  url       = {https://doi.org/10.4204/EPTCS.242.3},
  doi       = {10.4204/EPTCS.242.3},
  timestamp = {Wed, 03 May 2017 14:47:57 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/corr/AcayP17},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:journals/corr/SilvaFP17,
  author    = {Miguel Silva and
               M{\'{a}}rio Florido and
               Frank Pfenning},
  title     = {Non-Blocking Concurrent Imperative Programming with Session Types},
  booktitle = {Proceedings Fourth International Workshop on Linearity, {LINEARITY}
               2016, Porto, Portugal, 25 June 2016.},
  pages     = {64--72},
  year      = {2016},
  crossref  = {DBLP:journals/corr/CervesatoF17},
  url       = {https://doi.org/10.4204/EPTCS.238.7},
  doi       = {10.4204/EPTCS.238.7},
  timestamp = {Wed, 03 May 2017 14:47:56 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/corr/SilvaFP17},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:journals/corr/WillseyPP17,
  author    = {Max Willsey and
               Rokhini Prabhu and
               Frank Pfenning},
  title     = {Design and Implementation of Concurrent {C0}},
  booktitle = {Proceedings Fourth International Workshop on Linearity, {LINEARITY}
               2016, Porto, Portugal, 25 June 2016.},
  pages     = {73--82},
  year      = {2016},
  crossref  = {DBLP:journals/corr/CervesatoF17},
  url       = {https://doi.org/10.4204/EPTCS.238.8},
  doi       = {10.4204/EPTCS.238.8},
  timestamp = {Wed, 03 May 2017 14:47:56 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/corr/WillseyPP17},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/agere/BalzerP15,
  author    = {Stephanie Balzer and
               Frank Pfenning},
  title     = {Objects as session-typed processes},
  booktitle = {Proceedings of the 5th International Workshop on Programming Based
               on Actors, Agents, and Decentralized Control, AGERE! 2015, Pittsburgh,
               PA, USA, October 26, 2015},
  pages     = {13--24},
  year      = {2015},
  crossref  = {DBLP:conf/agere/2015},
  url       = {http://doi.acm.org/10.1145/2824815.2824817},
  doi       = {10.1145/2824815.2824817},
  timestamp = {Tue, 03 Nov 2015 15:26:34 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/agere/BalzerP15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/fossacs/PfenningG15,
  author    = {Frank Pfenning and
               Dennis Griffith},
  title     = {Polarized Substructural Session Types},
  booktitle = {Foundations of Software Science and Computation Structures - 18th
               International Conference, FoSSaCS 2015, Held as Part of the European
               Joint Conferences on Theory and Practice of Software, {ETAPS} 2015,
               London, UK, April 11-18, 2015. Proceedings},
  pages     = {3--22},
  year      = {2015},
  crossref  = {DBLP:conf/fossacs/2015},
  url       = {https://doi.org/10.1007/978-3-662-46678-0_1},
  doi       = {10.1007/978-3-662-46678-0_1},
  timestamp = {Fri, 02 Jun 2017 20:48:43 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/fossacs/PfenningG15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/popl/Pfenning15,
  author    = {Frank Pfenning},
  title     = {Proof theory and its role in programming language research},
  booktitle = {Proceedings of the Programming Languages Mentoring Workshop, PLMW@POPL
               2015, Mumbai, India, January 14, 2015},
  pages     = {4:1},
  year      = {2015},
  crossref  = {DBLP:conf/popl/2015plmw},
  url       = {http://doi.acm.org/10.1145/2792434.2792438},
  doi       = {10.1145/2792434.2792438},
  timestamp = {Thu, 02 Mar 2017 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/popl/Pfenning15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/iandc/PerezCPT14,
  author    = {Jorge A. P{\'{e}}rez and
               Lu{\'{\i}}s Caires and
               Frank Pfenning and
               Bernardo Toninho},
  title     = {Linear logical relations and observational equivalences for session-based
               concurrency},
  journal   = {Inf. Comput.},
  volume    = {239},
  pages     = {254--302},
  year      = {2014},
  url       = {https://doi.org/10.1016/j.ic.2014.08.001},
  doi       = {10.1016/j.ic.2014.08.001},
  timestamp = {Tue, 06 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/iandc/PerezCPT14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/tplp/Pfenning14,
  author    = {Frank Pfenning},
  title     = {\emph{Programming with Higher-Order Logic}, by Dale Miller and Gopalan
               Nadathur, Cambridge University Press, 2012, Hardcover, {ISBN-10:}
               052187940X, xiv + 306 pp},
  journal   = {{TPLP}},
  volume    = {14},
  number    = {2},
  pages     = {265--267},
  year      = {2014},
  url       = {https://doi.org/10.1017/S1471068414000027},
  doi       = {10.1017/S1471068414000027},
  timestamp = {Sat, 27 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/tplp/Pfenning14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/tplp/CruzRGP14,
  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   = {{TPLP}},
  volume    = {14},
  number    = {4-5},
  pages     = {493--507},
  year      = {2014},
  url       = {https://doi.org/10.1017/S1471068414000167},
  doi       = {10.1017/S1471068414000167},
  timestamp = {Fri, 09 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/tplp/CruzRGP14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/tgc/ToninhoCP14,
  author    = {Bernardo Toninho and
               Lu{\'{\i}}s Caires and
               Frank Pfenning},
  title     = {Corecursion and Non-divergence in Session-Typed Processes},
  booktitle = {Trustworthy Global Computing - 9th International Symposium, {TGC}
               2014, Rome, Italy, September 5-6, 2014. Revised Selected Papers},
  pages     = {159--175},
  year      = {2014},
  crossref  = {DBLP:conf/tgc/2014},
  url       = {https://doi.org/10.1007/978-3-662-45917-1_11},
  doi       = {10.1007/978-3-662-45917-1_11},
  timestamp = {Sun, 21 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tgc/ToninhoCP14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/corr/CruzRGP14,
  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   = {CoRR},
  volume    = {abs/1405.3556},
  year      = {2014},
  url       = {http://arxiv.org/abs/1405.3556},
  archivePrefix = {arXiv},
  eprint    = {1405.3556},
  timestamp = {Wed, 07 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/corr/CruzRGP14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/esop/CairesPPT13,
  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 = {Programming Languages and Systems - 22nd European Symposium on Programming,
               {ESOP} 2013, Held as Part of the European Joint Conferences on Theory
               and Practice of Software, {ETAPS} 2013, Rome, Italy, March 16-24,
               2013. Proceedings},
  pages     = {330--349},
  year      = {2013},
  crossref  = {DBLP:conf/esop/2013},
  url       = {https://doi.org/10.1007/978-3-642-37036-6_19},
  doi       = {10.1007/978-3-642-37036-6_19},
  timestamp = {Fri, 02 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/esop/CairesPPT13},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/esop/ToninhoCP13,
  author    = {Bernardo Toninho and
               Lu{\'{\i}}s Caires and
               Frank Pfenning},
  title     = {Higher-Order Processes, Functions, and Sessions: {A} Monadic Integration},
  booktitle = {Programming Languages and Systems - 22nd European Symposium on Programming,
               {ESOP} 2013, Held as Part of the European Joint Conferences on Theory
               and Practice of Software, {ETAPS} 2013, Rome, Italy, March 16-24,
               2013. Proceedings},
  pages     = {350--369},
  year      = {2013},
  crossref  = {DBLP:conf/esop/2013},
  url       = {https://doi.org/10.1007/978-3-642-37036-6_20},
  doi       = {10.1007/978-3-642-37036-6_20},
  timestamp = {Fri, 19 May 2017 01:25:18 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/esop/ToninhoCP13},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/fossacs/2013,
  editor    = {Frank Pfenning},
  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},
  series    = {Lecture Notes in Computer Science},
  volume    = {7794},
  publisher = {Springer},
  year      = {2013},
  url       = {https://doi.org/10.1007/978-3-642-37075-5},
  doi       = {10.1007/978-3-642-37075-5},
  isbn      = {978-3-642-37074-8},
  timestamp = {Tue, 23 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/fossacs/2013},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/jcs/GargP12,
  author    = {Deepak Garg and
               Frank Pfenning},
  title     = {Stateful authorization logic - Proof theory and a case study},
  journal   = {Journal of Computer Security},
  volume    = {20},
  number    = {4},
  pages     = {353--391},
  year      = {2012},
  url       = {https://doi.org/10.3233/JCS-2012-0456},
  doi       = {10.3233/JCS-2012-0456},
  timestamp = {Fri, 26 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/jcs/GargP12},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/csl/DeYoungCPT12,
  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 = {Computer Science Logic (CSL'12) - 26th International Workshop/21st
               Annual Conference of the EACSL, {CSL} 2012, September 3-6, 2012, Fontainebleau,
               France},
  pages     = {228--242},
  year      = {2012},
  crossref  = {DBLP:conf/csl/2012},
  url       = {https://doi.org/10.4230/LIPIcs.CSL.2012.228},
  doi       = {10.4230/LIPIcs.CSL.2012.228},
  timestamp = {Wed, 24 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/csl/DeYoungCPT12},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/esop/PerezCPT12,
  author    = {Jorge A. P{\'{e}}rez and
               Lu{\'{\i}}s Caires and
               Frank Pfenning and
               Bernardo Toninho},
  title     = {Linear Logical Relations for Session-Based Concurrency},
  booktitle = {Programming Languages and Systems - 21st European Symposium on Programming,
               {ESOP} 2012, Held as Part of the European Joint Conferences on Theory
               and Practice of Software, {ETAPS} 2012, Tallinn, Estonia, March 24
               - April 1, 2012. Proceedings},
  pages     = {539--558},
  year      = {2012},
  crossref  = {DBLP:conf/esop/2012},
  url       = {https://doi.org/10.1007/978-3-642-28869-2_27},
  doi       = {10.1007/978-3-642-28869-2_27},
  timestamp = {Fri, 02 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/esop/PerezCPT12},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/fossacs/ToninhoCP12,
  author    = {Bernardo Toninho and
               Lu{\'{\i}}s Caires and
               Frank Pfenning},
  title     = {Functions as Session-Typed Processes},
  booktitle = {Foundations of Software Science and Computational Structures - 15th
               International Conference, {FOSSACS} 2012, Held as Part of the European
               Joint Conferences on Theory and Practice of Software, {ETAPS} 2012,
               Tallinn, Estonia, March 24 - April 1, 2012. Proceedings},
  pages     = {346--360},
  year      = {2012},
  crossref  = {DBLP:conf/fossacs/2012},
  url       = {https://doi.org/10.1007/978-3-642-28729-9_23},
  doi       = {10.1007/978-3-642-28729-9_23},
  timestamp = {Tue, 23 May 2017 01:08:04 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/fossacs/ToninhoCP12},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/tldi/CairesPT12,
  author    = {Lu{\'{\i}}s Caires and
               Frank Pfenning and
               Bernardo Toninho},
  title     = {Towards concurrent type theory},
  booktitle = {Proceedings of {TLDI} 2012: The Seventh {ACM} {SIGPLAN} Workshop on
               Types in Languages Design and Implementation, Philadelphia, PA, USA,
               Saturday, January 28, 2012},
  pages     = {1--12},
  year      = {2012},
  crossref  = {DBLP:conf/tldi/2012},
  url       = {http://doi.acm.org/10.1145/2103786.2103788},
  doi       = {10.1145/2103786.2103788},
  timestamp = {Fri, 18 May 2012 21:46:11 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tldi/CairesPT12},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/lisp/SimmonsP11,
  author    = {Robert J. Simmons and
               Frank Pfenning},
  title     = {Logical approximation for program analysis},
  journal   = {Higher-Order and Symbolic Computation},
  volume    = {24},
  number    = {1-2},
  pages     = {41--80},
  year      = {2011},
  url       = {https://doi.org/10.1007/s10990-011-9071-2},
  doi       = {10.1007/s10990-011-9071-2},
  timestamp = {Tue, 06 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/lisp/SimmonsP11},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cpp/PfenningCT11,
  author    = {Frank Pfenning and
               Lu{\'{\i}}s Caires and
               Bernardo Toninho},
  title     = {Proof-Carrying Code in a Session-Typed Process Calculus},
  booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
               2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
  pages     = {21--36},
  year      = {2011},
  crossref  = {DBLP:conf/cpp/2011},
  url       = {https://doi.org/10.1007/978-3-642-25379-9_4},
  doi       = {10.1007/978-3-642-25379-9_4},
  timestamp = {Thu, 25 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cpp/PfenningCT11},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/ppdp/ToninhoCP11,
  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 {ACM} {SIGPLAN} Conference on
               Principles and Practice of Declarative Programming, July 20-22, 2011,
               Odense, Denmark},
  pages     = {161--172},
  year      = {2011},
  crossref  = {DBLP:conf/ppdp/2011},
  url       = {http://doi.acm.org/10.1145/2003476.2003499},
  doi       = {10.1145/2003476.2003499},
  timestamp = {Tue, 18 Oct 2011 19:19:37 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ppdp/ToninhoCP11},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/stm/MorgensternGP11,
  author    = {Jamie Morgenstern and
               Deepak Garg and
               Frank Pfenning},
  title     = {A Proof-Carrying File System with Revocable and Use-Once Certificates},
  booktitle = {Security and Trust Management - 7th International Workshop, {STM}
               2011, Copenhagen, Denmark, June 27-28, 2011, Revised Selected Papers},
  pages     = {40--55},
  year      = {2011},
  crossref  = {DBLP:conf/stm/2011},
  url       = {https://doi.org/10.1007/978-3-642-29963-6_5},
  doi       = {10.1007/978-3-642-29963-6_5},
  timestamp = {Wed, 24 May 2017 08:30:51 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/stm/MorgensternGP11},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/corr/abs-1009-1861,
  author    = {William Lovas and
               Frank Pfenning},
  title     = {Refinement Types for Logical Frameworks and Their Interpretation as
               Proof Irrelevance},
  journal   = {Logical Methods in Computer Science},
  volume    = {6},
  number    = {4},
  year      = {2010},
  url       = {https://doi.org/10.2168/LMCS-6(4:5)2010},
  doi       = {10.2168/LMCS-6(4:5)2010},
  timestamp = {Wed, 03 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/corr/abs-1009-1861},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/concur/CairesP10,
  author    = {Lu{\'{\i}}s Caires and
               Frank Pfenning},
  title     = {Session Types as Intuitionistic Linear Propositions},
  booktitle = {{CONCUR} 2010 - Concurrency Theory, 21th International Conference,
               {CONCUR} 2010, Paris, France, August 31-September 3, 2010. Proceedings},
  pages     = {222--236},
  year      = {2010},
  crossref  = {DBLP:conf/concur/2010},
  url       = {https://doi.org/10.1007/978-3-642-15375-4_16},
  doi       = {10.1007/978-3-642-15375-4_16},
  timestamp = {Tue, 23 May 2017 01:11:19 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/concur/CairesP10},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/lics/Pfenning10,
  author    = {Frank Pfenning},
  title     = {Possession as Linear Knowledge},
  booktitle = {3rd International Workshop on Logics, Agents, and Mobility, LAM'10,
               Edinburgh, UK, July 14, 2010},
  pages     = {1},
  year      = {2010},
  crossref  = {DBLP:conf/lics/2010lam},
  url       = {http://www.easychair.org/publications/paper/53011},
  timestamp = {Tue, 25 Jul 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lics/Pfenning10},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/sp/GargP10,
  author    = {Deepak Garg and
               Frank Pfenning},
  title     = {A Proof-Carrying File System},
  booktitle = {31st {IEEE} Symposium on Security and Privacy, S{\&}P 2010, 16-19
               May 2010, Berleley/Oakland, California, {USA}},
  pages     = {349--364},
  year      = {2010},
  crossref  = {DBLP:conf/sp/2010},
  url       = {https://doi.org/10.1109/SP.2010.28},
  doi       = {10.1109/SP.2010.28},
  timestamp = {Fri, 26 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/sp/GargP10},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/stm/GargP10,
  author    = {Deepak Garg and
               Frank Pfenning},
  title     = {Stateful Authorization Logic: - Proof Theory and a Case Study},
  booktitle = {Security and Trust Management - 6th International Workshop, {STM}
               2010, Athens, Greece, September 23-24, 2010, Revised Selected Papers},
  pages     = {210--225},
  year      = {2010},
  crossref  = {DBLP:conf/stm/2010},
  url       = {https://doi.org/10.1007/978-3-642-22444-7_14},
  doi       = {10.1007/978-3-642-22444-7_14},
  timestamp = {Wed, 24 May 2017 08:30:51 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/stm/GargP10},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/entcs/ReedP09,
  author    = {Jason Reed and
               Frank Pfenning},
  title     = {Intuitionistic Letcc via Labelled Deduction},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {231},
  pages     = {91--111},
  year      = {2009},
  url       = {https://doi.org/10.1016/j.entcs.2009.02.031},
  doi       = {10.1016/j.entcs.2009.02.031},
  timestamp = {Sun, 28 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/entcs/ReedP09},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/McLaughlinP09,
  author    = {Sean McLaughlin and
               Frank Pfenning},
  title     = {Efficient Intuitionistic Theorem Proving with the Polarized Inverse
               Method},
  booktitle = {Automated Deduction - CADE-22, 22nd International Conference on Automated
               Deduction, Montreal, Canada, August 2-7, 2009. Proceedings},
  pages     = {230--244},
  year      = {2009},
  crossref  = {DBLP:conf/cade/2009},
  url       = {https://doi.org/10.1007/978-3-642-02959-2_19},
  doi       = {10.1007/978-3-642-02959-2_19},
  timestamp = {Sun, 21 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/McLaughlinP09},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/lics/PfenningS09,
  author    = {Frank Pfenning and
               Robert J. Simmons},
  title     = {Substructural Operational Semantics as Ordered Logic Programming},
  booktitle = {Proceedings of the 24th Annual {IEEE} Symposium on Logic in Computer
               Science, {LICS} 2009, 11-14 August 2009, Los Angeles, CA, {USA}},
  pages     = {101--110},
  year      = {2009},
  crossref  = {DBLP:conf/lics/2009},
  url       = {https://doi.org/10.1109/LICS.2009.8},
  doi       = {10.1109/LICS.2009.8},
  timestamp = {Sun, 04 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lics/PfenningS09},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/pepm/SimmonsP09,
  author    = {Robert J. Simmons and
               Frank Pfenning},
  title     = {Linear logical approximations},
  booktitle = {Proceedings of the 2009 {ACM} {SIGPLAN} Symposium on Partial Evaluation
               and Semantics-based Program Manipulation, {PEPM} 2009, Savannah, GA,
               USA, January 19-20, 2009},
  pages     = {9--20},
  year      = {2009},
  crossref  = {DBLP:conf/pepm/2009},
  url       = {http://doi.acm.org/10.1145/1480945.1480949},
  doi       = {10.1145/1480945.1480949},
  timestamp = {Mon, 05 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/pepm/SimmonsP09},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/tlca/LovasP09,
  author    = {William Lovas and
               Frank Pfenning},
  title     = {Refinement Types as Proof Irrelevance},
  booktitle = {Typed Lambda Calculi and Applications, 9th International Conference,
               {TLCA} 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings},
  pages     = {157--171},
  year      = {2009},
  crossref  = {DBLP:conf/tlca/2009},
  url       = {https://doi.org/10.1007/978-3-642-02273-9_13},
  doi       = {10.1007/978-3-642-02273-9_13},
  timestamp = {Wed, 17 May 2017 14:24:41 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tlca/LovasP09},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/entcs/LovasP08,
  author    = {William Lovas and
               Frank Pfenning},
  title     = {A Bidirectional Refinement Type System for {LF}},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {196},
  pages     = {113--128},
  year      = {2008},
  url       = {https://doi.org/10.1016/j.entcs.2007.09.021},
  doi       = {10.1016/j.entcs.2007.09.021},
  timestamp = {Sun, 28 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/entcs/LovasP08},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/entcs/WatkinsCPW08,
  author    = {Kevin Watkins and
               Iliano Cervesato and
               Frank Pfenning and
               David Walker},
  title     = {Specifying Properties of Concurrent Computations in {CLF}},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {199},
  pages     = {67--87},
  year      = {2008},
  url       = {https://doi.org/10.1016/j.entcs.2007.11.013},
  doi       = {10.1016/j.entcs.2007.11.013},
  timestamp = {Mon, 05 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/entcs/WatkinsCPW08},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/jar/ChaudhuriPP08,
  author    = {Kaustuv Chaudhuri and
               Frank Pfenning and
               Greg Price},
  title     = {A Logical Characterization of Forward and Backward Chaining in the
               Inverse Method},
  journal   = {J. Autom. Reasoning},
  volume    = {40},
  number    = {2-3},
  pages     = {133--177},
  year      = {2008},
  url       = {https://doi.org/10.1007/s10817-007-9091-0},
  doi       = {10.1007/s10817-007-9091-0},
  timestamp = {Sat, 20 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/jar/ChaudhuriPP08},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/tocl/NanevskiPP08,
  author    = {Aleksandar Nanevski and
               Frank Pfenning and
               Brigitte Pientka},
  title     = {Contextual modal type theory},
  journal   = {{ACM} Trans. Comput. Log.},
  volume    = {9},
  number    = {3},
  pages     = {23:1--23:49},
  year      = {2008},
  url       = {http://doi.acm.org/10.1145/1352582.1352591},
  doi       = {10.1145/1352582.1352591},
  timestamp = {Mon, 09 Jan 2017 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/journals/tocl/NanevskiPP08},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/toplas/ParkPT08,
  author    = {Sungwoo Park and
               Frank Pfenning and
               Sebastian Thrun},
  title     = {A probabilistic language based on sampling functions},
  journal   = {{ACM} Trans. Program. Lang. Syst.},
  volume    = {31},
  number    = {1},
  pages     = {4:1--4:46},
  year      = {2008},
  url       = {http://doi.acm.org/10.1145/1452044.1452048},
  doi       = {10.1145/1452044.1452048},
  timestamp = {Fri, 06 Jan 2017 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/journals/toplas/ParkPT08},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/csfw/DeYoungGP08,
  author    = {Henry DeYoung and
               Deepak Garg and
               Frank Pfenning},
  title     = {An Authorization Logic With Explicit Time},
  booktitle = {Proceedings of the 21st {IEEE} Computer Security Foundations Symposium,
               {CSF} 2008, Pittsburgh, Pennsylvania, 23-25 June 2008},
  pages     = {133--145},
  year      = {2008},
  crossref  = {DBLP:conf/csfw/2008},
  url       = {https://doi.org/10.1109/CSF.2008.15},
  doi       = {10.1109/CSF.2008.15},
  timestamp = {Thu, 25 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/csfw/DeYoungGP08},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/icalp/SimmonsP08,
  author    = {Robert J. Simmons and
               Frank Pfenning},
  title     = {Linear Logical Algorithms},
  booktitle = {Automata, Languages and Programming, 35th International Colloquium,
               {ICALP} 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part
               {II} - Track {B:} Logic, Semantics, and Theory of Programming {\&}
               Track {C:} Security and Cryptography Foundations},
  pages     = {336--347},
  year      = {2008},
  crossref  = {DBLP:conf/icalp/2008-2},
  url       = {https://doi.org/10.1007/978-3-540-70583-3_28},
  doi       = {10.1007/978-3-540-70583-3_28},
  timestamp = {Tue, 13 Jun 2017 10:37:56 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/icalp/SimmonsP08},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/lpar/McLaughlinP08,
  author    = {Sean McLaughlin and
               Frank Pfenning},
  title     = {Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional
               Logic},
  booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 15th
               International Conference, {LPAR} 2008, Doha, Qatar, November 22-27,
               2008. Proceedings},
  pages     = {174--181},
  year      = {2008},
  crossref  = {DBLP:conf/lpar/2008},
  url       = {https://doi.org/10.1007/978-3-540-89439-1_12},
  doi       = {10.1007/978-3-540-89439-1_12},
  timestamp = {Tue, 13 Jun 2017 10:37:56 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/McLaughlinP08},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/icfp/Pfenning07,
  author    = {Frank Pfenning},
  title     = {Subtyping and intersection types revisited},
  booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
               Functional Programming, {ICFP} 2007, Freiburg, Germany, October 1-3,
               2007},
  pages     = {219},
  year      = {2007},
  crossref  = {DBLP:conf/icfp/2007},
  url       = {http://doi.acm.org/10.1145/1291151.1291153},
  doi       = {10.1145/1291151.1291153},
  timestamp = {Tue, 06 Nov 2007 12:48:33 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/icfp/Pfenning07},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/icra/SaranliP07,
  author    = {Uluc Saranli and
               Frank Pfenning},
  title     = {Using Constrained Intuitionistic Linear Logic for Hybrid Robotic Planning
               Problems},
  booktitle = {2007 {IEEE} International Conference on Robotics and Automation, {ICRA}
               2007, 10-14 April 2007, Roma, Italy},
  pages     = {3705--3710},
  year      = {2007},
  crossref  = {DBLP:conf/icra/2007},
  url       = {https://doi.org/10.1109/ROBOT.2007.364046},
  doi       = {10.1109/ROBOT.2007.364046},
  timestamp = {Mon, 22 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/icra/SaranliP07},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/ndss/BowersBGPR07,
  author    = {Kevin D. Bowers and
               Lujo Bauer and
               Deepak Garg and
               Frank Pfenning and
               Michael K. Reiter},
  title     = {Consumable Credentials in Linear-Logic-Based Access-Control Systems},
  booktitle = {Proceedings of the Network and Distributed System Security Symposium,
               {NDSS} 2007, San Diego, California, USA, 28th February - 2nd March
               2007},
  year      = {2007},
  crossref  = {DBLP:conf/ndss/2007},
  url       = {http://www.isoc.org/isoc/conferences/ndss/07/papers/consumable_credentials.pdf},
  timestamp = {Fri, 02 Jan 2015 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/ndss/BowersBGPR07},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/rta/Pfenning07,
  author    = {Frank Pfenning},
  title     = {On a Logical Foundation for Explicit Substitutions},
  booktitle = {Term Rewriting and Applications, 18th International Conference, {RTA}
               2007, Paris, France, June 26-28, 2007, Proceedings},
  pages     = {19},
  year      = {2007},
  crossref  = {DBLP:conf/rta/2007},
  url       = {https://doi.org/10.1007/978-3-540-73449-9_3},
  doi       = {10.1007/978-3-540-73449-9_3},
  timestamp = {Fri, 02 Jun 2017 13:01:07 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/rta/Pfenning07},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/tlca/Pfenning07,
  author    = {Frank Pfenning},
  title     = {On a Logical Foundation for Explicit Substitutions},
  booktitle = {Typed Lambda Calculi and Applications, 8th International Conference,
               {TLCA} 2007, Paris, France, June 26-28, 2007, Proceedings},
  pages     = {1},
  year      = {2007},
  crossref  = {DBLP:conf/tlca/2007},
  url       = {https://doi.org/10.1007/978-3-540-73228-0_1},
  doi       = {10.1007/978-3-540-73228-0_1},
  timestamp = {Fri, 02 Jun 2017 13:01:07 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tlca/Pfenning07},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/2007,
  editor    = {Frank Pfenning},
  title     = {Automated Deduction - CADE-21, 21st International Conference on Automated
               Deduction, Bremen, Germany, July 17-20, 2007, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4603},
  publisher = {Springer},
  year      = {2007},
  url       = {https://doi.org/10.1007/978-3-540-73595-3},
  doi       = {10.1007/978-3-540-73595-3},
  isbn      = {978-3-540-73594-6},
  timestamp = {Fri, 02 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/2007},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/ChaudhuriPP06,
  author    = {Kaustuv Chaudhuri and
               Frank Pfenning and
               Greg Price},
  title     = {A Logical Characterization of Forward and Backward Chaining in the
               Inverse Method},
  booktitle = {Automated Reasoning, Third International Joint Conference, {IJCAR}
               2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
  pages     = {97--111},
  year      = {2006},
  crossref  = {DBLP:conf/cade/2006},
  url       = {https://doi.org/10.1007/11814771_9},
  doi       = {10.1007/11814771_9},
  timestamp = {Fri, 02 Jun 2017 13:01:06 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/ChaudhuriPP06},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/csfw/GargP06,
  author    = {Deepak Garg and
               Frank Pfenning},
  title     = {Non-Interference in Constructive Authorization Logic},
  booktitle = {19th {IEEE} Computer Security Foundations Workshop, {(CSFW-19} 2006),
               5-7 July 2006, Venice, Italy},
  pages     = {283--296},
  year      = {2006},
  crossref  = {DBLP:conf/csfw/2006},
  url       = {https://doi.org/10.1109/CSFW.2006.18},
  doi       = {10.1109/CSFW.2006.18},
  timestamp = {Thu, 25 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/csfw/GargP06},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/esorics/GargBBPR06,
  author    = {Deepak Garg and
               Lujo Bauer and
               Kevin D. Bowers and
               Frank Pfenning and
               Michael K. Reiter},
  title     = {A Linear Logic of Authorization and Knowledge},
  booktitle = {Computer Security - {ESORICS} 2006, 11th European Symposium on Research
               in Computer Security, Hamburg, Germany, September 18-20, 2006, Proceedings},
  pages     = {297--312},
  year      = {2006},
  crossref  = {DBLP:conf/esorics/2006},
  url       = {https://doi.org/10.1007/11863908_19},
  doi       = {10.1007/11863908_19},
  timestamp = {Fri, 02 Jun 2017 13:01:07 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/esorics/GargBBPR06},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/rta/2006,
  editor    = {Frank Pfenning},
  title     = {Term Rewriting and Applications, 17th International Conference, {RTA}
               2006, Seattle, WA, USA, August 12-14, 2006, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4098},
  publisher = {Springer},
  year      = {2006},
  url       = {https://doi.org/10.1007/11805618},
  doi       = {10.1007/11805618},
  isbn      = {3-540-36834-5},
  timestamp = {Fri, 02 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/rta/2006},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/jfp/CraryKP05,
  author    = {Karl Crary and
               Aleksey Kliger and
               Frank Pfenning},
  title     = {A monadic analysis of information flow security with mutable state},
  journal   = {J. Funct. Program.},
  volume    = {15},
  number    = {2},
  pages     = {249--291},
  year      = {2005},
  url       = {https://doi.org/10.1017/S0956796804005441},
  doi       = {10.1017/S0956796804005441},
  timestamp = {Sat, 27 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/jfp/CraryKP05},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/jfp/NanevskiP05,
  author    = {Aleksandar Nanevski and
               Frank Pfenning},
  title     = {Staged computation with names and necessity},
  journal   = {J. Funct. Program.},
  volume    = {15},
  number    = {5},
  pages     = {893--939},
  year      = {2005},
  url       = {https://doi.org/10.1017/S095679680500568X},
  doi       = {10.1017/S095679680500568X},
  timestamp = {Sat, 27 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/jfp/NanevskiP05},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/tocl/HarperP05,
  author    = {Robert Harper and
               Frank Pfenning},
  title     = {On equivalence and canonical forms in the {LF} type theory},
  journal   = {{ACM} Trans. Comput. Log.},
  volume    = {6},
  number    = {1},
  pages     = {61--101},
  year      = {2005},
  url       = {http://doi.acm.org/10.1145/1042038.1042041},
  doi       = {10.1145/1042038.1042041},
  timestamp = {Tue, 14 Mar 2017 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/journals/tocl/HarperP05},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/ChaudhuriP05,
  author    = {Kaustuv Chaudhuri and
               Frank Pfenning},
  title     = {A Focusing Inverse Method Theorem Prover for First-Order Linear Logic},
  booktitle = {Automated Deduction - CADE-20, 20th International Conference on Automated
               Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings},
  pages     = {69--83},
  year      = {2005},
  crossref  = {DBLP:conf/cade/2005},
  url       = {https://doi.org/10.1007/11532231_6},
  doi       = {10.1007/11532231_6},
  timestamp = {Tue, 30 May 2017 16:36:52 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/ChaudhuriP05},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/concur/GargP05,
  author    = {Deepak Garg and
               Frank Pfenning},
  title     = {Type-Directed Concurrency},
  booktitle = {{CONCUR} 2005 - Concurrency Theory, 16th International Conference,
               {CONCUR} 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings},
  pages     = {6--20},
  year      = {2005},
  crossref  = {DBLP:conf/concur/2005},
  url       = {https://doi.org/10.1007/11539452_5},
  doi       = {10.1007/11539452_5},
  timestamp = {Tue, 30 May 2017 16:36:53 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/concur/GargP05},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/csl/ChaudhuriP05,
  author    = {Kaustuv Chaudhuri and
               Frank Pfenning},
  title     = {Focusing the Inverse Method for Linear Logic},
  booktitle = {Computer Science Logic, 19th International Workshop, {CSL} 2005, 14th
               Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings},
  pages     = {200--215},
  year      = {2005},
  crossref  = {DBLP:conf/csl/2005},
  url       = {https://doi.org/10.1007/11538363_15},
  doi       = {10.1007/11538363_15},
  timestamp = {Tue, 30 May 2017 16:36:53 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/csl/ChaudhuriP05},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/icfp/Pfenning05,
  author    = {Frank Pfenning},
  title     = {Towards a type theory of contexts},
  booktitle = {{ACM} {SIGPLAN} International Conference on Functional Programming,
               Workshop on Mechanized reasoning about languages with variable binding,
               {MERLIN} 2005, Tallinn, Estonia, September 30, 2005},
  pages     = {1},
  year      = {2005},
  crossref  = {DBLP:conf/icfp/2005merlin},
  url       = {http://doi.acm.org/10.1145/1088454.1088455},
  doi       = {10.1145/1088454.1088455},
  timestamp = {Wed, 23 Apr 2008 15:32:32 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/icfp/Pfenning05},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/popl/ParkPT05,
  author    = {Sungwoo Park and
               Frank Pfenning and
               Sebastian Thrun},
  title     = {A probabilistic language based upon sampling functions},
  booktitle = {Proceedings of the 32nd {ACM} {SIGPLAN-SIGACT} Symposium on Principles
               of Programming Languages, {POPL} 2005, Long Beach, California, USA,
               January 12-14, 2005},
  pages     = {171--182},
  year      = {2005},
  crossref  = {DBLP:conf/popl/2005},
  url       = {http://doi.acm.org/10.1145/1040305.1040320},
  doi       = {10.1145/1040305.1040320},
  timestamp = {Tue, 22 May 2012 15:24:56 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/popl/ParkPT05},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/ppdp/LopezPPW05,
  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 {ACM} {SIGPLAN} Conference on
               Principles and Practice of Declarative Programming, July 11-13 2005,
               Lisbon, Portugal},
  pages     = {35--46},
  year      = {2005},
  crossref  = {DBLP:conf/ppdp/2005},
  url       = {http://doi.acm.org/10.1145/1069774.1069778},
  doi       = {10.1145/1069774.1069778},
  timestamp = {Wed, 15 Feb 2006 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/ppdp/LopezPPW05},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/jar/AndrewsBPBIX04,
  author    = {Peter B. Andrews and
               Chad E. Brown and
               Frank Pfenning and
               Matthew Bishop and
               Sunil Issar and
               Hongwei Xi},
  title     = {{ETPS:} {A} System to Help Students Write Formal Proofs},
  journal   = {J. Autom. Reasoning},
  volume    = {32},
  number    = {1},
  pages     = {75--92},
  year      = {2004},
  url       = {https://doi.org/10.1023/B:JARS.0000021871.18776.94},
  doi       = {10.1023/B:JARS.0000021871.18776.94},
  timestamp = {Sat, 20 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/jar/AndrewsBPBIX04},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/aplas/Pfenning04,
  author    = {Frank Pfenning},
  title     = {Substructural Operational Semantics and Linear Destination-Passing
               Style (Invited Talk)},
  booktitle = {Programming Languages and Systems: Second Asian Symposium, {APLAS}
               2004, Taipei, Taiwan, November 4-6, 2004. Proceedings},
  pages     = {196},
  year      = {2004},
  crossref  = {DBLP:conf/aplas/2004},
  url       = {https://doi.org/10.1007/978-3-540-30477-7_13},
  doi       = {10.1007/978-3-540-30477-7_13},
  timestamp = {Tue, 30 May 2017 16:36:52 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/aplas/Pfenning04},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/lics/VIICHP04,
  author    = {Tom Murphy VII and
               Karl Crary and
               Robert Harper and
               Frank Pfenning},
  title     = {A Symmetric Modal Lambda Calculus for Distributed Computing},
  booktitle = {19th {IEEE} Symposium on Logic in Computer Science {(LICS} 2004),
               14-17 July 2004, Turku, Finland, Proceedings},
  pages     = {286--295},
  year      = {2004},
  crossref  = {DBLP:conf/lics/2004},
  url       = {https://doi.org/10.1109/LICS.2004.1319623},
  doi       = {10.1109/LICS.2004.1319623},
  timestamp = {Thu, 25 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lics/VIICHP04},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/popl/DunfieldP04,
  author    = {Joshua Dunfield and
               Frank Pfenning},
  title     = {Tridirectional typechecking},
  booktitle = {Proceedings of the 31st {ACM} {SIGPLAN-SIGACT} Symposium on Principles
               of Programming Languages, {POPL} 2004, Venice, Italy, January 14-16,
               2004},
  pages     = {281--292},
  year      = {2004},
  crossref  = {DBLP:conf/popl/2004},
  url       = {http://doi.acm.org/10.1145/964001.964025},
  doi       = {10.1145/964001.964025},
  timestamp = {Tue, 22 May 2012 15:24:56 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/popl/DunfieldP04},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/tphol/AndersonP04,
  author    = {Penny Anderson and
               Frank Pfenning},
  title     = {Verifying Uniqueness in a Logical Framework},
  booktitle = {Theorem Proving in Higher Order Logics, 17th International Conference,
               TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings},
  pages     = {18--33},
  year      = {2004},
  crossref  = {DBLP:conf/tphol/2004},
  url       = {https://doi.org/10.1007/978-3-540-30142-4_2},
  doi       = {10.1007/978-3-540-30142-4_2},
  timestamp = {Tue, 30 May 2017 12:57:44 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tphol/AndersonP04},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/logcom/CervesatoP03,
  author    = {Iliano Cervesato and
               Frank Pfenning},
  title     = {A Linear Spine Calculus},
  journal   = {J. Log. Comput.},
  volume    = {13},
  number    = {5},
  pages     = {639--688},
  year      = {2003},
  url       = {https://doi.org/10.1093/logcom/13.5.639},
  doi       = {10.1093/logcom/13.5.639},
  timestamp = {Tue, 06 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/logcom/CervesatoP03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/tcs/ColbyCHLP03,
  author    = {Christopher Colby and
               Karl Crary and
               Robert Harper and
               Peter Lee and
               Frank Pfenning},
  title     = {Automated techniques for provably safe mobile code},
  journal   = {Theor. Comput. Sci.},
  volume    = {290},
  number    = {2},
  pages     = {1175--1199},
  year      = {2003},
  url       = {https://doi.org/10.1016/S0304-3975(01)00201-8},
  doi       = {10.1016/S0304-3975(01)00201-8},
  timestamp = {Sun, 28 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/tcs/ColbyCHLP03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/tocl/MomiglianoP03,
  author    = {Alberto Momigliano and
               Frank Pfenning},
  title     = {Higher-order pattern complement and the strict lambda-calculus},
  journal   = {{ACM} Trans. Comput. Log.},
  volume    = {4},
  number    = {4},
  pages     = {493--529},
  year      = {2003},
  url       = {http://doi.acm.org/10.1145/937555.937559},
  doi       = {10.1145/937555.937559},
  timestamp = {Sat, 16 Sep 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/tocl/MomiglianoP03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/PientkaP03,
  author    = {Brigitte Pientka and
               Frank Pfenning},
  title     = {Optimizing Higher-Order Pattern Unification},
  booktitle = {Automated Deduction - CADE-19, 19th International Conference on Automated
               Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings},
  pages     = {473--487},
  year      = {2003},
  crossref  = {DBLP:conf/cade/2003},
  url       = {https://doi.org/10.1007/978-3-540-45085-6_40},
  doi       = {10.1007/978-3-540-45085-6_40},
  timestamp = {Mon, 29 May 2017 16:53:43 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/PientkaP03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/fossacs/DunfieldP03,
  author    = {Joshua Dunfield and
               Frank Pfenning},
  title     = {Type Assignment for Intersections and Unions in Call-by-Value Languages},
  booktitle = {Foundations of Software Science and Computational Structures, 6th
               International Conference, {FOSSACS} 2003 Held as Part of the Joint
               European Conference on Theory and Practice of Software, {ETAPS} 2003,
               Warsaw, Poland, April 7-11, 2003, Proceedings},
  pages     = {250--266},
  year      = {2003},
  crossref  = {DBLP:conf/fossacs/2003},
  url       = {https://doi.org/10.1007/3-540-36576-1_16},
  doi       = {10.1007/3-540-36576-1_16},
  timestamp = {Mon, 29 May 2017 16:53:44 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/fossacs/DunfieldP03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/icfp/NanevskiPP03,
  author    = {Aleksandar Nanevski and
               Brigitte Pientka and
               Frank Pfenning},
  title     = {A modal foundation for meta-variables},
  booktitle = {Eighth {ACM} {SIGPLAN} International Conference on Functional Programming,
               Workshop on Mechanized reasoning about languages with variable binding,
               {MERLIN} 2003, Uppsala, Sweden, August 2003},
  year      = {2003},
  crossref  = {DBLP:conf/icfp/2003merlin},
  url       = {http://doi.acm.org/10.1145/976571.976582},
  doi       = {10.1145/976571.976582},
  timestamp = {Mon, 13 Feb 2006 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/icfp/NanevskiPP03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/ijcai/ThrunGPBSL03,
  author    = {Sebastian Thrun and
               Geoffrey J. Gordon and
               Frank Pfenning and
               Mary Berna and
               Brennan Sellner and
               Brad Lisien},
  title     = {A Learning Algorithm for Localizing People Based on Wireless Signal
               Strength that Uses Labeled and Unlabeled Data},
  booktitle = {IJCAI-03, Proceedings of the Eighteenth International Joint Conference
               on Artificial Intelligence, Acapulco, Mexico, August 9-15, 2003},
  pages     = {1427--1428},
  year      = {2003},
  crossref  = {DBLP:conf/ijcai/2003},
  url       = {http://ijcai.org/Proceedings/03/Papers/226.pdf},
  timestamp = {Thu, 25 Aug 2016 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ijcai/ThrunGPBSL03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/popl/PetersenHCP03,
  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 {POPL} 2003: The 30th {SIGPLAN-SIGACT} Symposium
               on Principles of Programming Languages, New Orleans, Louisisana, USA,
               January 15-17, 2003},
  pages     = {172--184},
  year      = {2003},
  crossref  = {DBLP:conf/popl/2003},
  url       = {http://doi.acm.org/10.1145/640128.604147},
  doi       = {10.1145/640128.604147},
  timestamp = {Tue, 14 Mar 2017 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/popl/PetersenHCP03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/tphol/SchurmannP03,
  author    = {Carsten Sch{\"{u}}rmann and
               Frank Pfenning},
  title     = {A Coverage Checking Algorithm for {LF}},
  booktitle = {Theorem Proving in Higher Order Logics, 16th International Conference,
               TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings},
  pages     = {120--135},
  year      = {2003},
  crossref  = {DBLP:conf/tphol/2003},
  url       = {https://doi.org/10.1007/10930755_8},
  doi       = {10.1007/10930755_8},
  timestamp = {Mon, 29 May 2017 16:53:44 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tphol/SchurmannP03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/types/WatkinsCPW03,
  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, International Workshop, {TYPES} 2003,
               Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers},
  pages     = {355--377},
  year      = {2003},
  crossref  = {DBLP:conf/types/2003},
  url       = {https://doi.org/10.1007/978-3-540-24849-1_23},
  doi       = {10.1007/978-3-540-24849-1_23},
  timestamp = {Thu, 15 Jun 2017 21:39:32 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/types/WatkinsCPW03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/gpce/2003,
  editor    = {Frank Pfenning and
               Yannis Smaragdakis},
  title     = {Generative Programming and Component Engineering, Second International
               Conference, {GPCE} 2003, Erfurt, Germany, September 22-25, 2003, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2830},
  publisher = {Springer},
  year      = {2003},
  url       = {https://doi.org/10.1007/b13639},
  doi       = {10.1007/b13639},
  isbn      = {3-540-20102-5},
  timestamp = {Mon, 29 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/gpce/2003},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/entcs/Pfenning02a,
  author    = {Frank Pfenning},
  title     = {Invited talk: Tri-Directional Type Checking},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {70},
  number    = {1},
  year      = {2002},
  url       = {http://www1.elsevier.com/gej-ng/31/29/23/125/51/show/Products/notes/index.htt#012},
  timestamp = {Wed, 28 Jul 2004 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/entcs/Pfenning02a},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/entcs/Pfenning02,
  author    = {Frank Pfenning},
  title     = {Preface},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {70},
  number    = {2},
  pages     = {146},
  year      = {2002},
  url       = {https://doi.org/10.1016/S1571-0661(05)80511-0},
  doi       = {10.1016/S1571-0661(05)80511-0},
  timestamp = {Sun, 28 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/entcs/Pfenning02},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/iandc/CervesatoP02,
  author    = {Iliano Cervesato and
               Frank Pfenning},
  title     = {A Linear Logical Framework},
  journal   = {Inf. Comput.},
  volume    = {179},
  number    = {1},
  pages     = {19--75},
  year      = {2002},
  url       = {https://doi.org/10.1006/inco.2001.2951},
  doi       = {10.1006/inco.2001.2951},
  timestamp = {Tue, 06 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/iandc/CervesatoP02},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/tocl/AbadiLP02,
  author    = {Mart{\'{\i}}n Abadi and
               Leonid Libkin and
               Frank Pfenning},
  title     = {Editorial},
  journal   = {{ACM} Trans. Comput. Log.},
  volume    = {3},
  number    = {3},
  pages     = {335--335},
  year      = {2002},
  url       = {http://doi.acm.org/10.1145/507382.507383},
  doi       = {10.1145/507382.507383},
  timestamp = {Fri, 21 Nov 2003 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/journals/tocl/AbadiLP02},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/grid/ChangCDHLVP02,
  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 = {Grid Computing - {GRID} 2002, Third International Workshop, Baltimore,
               MD, USA, November 18, 2002, Proceedings},
  pages     = {112--125},
  year      = {2002},
  crossref  = {DBLP:conf/grid/2002},
  url       = {https://doi.org/10.1007/3-540-36133-2_11},
  doi       = {10.1007/3-540-36133-2_11},
  timestamp = {Fri, 26 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/grid/ChangCDHLVP02},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/jacm/DaviesP01,
  author    = {Rowan Davies and
               Frank Pfenning},
  title     = {A modal analysis of staged computation},
  journal   = {J. {ACM}},
  volume    = {48},
  number    = {3},
  pages     = {555--604},
  year      = {2001},
  url       = {http://doi.acm.org/10.1145/382780.382785},
  doi       = {10.1145/382780.382785},
  timestamp = {Thu, 20 Nov 2003 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/journals/jacm/DaviesP01},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/mscs/PfenningD01,
  author    = {Frank Pfenning and
               Rowan Davies},
  title     = {A judgmental reconstruction of modal logic},
  journal   = {Mathematical Structures in Computer Science},
  volume    = {11},
  number    = {4},
  pages     = {511--540},
  year      = {2001},
  url       = {https://doi.org/10.1017/S0960129501003322},
  doi       = {10.1017/S0960129501003322},
  timestamp = {Sun, 28 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/mscs/PfenningD01},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/tcs/SchurmannDP01,
  author    = {Carsten Sch{\"{u}}rmann and
               Jo{\"{e}}lle Despeyroux and
               Frank Pfenning},
  title     = {Primitive recursion for higher-order abstract syntax},
  journal   = {Theor. Comput. Sci.},
  volume    = {266},
  number    = {1-2},
  pages     = {1--57},
  year      = {2001},
  url       = {https://doi.org/10.1016/S0304-3975(00)00418-7},
  doi       = {10.1016/S0304-3975(00)00418-7},
  timestamp = {Sun, 28 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/tcs/SchurmannDP01},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/lics/Pfenning01,
  author    = {Frank Pfenning},
  title     = {Intensionality, Extensionality, and Proof Irrelevance in Modal Type
               Theory},
  booktitle = {16th Annual {IEEE} Symposium on Logic in Computer Science, Boston,
               Massachusetts, USA, June 16-19, 2001, Proceedings},
  pages     = {221--230},
  year      = {2001},
  crossref  = {DBLP:conf/lics/2001},
  url       = {https://doi.org/10.1109/LICS.2001.932499},
  doi       = {10.1109/LICS.2001.932499},
  timestamp = {Thu, 25 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lics/Pfenning01},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@incollection{DBLP:books/el/RV01/Pfenning01,
  author    = {Frank Pfenning},
  title     = {Logical Frameworks},
  booktitle = {Handbook of Automated Reasoning (in 2 volumes)},
  pages     = {1063--1147},
  year      = {2001},
  crossref  = {DBLP:books/el/RobinsonV01},
  timestamp = {Wed, 29 Mar 2017 16:45:21 +0200},
  biburl    = {http://dblp.org/rec/bib/books/el/RV01/Pfenning01},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/corr/cs-LO-0109072,
  author    = {Alberto Momigliano and
               Frank Pfenning},
  title     = {Higher-Order Pattern Complement and the Strict Lambda-Calculus},
  journal   = {CoRR},
  volume    = {cs.LO/0109072},
  year      = {2001},
  url       = {http://arxiv.org/abs/cs.LO/0109072},
  timestamp = {Wed, 07 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/corr/cs-LO-0109072},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/corr/cs-LO-0110028,
  author    = {Robert Harper and
               Frank Pfenning},
  title     = {On Equivalence and Canonical Forms in the {LF} Type Theory},
  journal   = {CoRR},
  volume    = {cs.LO/0110028},
  year      = {2001},
  url       = {http://arxiv.org/abs/cs.LO/0110028},
  timestamp = {Wed, 07 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/corr/cs-LO-0110028},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/amai/GramlichKP00,
  author    = {Bernhard Gramlich and
               H{\'{e}}l{\`{e}}ne Kirchner and
               Frank Pfenning},
  title     = {Editorial: Strategies in Automated Deduction},
  journal   = {Ann. Math. Artif. Intell.},
  volume    = {29},
  number    = {1-4},
  pages     = {0},
  year      = {2000},
  url       = {https://doi.org/10.1023/A:1016668707781},
  doi       = {10.1023/A:1016668707781},
  timestamp = {Sun, 28 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/amai/GramlichKP00},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/iandc/Pfenning00,
  author    = {Frank Pfenning},
  title     = {Structural Cut Elimination: I. Intuitionistic and Classical Logic},
  journal   = {Inf. Comput.},
  volume    = {157},
  number    = {1-2},
  pages     = {84--141},
  year      = {2000},
  url       = {https://doi.org/10.1006/inco.1999.2832},
  doi       = {10.1006/inco.1999.2832},
  timestamp = {Thu, 18 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/iandc/Pfenning00},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/tcs/CervesatoHP00,
  author    = {Iliano Cervesato and
               Joshua S. Hodas and
               Frank Pfenning},
  title     = {Efficient resource management for linear logic proof search},
  journal   = {Theor. Comput. Sci.},
  volume    = {232},
  number    = {1-2},
  pages     = {133--163},
  year      = {2000},
  url       = {https://doi.org/10.1016/S0304-3975(99)00173-5},
  doi       = {10.1016/S0304-3975(99)00173-5},
  timestamp = {Sun, 28 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/tcs/CervesatoHP00},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/icfp/DaviesP00,
  author    = {Rowan Davies and
               Frank Pfenning},
  title     = {Intersection types and computational effects},
  booktitle = {Proceedings of the Fifth {ACM} {SIGPLAN} International Conference
               on Functional Programming {(ICFP} '00), Montreal, Canada, September
               18-21, 2000.},
  pages     = {198--208},
  year      = {2000},
  crossref  = {DBLP:conf/icfp/2000},
  url       = {http://doi.acm.org/10.1145/351240.351259},
  doi       = {10.1145/351240.351259},
  timestamp = {Tue, 11 Jun 2013 13:51:25 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/icfp/DaviesP00},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/pepm/Pfenning00,
  author    = {Frank Pfenning},
  title     = {On the Logical Foundations of Staged Computation (Abstract of Invited
               Talk)},
  booktitle = {Proceedings of the 2000 {ACM} {SIGPLAN} Workshop on Partial Evaluation
               and Semantics-Based Program Manipulation {(PEPM} '00), Boston, Massachusetts,
               USA, January 22-23, 2000},
  pages     = {33},
  year      = {2000},
  crossref  = {DBLP:conf/pepm/2000},
  url       = {http://doi.acm.org/10.1145/328690.328696},
  doi       = {10.1145/328690.328696},
  timestamp = {Tue, 22 May 2012 15:24:56 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/pepm/Pfenning00},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/saig/Pfenning00,
  author    = {Frank Pfenning},
  title     = {Reasoning about Staged Computation},
  booktitle = {Semantics, Applications, and Implementation of Program Generation,
               International Workshop {SAIG} 2000, Montreal, Canada, September 20,
               2000, Proceedings},
  pages     = {5--6},
  year      = {2000},
  crossref  = {DBLP:conf/saig/2000},
  url       = {https://doi.org/10.1007/3-540-45350-4_3},
  doi       = {10.1007/3-540-45350-4_3},
  timestamp = {Wed, 24 May 2017 15:40:45 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/saig/Pfenning00},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/entcs/PolokowP99,
  author    = {J. Polokow and
               Frank Pfenning},
  title     = {Relating Natural Deduction and Sequent Calculus for Intuitionistic
               Non-Commutative Linear Logic},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {20},
  pages     = {449--466},
  year      = {1999},
  url       = {https://doi.org/10.1016/S1571-0661(04)80088-4},
  doi       = {10.1016/S1571-0661(04)80088-4},
  timestamp = {Sun, 28 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/entcs/PolokowP99},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/entcs/DanvyDP99,
  author    = {Olivier Danvy and
               Belmina Dzafic and
               Frank Pfenning},
  title     = {On proving syntactic properties of {CPS} programs},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {26},
  pages     = {21--33},
  year      = {1999},
  url       = {https://doi.org/10.1016/S1571-0661(05)80281-6},
  doi       = {10.1016/S1571-0661(05)80281-6},
  timestamp = {Sun, 28 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/entcs/DanvyDP99},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/agp/MomiglianoP99,
  author    = {Alberto Momigliano and
               Frank Pfenning},
  title     = {The Relative Complement Problem for Higher-Order Patterns},
  booktitle = {1999 Joint Conference on Declarative Programming, AGP'99, L'Aquila,
               Italy, September 6-9, 1999},
  pages     = {497--512},
  year      = {1999},
  crossref  = {DBLP:conf/agp/1999},
  timestamp = {Wed, 01 Dec 2004 15:33:47 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/agp/MomiglianoP99},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/PfenningS99,
  author    = {Frank Pfenning and
               Carsten Sch{\"{u}}rmann},
  title     = {System Description: Twelf - {A} Meta-Logical Framework for Deductive
               Systems},
  booktitle = {Automated Deduction - CADE-16, 16th International Conference on Automated
               Deduction, Trento, Italy, July 7-10, 1999, Proceedings},
  pages     = {202--206},
  year      = {1999},
  crossref  = {DBLP:conf/cade/1999},
  url       = {https://doi.org/10.1007/3-540-48660-7_14},
  doi       = {10.1007/3-540-48660-7_14},
  timestamp = {Wed, 24 May 2017 15:40:41 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/PfenningS99},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/iclp/MomiglianoP99,
  author    = {Alberto Momigliano and
               Frank Pfenning},
  title     = {The Relative Complement Problem for Higher-Order Patterns},
  booktitle = {Logic Programming: The 1999 International Conference, Las Cruces,
               New Mexico, USA, November 29 - December 4, 1999},
  pages     = {380--394},
  year      = {1999},
  crossref  = {DBLP:conf/iclp/1999},
  timestamp = {Mon, 02 Dec 2013 17:40:45 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/iclp/MomiglianoP99},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/popl/XiP99,
  author    = {Hongwei Xi and
               Frank Pfenning},
  title     = {Dependent Types in Practical Programming},
  booktitle = {{POPL} '99, Proceedings of the 26th {ACM} {SIGPLAN-SIGACT} Symposium
               on Principles of Programming Languages, San Antonio, TX, USA, January
               20-22, 1999},
  pages     = {214--227},
  year      = {1999},
  crossref  = {DBLP:conf/popl/1999},
  url       = {http://doi.acm.org/10.1145/292540.292560},
  doi       = {10.1145/292540.292560},
  timestamp = {Mon, 21 May 2012 16:19:51 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/popl/XiP99},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/ppdp/Pfenning99,
  author    = {Frank Pfenning},
  title     = {Logical and Meta-Logical Frameworks (Abstract)},
  booktitle = {Principles and Practice of Declarative Programming, International
               Conference PPDP'99, Paris, France, September 29 - October 1, 1999,
               Proceedings},
  pages     = {206},
  year      = {1999},
  crossref  = {DBLP:conf/ppdp/1999},
  url       = {https://doi.org/10.1007/10704567_12},
  doi       = {10.1007/10704567_12},
  timestamp = {Wed, 24 May 2017 15:40:43 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ppdp/Pfenning99},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/tlca/PolakowP99,
  author    = {Jeff Polakow and
               Frank Pfenning},
  title     = {Natural Deduction for Intuitionistic Non-communicative Linear Logic},
  booktitle = {Typed Lambda Calculi and Applications, 4th International Conference,
               TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings},
  pages     = {295--309},
  year      = {1999},
  crossref  = {DBLP:conf/tlca/1999},
  url       = {https://doi.org/10.1007/3-540-48959-2_21},
  doi       = {10.1007/3-540-48959-2_21},
  timestamp = {Tue, 23 May 2017 14:54:58 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tlca/PolakowP99},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/csur/WicklineLPD98,
  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} Comput. Surv.},
  volume    = {30},
  number    = {3es},
  pages     = {8},
  year      = {1998},
  url       = {http://doi.acm.org/10.1145/289121.289129},
  doi       = {10.1145/289121.289129},
  timestamp = {Mon, 10 Dec 2012 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/journals/csur/WicklineLPD98},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/entcs/PfenningS98,
  author    = {Frank Pfenning and
               Carsten Sch{\"{u}}rmann},
  title     = {Algorithms for Equality and Unification in the Presence of Notational
               Definitions},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {17},
  pages     = {1--13},
  year      = {1998},
  url       = {https://doi.org/10.1016/S1571-0661(05)01181-3},
  doi       = {10.1016/S1571-0661(05)01181-3},
  timestamp = {Sun, 28 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/entcs/PfenningS98},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/logcom/HarperP98,
  author    = {Robert Harper and
               Frank Pfenning},
  title     = {A Module System for a Programming Language Based on the {LF} Logical
               Framework},
  journal   = {J. Log. Comput.},
  volume    = {8},
  number    = {1},
  pages     = {5--31},
  year      = {1998},
  url       = {https://doi.org/10.1093/logcom/8.1.5},
  doi       = {10.1093/logcom/8.1.5},
  timestamp = {Wed, 17 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/logcom/HarperP98},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/sLogica/SiegP98,
  author    = {Wilfried Sieg and
               Frank Pfenning},
  title     = {Note by the Guest Editors},
  journal   = {Studia Logica},
  volume    = {60},
  number    = {1},
  pages     = {1},
  year      = {1998},
  url       = {https://doi.org/10.1023/A:1005065031956},
  doi       = {10.1023/A:1005065031956},
  timestamp = {Sat, 20 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/sLogica/SiegP98},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/Pfenning98,
  author    = {Frank Pfenning},
  title     = {Reasoning About Deductions in Linear Logic (Abstract of Invited Talk)},
  booktitle = {Automated Deduction - CADE-15, 15th International Conference on Automated
               Deduction, Lindau, Germany, July 5-10, 1998, Proceedings},
  pages     = {1--2},
  year      = {1998},
  crossref  = {DBLP:conf/cade/1998},
  url       = {https://doi.org/10.1007/BFb0054240},
  doi       = {10.1007/BFb0054240},
  timestamp = {Tue, 23 May 2017 11:53:57 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/Pfenning98},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/SchurmannP98,
  author    = {Carsten Sch{\"{u}}rmann and
               Frank Pfenning},
  title     = {Automated Theorem Proving in a Simple Meta-Logic for {LF}},
  booktitle = {Automated Deduction - CADE-15, 15th International Conference on Automated
               Deduction, Lindau, Germany, July 5-10, 1998, Proceedings},
  pages     = {286--300},
  year      = {1998},
  crossref  = {DBLP:conf/cade/1998},
  url       = {https://doi.org/10.1007/BFb0054266},
  doi       = {10.1007/BFb0054266},
  timestamp = {Tue, 23 May 2017 11:53:57 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/SchurmannP98},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/pldi/WicklineLP98,
  author    = {Philip Wickline and
               Peter Lee and
               Frank Pfenning},
  title     = {Run-time Code Generation and Modal-ML},
  booktitle = {Proceedings of the {ACM} {SIGPLAN} '98 Conference on Programming Language
               Design and Implementation (PLDI), Montreal, Canada, June 17-19, 1998},
  pages     = {224--235},
  year      = {1998},
  crossref  = {DBLP:conf/pldi/1998},
  url       = {http://doi.acm.org/10.1145/277650.277727},
  doi       = {10.1145/277650.277727},
  timestamp = {Mon, 10 Dec 2012 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/pldi/WicklineLP98},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/pldi/XiP98,
  author    = {Hongwei Xi and
               Frank Pfenning},
  title     = {Eliminating Array Bound Checking Through Dependent Types},
  booktitle = {Proceedings of the {ACM} {SIGPLAN} '98 Conference on Programming Language
               Design and Implementation (PLDI), Montreal, Canada, June 17-19, 1998},
  pages     = {249--257},
  year      = {1998},
  crossref  = {DBLP:conf/pldi/1998},
  url       = {http://doi.acm.org/10.1145/277650.277732},
  doi       = {10.1145/277650.277732},
  timestamp = {Mon, 21 May 2012 16:19:53 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/pldi/XiP98},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/types/PfenningS98,
  author    = {Frank Pfenning and
               Carsten Sch{\"{u}}rmann},
  title     = {Algorithms for Equality and Unification in the Presence of Notational
               Definitions},
  booktitle = {Types for Proofs and Programs, International Workshop {TYPES} '98,
               Kloster Irsee, Germany, March 27-31, 1998, Selected Papers},
  pages     = {179--193},
  year      = {1998},
  crossref  = {DBLP:conf/types/1998},
  url       = {https://doi.org/10.1007/3-540-48167-2_13},
  doi       = {10.1007/3-540-48167-2_13},
  timestamp = {Wed, 24 May 2017 15:40:43 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/types/PfenningS98},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/jsyml/NarendranPS97,
  author    = {Paliath Narendran and
               Frank Pfenning and
               Richard Statman},
  title     = {On the Unification Problem for Cartesian Closed Categories},
  journal   = {J. Symb. Log.},
  volume    = {62},
  number    = {2},
  pages     = {636--647},
  year      = {1997},
  url       = {https://doi.org/10.2307/2275552},
  doi       = {10.2307/2275552},
  timestamp = {Sun, 28 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/jsyml/NarendranPS97},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/lics/CervesatoP97,
  author    = {Iliano Cervesato and
               Frank Pfenning},
  title     = {Linear Higher-Order Pre-Unification},
  booktitle = {Proceedings, 12th Annual {IEEE} Symposium on Logic in Computer Science,
               Warsaw, Poland, June 29 - July 2, 1997},
  pages     = {422--433},
  year      = {1997},
  crossref  = {DBLP:conf/lics/1997},
  url       = {https://doi.org/10.1109/LICS.1997.614967},
  doi       = {10.1109/LICS.1997.614967},
  timestamp = {Thu, 25 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lics/CervesatoP97},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/tlca/DespeyrouxPS97,
  author    = {Jo{\"{e}}lle Despeyroux and
               Frank Pfenning and
               Carsten Sch{\"{u}}rmann},
  title     = {Primitive Recursion for Higher-Order Abstract Syntax},
  booktitle = {Typed Lambda Calculi and Applications, Third International Conference
               on Typed Lambda Calculi and Applications, {TLCA} '97, Nancy, France,
               April 2-4, 1997, Proceedings},
  pages     = {147--163},
  year      = {1997},
  crossref  = {DBLP:conf/tlca/1997},
  url       = {https://doi.org/10.1007/3-540-62688-3_34},
  doi       = {10.1007/3-540-62688-3_34},
  timestamp = {Mon, 22 May 2017 17:11:16 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tlca/DespeyrouxPS97},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/jar/AndrewsBINPX96,
  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   = {J. Autom. Reasoning},
  volume    = {16},
  number    = {3},
  pages     = {321--353},
  year      = {1996},
  url       = {https://doi.org/10.1007/BF00252180},
  doi       = {10.1007/BF00252180},
  timestamp = {Sat, 20 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/jar/AndrewsBINPX96},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/caap/Pfenning96,
  author    = {Frank Pfenning},
  title     = {The Practice of Logical Frameworks},
  booktitle = {Trees in Algebra and Programming - CAAP'96, 21st International Colloquium,
               Link{\"{o}}ping, Sweden, April, 22-24, 1996, Proceedings},
  pages     = {119--134},
  year      = {1996},
  crossref  = {DBLP:conf/caap/1996},
  url       = {https://doi.org/10.1007/3-540-61064-2_33},
  doi       = {10.1007/3-540-61064-2_33},
  timestamp = {Mon, 22 May 2017 16:14:06 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/caap/Pfenning96},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/elp/CervesatoHP96,
  author    = {Iliano Cervesato and
               Joshua S. Hodas and
               Frank Pfenning},
  title     = {Efficient Resource Management for Linear Logic Proof Search},
  booktitle = {Extensions of Logic Programming, 5th International Workshop, ELP'96,
               Leipzig, Germany, March 28-30, 1996, Proceedings},
  pages     = {67--81},
  year      = {1996},
  crossref  = {DBLP:conf/elp/1996},
  url       = {https://doi.org/10.1007/3-540-60983-0_5},
  doi       = {10.1007/3-540-60983-0_5},
  timestamp = {Mon, 22 May 2017 16:14:04 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/elp/CervesatoHP96},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/esop/RohwedderP96,
  author    = {Ekkehard Rohwedder and
               Frank Pfenning},
  title     = {Mode and Termination Checking for Higher-Order Logic Programs},
  booktitle = {Programming Languages and Systems - ESOP'96, 6th European Symposium
               on Programming, Link{\"{o}}ping, Sweden, April 22-24, 1996, Proceedings},
  pages     = {296--310},
  year      = {1996},
  crossref  = {DBLP:conf/esop/1996},
  url       = {https://doi.org/10.1007/3-540-61055-3_44},
  doi       = {10.1007/3-540-61055-3_44},
  timestamp = {Mon, 22 May 2017 16:14:04 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/esop/RohwedderP96},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/iclp/DowekHKP96,
  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 = {Logic Programming, Proceedings of the 1996 Joint International Conference
               and Symposium on Logic Programming, Bonn, Germany, September 2-6,
               1996},
  pages     = {259--273},
  year      = {1996},
  crossref  = {DBLP:conf/iclp/1996},
  url       = {http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6278922},
  timestamp = {Thu, 17 Aug 2017 12:43:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/iclp/DowekHKP96},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/lics/CervesatoP96,
  author    = {Iliano Cervesato and
               Frank Pfenning},
  title     = {A Linear Logical Framework},
  booktitle = {Proceedings, 11th Annual {IEEE} Symposium on Logic in Computer Science,
               New Brunswick, New Jersey, USA, July 27-30, 1996},
  pages     = {264--275},
  year      = {1996},
  crossref  = {DBLP:conf/lics/1996},
  url       = {https://doi.org/10.1109/LICS.1996.561339},
  doi       = {10.1109/LICS.1996.561339},
  timestamp = {Thu, 25 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lics/CervesatoP96},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/popl/DaviesP96,
  author    = {Rowan Davies and
               Frank Pfenning},
  title     = {A Modal Analysis of Staged Computation},
  booktitle = {Conference Record of POPL'96: The 23rd {ACM} {SIGPLAN-SIGACT} Symposium
               on Principles of Programming Languages, Papers Presented at the Symposium,
               St. Petersburg Beach, Florida, USA, January 21-24, 1996},
  pages     = {258--270},
  year      = {1996},
  crossref  = {DBLP:conf/popl/1996},
  url       = {http://doi.acm.org/10.1145/237721.237788},
  doi       = {10.1145/237721.237788},
  timestamp = {Mon, 21 May 2012 16:19:50 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/popl/DaviesP96},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/entcs/PfenningW95,
  author    = {Frank Pfenning and
               Hao{-}Chi Wong},
  title     = {On a modal lambda calculus for {S4}},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {1},
  pages     = {515--534},
  year      = {1995},
  url       = {https://doi.org/10.1016/S1571-0661(04)00028-3},
  doi       = {10.1016/S1571-0661(04)00028-3},
  timestamp = {Sun, 28 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/entcs/PfenningW95},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/lics/Pfenning95,
  author    = {Frank Pfenning},
  title     = {Structural Cut Elimination},
  booktitle = {Proceedings, 10th Annual {IEEE} Symposium on Logic in Computer Science,
               San Diego, California, USA, June 26-29, 1995},
  pages     = {156--166},
  year      = {1995},
  crossref  = {DBLP:conf/lics/1995},
  url       = {https://doi.org/10.1109/LICS.1995.523253},
  doi       = {10.1109/LICS.1995.523253},
  timestamp = {Thu, 25 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lics/Pfenning95},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/Pfenning94,
  author    = {Frank Pfenning},
  title     = {Elf: {A} Meta-Language for Deductive Systems (System Descrition)},
  booktitle = {Automated Deduction - CADE-12, 12th International Conference on Automated
               Deduction, Nancy, France, June 26 - July 1, 1994, Proceedings},
  pages     = {811--815},
  year      = {1994},
  crossref  = {DBLP:conf/cade/1994},
  url       = {https://doi.org/10.1007/3-540-58156-1_66},
  doi       = {10.1007/3-540-58156-1_66},
  timestamp = {Sat, 20 May 2017 15:32:47 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/Pfenning94},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/1994,
  editor    = {Frank Pfenning},
  title     = {Logic Programming and Automated Reasoning, 5th International Conference,
               LPAR'94, Kiev, Ukraine, July 16-22, 1994, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {822},
  publisher = {Springer},
  year      = {1994},
  url       = {https://doi.org/10.1007/3-540-58216-9},
  doi       = {10.1007/3-540-58216-9},
  isbn      = {3-540-58216-9},
  timestamp = {Sat, 20 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/1994},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/fuin/Pfenning93,
  author    = {Frank Pfenning},
  title     = {On the Undecidability of Partial Polymorphic Type Reconstruction},
  journal   = {Fundam. Inform.},
  volume    = {19},
  number    = {1/2},
  pages     = {185--199},
  year      = {1993},
  timestamp = {Thu, 27 Nov 2003 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/journals/fuin/Pfenning93},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/lics/NarendranPS93,
  author    = {Paliath Narendran and
               Frank Pfenning and
               Richard Statman},
  title     = {On the Unification Problem for Cartesian Closed Categories},
  booktitle = {Proceedings of the Eighth Annual Symposium on Logic in Computer Science
               {(LICS} '93), Montreal, Canada, June 19-23, 1993},
  pages     = {57--63},
  year      = {1993},
  crossref  = {DBLP:conf/lics/1993},
  url       = {https://doi.org/10.1109/LICS.1993.287600},
  doi       = {10.1109/LICS.1993.287600},
  timestamp = {Thu, 25 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lics/NarendranPS93},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/ppcp/MichaylovP93,
  author    = {Spiro Michaylov and
               Frank Pfenning},
  title     = {Higher-Order Logic Programming as Constraint Logic Programming},
  booktitle = {{PPCP}},
  pages     = {210--218},
  year      = {1993},
  timestamp = {Thu, 03 Jan 2002 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/ppcp/MichaylovP93},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/slp/KohlhaseP93,
  author    = {Michael Kohlhase and
               Frank Pfenning},
  title     = {Unification in a Lambda-Calculus with Intersection Types},
  booktitle = {Logic Programming, Proceedings of the 1993 International Symposium,
               Vancouver, British Columbia, Canada, October 26-29, 1993},
  pages     = {488--505},
  year      = {1993},
  crossref  = {DBLP:conf/slp/1993},
  timestamp = {Sun, 12 Nov 2017 16:01:30 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/slp/KohlhaseP93},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/tphol/AndrewsBINPX93,
  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 = {Higher Order Logic Theorem Proving and its Applications, 6th International
               Workshop, {HUG} '93, Vancouver, BC, Canada, August 11-13, 1993, Proceedings},
  pages     = {366--370},
  year      = {1993},
  crossref  = {DBLP:conf/tphol/1993},
  url       = {https://doi.org/10.1007/3-540-57826-9_148},
  doi       = {10.1007/3-540-57826-9_148},
  timestamp = {Sat, 20 May 2017 15:32:54 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tphol/AndrewsBINPX93},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/ml/DietzenP92,
  author    = {Scott Dietzen and
               Frank Pfenning},
  title     = {Higher-Order and Modal Logic as a Framework for Explanation-Based
               Generalization},
  journal   = {Machine Learning},
  volume    = {9},
  pages     = {23--55},
  year      = {1992},
  url       = {https://doi.org/10.1007/BF00993253},
  doi       = {10.1007/BF00993253},
  timestamp = {Sun, 28 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/ml/DietzenP92},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/PfenningR92,
  author    = {Frank Pfenning and
               Ekkehard Rohwedder},
  title     = {Implementing the Meta-Theory of Deductive Systems},
  booktitle = {Automated Deduction - CADE-11, 11th International Conference on Automated
               Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings},
  pages     = {537--551},
  year      = {1992},
  crossref  = {DBLP:conf/cade/1992},
  url       = {https://doi.org/10.1007/3-540-55602-8_190},
  doi       = {10.1007/3-540-55602-8_190},
  timestamp = {Sat, 20 May 2017 15:32:46 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/PfenningR92},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/lics/PfenningH92,
  author    = {John Hannan and
               Frank Pfenning},
  title     = {Compiler Verification in {LF}},
  booktitle = {Proceedings of the Seventh Annual Symposium on Logic in Computer Science
               {(LICS} '92), Santa Cruz, California, USA, June 22-25, 1992},
  pages     = {407--418},
  year      = {1992},
  crossref  = {DBLP:conf/lics/1992},
  url       = {https://doi.org/10.1109/LICS.1992.185552},
  doi       = {10.1109/LICS.1992.185552},
  timestamp = {Thu, 25 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lics/PfenningH92},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@incollection{DBLP:books/mit/pfenning92/NadathurP92,
  author    = {Gopalan Nadathur and
               Frank Pfenning},
  title     = {The Type System of a Higher-Order Logic Programming Language},
  booktitle = {Types in Logic Programming},
  pages     = {245--283},
  year      = {1992},
  timestamp = {Thu, 03 Jan 2002 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/books/mit/pfenning92/NadathurP92},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@incollection{DBLP:books/mit/pfenning92/Pfenning92,
  author    = {Frank Pfenning},
  title     = {Dependent Types in Logic Programming},
  booktitle = {Types in Logic Programming},
  pages     = {285--311},
  year      = {1992},
  timestamp = {Thu, 03 Jan 2002 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/books/mit/pfenning92/Pfenning92},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/apal/MillerNPS91,
  author    = {Dale Miller and
               Gopalan Nadathur and
               Frank Pfenning and
               Andre Scedrov},
  title     = {Uniform Proofs as a Foundation for Logic Programming},
  journal   = {Ann. Pure Appl. Logic},
  volume    = {51},
  number    = {1-2},
  pages     = {125--157},
  year      = {1991},
  url       = {https://doi.org/10.1016/0168-0072(91)90068-W},
  doi       = {10.1016/0168-0072(91)90068-W},
  timestamp = {Sun, 12 Nov 2017 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/journals/apal/MillerNPS91},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/tcs/PfenningL91,
  author    = {Frank Pfenning and
               Peter Lee},
  title     = {Metacircularity in the Polymorphic lambda-Calculus},
  journal   = {Theor. Comput. Sci.},
  volume    = {89},
  number    = {1},
  pages     = {137--159},
  year      = {1991},
  url       = {https://doi.org/10.1016/0304-3975(90)90109-U},
  doi       = {10.1016/0304-3975(90)90109-U},
  timestamp = {Sun, 28 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/tcs/PfenningL91},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/elp/MichaylovP91,
  author    = {Spiro Michaylov and
               Frank Pfenning},
  title     = {Natural Semantics and Some of Its Meta-Theory in Elf},
  booktitle = {Extensions of Logic Programming, Second International Workshop, ELP'91,
               Stockholm, Sweden, January 27-29, 1991, Proceedings},
  pages     = {299--344},
  year      = {1991},
  crossref  = {DBLP:conf/elp/1991},
  url       = {https://doi.org/10.1007/BFb0013612},
  doi       = {10.1007/BFb0013612},
  timestamp = {Sat, 20 May 2017 15:32:49 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/elp/MichaylovP91},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/lics/Pfenning91,
  author    = {Frank Pfenning},
  title     = {Unification and Anti-Unification in the Calculus of Constructions},
  booktitle = {Proceedings of the Sixth Annual Symposium on Logic in Computer Science
               {(LICS} '91), Amsterdam, The Netherlands, July 15-18, 1991},
  pages     = {74--85},
  year      = {1991},
  crossref  = {DBLP:conf/lics/1991},
  url       = {https://doi.org/10.1109/LICS.1991.151632},
  doi       = {10.1109/LICS.1991.151632},
  timestamp = {Thu, 25 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lics/Pfenning91},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/pepm/MichaylovP91,
  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, PEPM'91, Yale University, New Haven, Connecticut,
               USA, June 17-19, 1991},
  pages     = {285--296},
  year      = {1991},
  crossref  = {DBLP:conf/pepm/1991},
  url       = {http://doi.acm.org/10.1145/115865.115896},
  doi       = {10.1145/115865.115896},
  timestamp = {Tue, 22 May 2012 15:24:56 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/pepm/MichaylovP91},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/pldi/FreemanP91,
  author    = {Timothy S. Freeman and
               Frank Pfenning},
  title     = {Refinement Types for {ML}},
  booktitle = {Proceedings of the {ACM} SIGPLAN'91 Conference on Programming Language
               Design and Implementation (PLDI), Toronto, Ontario, Canada, June 26-28,
               1991},
  pages     = {268--277},
  year      = {1991},
  crossref  = {DBLP:conf/pldi/1991},
  url       = {http://doi.acm.org/10.1145/113445.113468},
  doi       = {10.1145/113445.113468},
  timestamp = {Wed, 30 Nov 2016 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/pldi/FreemanP91},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/slp/DietzenP91,
  author    = {Scott Dietzen and
               Frank Pfenning},
  title     = {A Declarative Alternative to "Assert" in Logic Programming},
  booktitle = {Logic Programming, Proceedings of the 1991 International Symposium,
               San Diego, California, USA, Oct. 28 - Nov 1, 1991},
  pages     = {372--386},
  year      = {1991},
  crossref  = {DBLP:conf/slp/1991},
  timestamp = {Wed, 04 Dec 2013 14:42:58 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/slp/DietzenP91},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/PfenningN90,
  author    = {Frank Pfenning and
               Dan Nesmith},
  title     = {Presenting Intuitive Deductions via Symmetric Simplification},
  booktitle = {10th International Conference on Automated Deduction, Kaiserslautern,
               FRG, July 24-27, 1990, Proceedings},
  pages     = {336--350},
  year      = {1990},
  crossref  = {DBLP:conf/cade/1990},
  url       = {https://doi.org/10.1007/3-540-52885-7_98},
  doi       = {10.1007/3-540-52885-7_98},
  timestamp = {Fri, 19 May 2017 13:10:45 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/PfenningN90},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/AndrewsINP90,
  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, Kaiserslautern,
               FRG, July 24-27, 1990, Proceedings},
  pages     = {641--642},
  year      = {1990},
  crossref  = {DBLP:conf/cade/1990},
  url       = {https://doi.org/10.1007/3-540-52885-7_120},
  doi       = {10.1007/3-540-52885-7_120},
  timestamp = {Fri, 19 May 2017 13:10:45 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/AndrewsINP90},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/FeltyGMP90,
  author    = {Amy P. Felty and
               Elsa L. Gunter and
               Dale Miller and
               Frank Pfenning},
  title     = {Tutorial on Lambda-Prolog},
  booktitle = {10th International Conference on Automated Deduction, Kaiserslautern,
               FRG, July 24-27, 1990, Proceedings},
  pages     = {682},
  year      = {1990},
  crossref  = {DBLP:conf/cade/1990},
  url       = {https://doi.org/10.1007/3-540-52885-7_142},
  doi       = {10.1007/3-540-52885-7_142},
  timestamp = {Sun, 12 Nov 2017 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/cade/FeltyGMP90},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/iclp/Pfenning90,
  author    = {Frank Pfenning},
  title     = {Types in Logic Programming},
  booktitle = {Logic Programming, Proceedings of the Seventh International Conference,
               Jerusalem, Israel, June 18-20, 1990},
  pages     = {786},
  year      = {1990},
  crossref  = {DBLP:conf/iclp/1990},
  timestamp = {Fri, 29 Nov 2013 14:57:24 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/iclp/Pfenning90},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/icml/DietzenP89,
  author    = {Scott Dietzen and
               Frank Pfenning},
  title     = {Higher-Order and Modal Logic as a Framework for Explanation-Based
               Generalization},
  booktitle = {Proceedings of the Sixth International Workshop on Machine Learning
               {(ML} 1989), Cornell University, Ithaca, New York, USA, June 26-27,
               1989},
  pages     = {447--449},
  year      = {1989},
  crossref  = {DBLP:conf/icml/1989},
  timestamp = {Thu, 05 Dec 2002 12:38:01 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/icml/DietzenP89},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/lics/Pfenning89,
  author    = {Frank Pfenning},
  title     = {Elf: {A} Language for Logic Definition and Verified Metaprogramming},
  booktitle = {Proceedings of the Fourth Annual Symposium on Logic in Computer Science
               {(LICS} '89), Pacific Grove, California, USA, June 5-8, 1989},
  pages     = {313--322},
  year      = {1989},
  crossref  = {DBLP:conf/lics/1989},
  url       = {https://doi.org/10.1109/LICS.1989.39186},
  doi       = {10.1109/LICS.1989.39186},
  timestamp = {Thu, 25 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lics/Pfenning89},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/mfps/PfenningP89,
  author    = {Frank Pfenning and
               Christine Paulin{-}Mohring},
  title     = {Inductively Defined Types in the Calculus of Constructions},
  booktitle = {Mathematical Foundations of Programming Semantics, 5th International
               Conference, Tulane University, New Orleans, Louisiana, USA, March
               29 - April 1, 1989, Proceedings},
  pages     = {209--228},
  year      = {1989},
  crossref  = {DBLP:conf/mfps/1989},
  url       = {https://doi.org/10.1007/BFb0040259},
  doi       = {10.1007/BFb0040259},
  timestamp = {Fri, 19 May 2017 13:10:47 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/mfps/PfenningP89},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/tapsoft/PfenningL89,
  author    = {Frank Pfenning and
               Peter Lee},
  title     = {{LEAP:} {A} Language with Eval And Polymorphism},
  booktitle = {TAPSOFT'89: Proceedings of the International Joint Conference on Theory
               and Practice of Software Development, Barcelona, Spain, March 13-17,
               1989, Volume 2: Advanced Seminar on Foundations of Innovative Software
               Development {II} and Colloquium on Current Issues in Programming Languages
               {(CCIPL)}},
  pages     = {345--359},
  year      = {1989},
  crossref  = {DBLP:conf/tapsoft/1989-2},
  url       = {https://doi.org/10.1007/3-540-50940-2_46},
  doi       = {10.1007/3-540-50940-2_46},
  timestamp = {Fri, 19 May 2017 13:10:47 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tapsoft/PfenningL89},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/Pfenning88,
  author    = {Frank Pfenning},
  title     = {Single Axioms in the Implicational Propositional Calculus},
  booktitle = {9th International Conference on Automated Deduction, Argonne, Illinois,
               USA, May 23-26, 1988, Proceedings},
  pages     = {710--713},
  year      = {1988},
  crossref  = {DBLP:conf/cade/1988},
  url       = {https://doi.org/10.1007/BFb0012869},
  doi       = {10.1007/BFb0012869},
  timestamp = {Fri, 19 May 2017 13:10:45 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/Pfenning88},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/AndrewsINP88,
  author    = {Peter B. Andrews and
               Sunil Issar and
               Daniel Nesmith and
               Frank Pfenning},
  title     = {The {TPS} Theorem Proving System},
  booktitle = {9th International Conference on Automated Deduction, Argonne, Illinois,
               USA, May 23-26, 1988, Proceedings},
  pages     = {760--761},
  year      = {1988},
  crossref  = {DBLP:conf/cade/1988},
  url       = {https://doi.org/10.1007/BFb0012885},
  doi       = {10.1007/BFb0012885},
  timestamp = {Fri, 19 May 2017 13:10:45 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/AndrewsINP88},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/lfp/Pfenning88,
  author    = {Frank Pfenning},
  title     = {Partial Polymorphic Type Inference and Higher-Order Unification},
  booktitle = {{LISP} and Functional Programming},
  pages     = {153--163},
  year      = {1988},
  url       = {http://doi.acm.org/10.1145/62678.62697},
  doi       = {10.1145/62678.62697},
  timestamp = {Mon, 16 Dec 2002 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/lfp/Pfenning88},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/pldi/PfenningE88,
  author    = {Frank Pfenning and
               Conal Elliott},
  title     = {Higher-Order Abstract Syntax},
  booktitle = {Proceedings of the {ACM} SIGPLAN'88 Conference on Programming Language
               Design and Implementation (PLDI), Atlanta, Georgia, USA, June 22-24,
               1988},
  pages     = {199--208},
  year      = {1988},
  crossref  = {DBLP:conf/pldi/1988},
  url       = {http://doi.acm.org/10.1145/53990.54010},
  doi       = {10.1145/53990.54010},
  timestamp = {Mon, 21 May 2012 16:19:53 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/pldi/PfenningE88},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/sde/LeePRS88,
  author    = {Peter Lee and
               Frank Pfenning and
               Gene Rollins and
               William L. 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, Boston, Massachusetts,
               USA, November 28-30, 1988},
  pages     = {25--34},
  year      = {1988},
  crossref  = {DBLP:conf/sde/1988},
  url       = {http://doi.acm.org/10.1145/64135.65006},
  doi       = {10.1145/64135.65006},
  timestamp = {Mon, 10 Dec 2012 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/sde/LeePRS88},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/sde/NordP88,
  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, Boston, Massachusetts,
               USA, November 28-30, 1988},
  pages     = {110--120},
  year      = {1988},
  crossref  = {DBLP:conf/sde/1988},
  url       = {http://doi.acm.org/10.1145/64135.65014},
  doi       = {10.1145/64135.65014},
  timestamp = {Tue, 22 May 2012 15:24:55 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/sde/NordP88},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/AndrewsPIK86,
  author    = {Peter B. Andrews and
               Frank Pfenning and
               Sunil Issar and
               C. P. Klapper},
  title     = {The {TPS} Theorem Proving System},
  booktitle = {8th International Conference on Automated Deduction, Oxford, England,
               July 27 - August 1, 1986, Proceedings},
  pages     = {663--664},
  year      = {1986},
  crossref  = {DBLP:conf/cade/1986},
  url       = {https://doi.org/10.1007/3-540-16780-3_128},
  doi       = {10.1007/3-540-16780-3_128},
  timestamp = {Fri, 19 May 2017 12:26:18 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/AndrewsPIK86},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/Pfenning84,
  author    = {Frank Pfenning},
  title     = {Analytic and Non-analytic Proofs},
  booktitle = {7th International Conference on Automated Deduction, Napa, California,
               USA, May 14-16, 1984, Proceedings},
  pages     = {394--413},
  year      = {1984},
  crossref  = {DBLP:conf/cade/1984},
  url       = {https://doi.org/10.1007/978-0-387-34768-4_23},
  doi       = {10.1007/978-0-387-34768-4_23},
  timestamp = {Fri, 19 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/Pfenning84},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/aplas/2016,
  editor    = {Atsushi Igarashi},
  title     = {Programming Languages and Systems - 14th Asian Symposium, {APLAS}
               2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {10017},
  year      = {2016},
  url       = {https://doi.org/10.1007/978-3-319-47958-3},
  doi       = {10.1007/978-3-319-47958-3},
  isbn      = {978-3-319-47957-6},
  timestamp = {Fri, 19 May 2017 01:25:54 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/aplas/2016},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/popl/2016,
  editor    = {Rastislav Bod{\'{\i}}k and
               Rupak Majumdar},
  title     = {Proceedings of the 43rd Annual {ACM} {SIGPLAN-SIGACT} Symposium on
               Principles of Programming Languages, {POPL} 2016, St. Petersburg,
               FL, USA, January 20 - 22, 2016},
  publisher = {{ACM}},
  year      = {2016},
  url       = {http://dl.acm.org/citation.cfm?id=2837614},
  isbn      = {978-1-4503-3549-2},
  timestamp = {Wed, 09 Mar 2016 08:11:59 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/popl/2016},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:journals/corr/Kobayashi17,
  editor    = {Naoki Kobayashi},
  title     = {Proceedings Eighth Workshop on Intersection Types and Related Systems,
               {ITRS} 2016, Porto, Portugal, 26th June 2016},
  series    = {{EPTCS}},
  volume    = {242},
  year      = {2017},
  url       = {https://doi.org/10.4204/EPTCS.242},
  doi       = {10.4204/EPTCS.242},
  timestamp = {Wed, 03 May 2017 14:47:57 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/corr/Kobayashi17},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:journals/corr/CervesatoF17,
  editor    = {Iliano Cervesato and
               Maribel Fern{\'{a}}ndez},
  title     = {Proceedings Fourth International Workshop on Linearity, {LINEARITY}
               2016, Porto, Portugal, 25 June 2016},
  series    = {{EPTCS}},
  volume    = {238},
  year      = {2017},
  url       = {https://doi.org/10.4204/EPTCS.238},
  doi       = {10.4204/EPTCS.238},
  timestamp = {Wed, 03 May 2017 14:47:56 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/corr/CervesatoF17},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/agere/2015,
  editor    = {Elisa Gonzalez Boix and
               Philipp Haller and
               Alessandro Ricci and
               Carlos Varela},
  title     = {Proceedings of the 5th International Workshop on Programming Based
               on Actors, Agents, and Decentralized Control, AGERE! 2015, Pittsburgh,
               PA, USA, October 26, 2015},
  publisher = {{ACM}},
  year      = {2015},
  url       = {http://doi.acm.org/10.1145/2824815},
  doi       = {10.1145/2824815},
  isbn      = {978-1-4503-3901-8},
  timestamp = {Tue, 03 Nov 2015 15:26:34 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/agere/2015},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/fossacs/2015,
  editor    = {Andrew M. Pitts},
  title     = {Foundations of Software Science and Computation Structures - 18th
               International Conference, FoSSaCS 2015, Held as Part of the European
               Joint Conferences on Theory and Practice of Software, {ETAPS} 2015,
               London, UK, April 11-18, 2015. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {9034},
  publisher = {Springer},
  year      = {2015},
  url       = {https://doi.org/10.1007/978-3-662-46678-0},
  doi       = {10.1007/978-3-662-46678-0},
  isbn      = {978-3-662-46677-3},
  timestamp = {Fri, 02 Jun 2017 20:48:43 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/fossacs/2015},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/popl/2015plmw,
  title     = {Proceedings of the Programming Languages Mentoring Workshop, PLMW@POPL
               2015, Mumbai, India, January 14, 2015},
  publisher = {{ACM}},
  year      = {2015},
  url       = {http://dl.acm.org/citation.cfm?id=2792434},
  isbn      = {978-1-4503-3299-6},
  timestamp = {Tue, 23 Jun 2015 20:35:55 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/popl/2015plmw},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/tgc/2014,
  editor    = {Matteo Maffei and
               Emilio Tuosto},
  title     = {Trustworthy Global Computing - 9th International Symposium, {TGC}
               2014, Rome, Italy, September 5-6, 2014. Revised Selected Papers},
  series    = {Lecture Notes in Computer Science},
  volume    = {8902},
  publisher = {Springer},
  year      = {2014},
  url       = {https://doi.org/10.1007/978-3-662-45917-1},
  doi       = {10.1007/978-3-662-45917-1},
  isbn      = {978-3-662-45916-4},
  timestamp = {Sun, 21 May 2017 00:19:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tgc/2014},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/esop/2013,
  editor    = {Matthias Felleisen and
               Philippa Gardner},
  title     = {Programming Languages and Systems - 22nd European Symposium on Programming,
               {ESOP} 2013, Held as Part of the European Joint Conferences on Theory
               and Practice of Software, {ETAPS} 2013, Rome, Italy, March 16-24,
               2013. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {7792},
  publisher = {Springer},
  year      = {2013},
  url       = {https://doi.org/10.1007/978-3-642-37036-6},
  doi       = {10.1007/978-3-642-37036-6},
  isbn      = {978-3-642-37035-9},
  timestamp = {Fri, 19 May 2017 01:25:18 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/esop/2013},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/csl/2012,
  editor    = {Patrick C{\'{e}}gielski and
               Arnaud Durand},
  title     = {Computer Science Logic (CSL'12) - 26th International Workshop/21st
               Annual Conference of the EACSL, {CSL} 2012, September 3-6, 2012, Fontainebleau,
               France},
  series    = {LIPIcs},
  volume    = {16},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  year      = {2012},
  url       = {http://drops.dagstuhl.de/opus/portals/extern/index.php?semnr=12009},
  isbn      = {978-3-939897-42-2},
  timestamp = {Sun, 08 Nov 2015 18:33:34 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/csl/2012},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/esop/2012,
  editor    = {Helmut Seidl},
  title     = {Programming Languages and Systems - 21st European Symposium on Programming,
               {ESOP} 2012, Held as Part of the European Joint Conferences on Theory
               and Practice of Software, {ETAPS} 2012, Tallinn, Estonia, March 24
               - April 1, 2012. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {7211},
  publisher = {Springer},
  year      = {2012},
  url       = {https://doi.org/10.1007/978-3-642-28869-2},
  doi       = {10.1007/978-3-642-28869-2},
  isbn      = {978-3-642-28868-5},
  timestamp = {Fri, 19 May 2017 01:25:18 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/esop/2012},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/fossacs/2012,
  editor    = {Lars Birkedal},
  title     = {Foundations of Software Science and Computational Structures - 15th
               International Conference, {FOSSACS} 2012, Held as Part of the European
               Joint Conferences on Theory and Practice of Software, {ETAPS} 2012,
               Tallinn, Estonia, March 24 - April 1, 2012. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {7213},
  publisher = {Springer},
  year      = {2012},
  url       = {https://doi.org/10.1007/978-3-642-28729-9},
  doi       = {10.1007/978-3-642-28729-9},
  isbn      = {978-3-642-28728-2},
  timestamp = {Tue, 23 May 2017 01:08:04 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/fossacs/2012},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/tldi/2012,
  editor    = {Benjamin C. Pierce},
  title     = {Proceedings of {TLDI} 2012: The Seventh {ACM} {SIGPLAN} Workshop on
               Types in Languages Design and Implementation, Philadelphia, PA, USA,
               Saturday, January 28, 2012},
  publisher = {{ACM}},
  year      = {2012},
  url       = {http://dl.acm.org/citation.cfm?id=2103786},
  isbn      = {978-1-4503-1120-5},
  timestamp = {Fri, 18 May 2012 21:46:11 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tldi/2012},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cpp/2011,
  editor    = {Jean{-}Pierre Jouannaud and
               Zhong Shao},
  title     = {Certified Programs and Proofs - First International Conference, {CPP}
               2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {7086},
  publisher = {Springer},
  year      = {2011},
  url       = {https://doi.org/10.1007/978-3-642-25379-9},
  doi       = {10.1007/978-3-642-25379-9},
  isbn      = {978-3-642-25378-2},
  timestamp = {Thu, 25 May 2017 00:42:11 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cpp/2011},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/ppdp/2011,
  editor    = {Peter Schneider{-}Kamp and
               Michael Hanus},
  title     = {Proceedings of the 13th International {ACM} {SIGPLAN} Conference on
               Principles and Practice of Declarative Programming, July 20-22, 2011,
               Odense, Denmark},
  publisher = {{ACM}},
  year      = {2011},
  isbn      = {978-1-4503-0776-5},
  timestamp = {Tue, 18 Oct 2011 19:19:37 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ppdp/2011},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/stm/2011,
  editor    = {Catherine A. Meadows and
               M. Carmen Fern{\'{a}}ndez Gago},
  title     = {Security and Trust Management - 7th International Workshop, {STM}
               2011, Copenhagen, Denmark, June 27-28, 2011, Revised Selected Papers},
  series    = {Lecture Notes in Computer Science},
  volume    = {7170},
  publisher = {Springer},
  year      = {2012},
  url       = {https://doi.org/10.1007/978-3-642-29963-6},
  doi       = {10.1007/978-3-642-29963-6},
  isbn      = {978-3-642-29962-9},
  timestamp = {Wed, 24 May 2017 08:30:51 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/stm/2011},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/concur/2010,
  editor    = {Paul Gastin and
               Fran{\c{c}}ois Laroussinie},
  title     = {{CONCUR} 2010 - Concurrency Theory, 21th International Conference,
               {CONCUR} 2010, Paris, France, August 31-September 3, 2010. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {6269},
  publisher = {Springer},
  year      = {2010},
  url       = {https://doi.org/10.1007/978-3-642-15375-4},
  doi       = {10.1007/978-3-642-15375-4},
  isbn      = {978-3-642-15374-7},
  timestamp = {Tue, 23 May 2017 01:11:19 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/concur/2010},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lics/2010lam,
  editor    = {Berndt M{\"{u}}ller},
  title     = {3rd International Workshop on Logics, Agents, and Mobility, LAM'10,
               Edinburgh, UK, July 14, 2010},
  series    = {EPiC Series in Computing},
  volume    = {7},
  publisher = {EasyChair},
  year      = {2012},
  url       = {http://www.easychair.org/publications/?page=451148882},
  timestamp = {Thu, 16 Jun 2016 17:11:03 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lics/2010lam},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/sp/2010,
  title     = {31st {IEEE} Symposium on Security and Privacy, S{\&}P 2010, 16-19
               May 2010, Berleley/Oakland, California, {USA}},
  publisher = {{IEEE} Computer Society},
  year      = {2010},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=5504620},
  isbn      = {978-0-7695-4035-1},
  timestamp = {Thu, 08 Jan 2015 16:59:43 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/sp/2010},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/stm/2010,
  editor    = {Jorge Cu{\'{e}}llar and
               Javier Lopez and
               Gilles Barthe and
               Alexander Pretschner},
  title     = {Security and Trust Management - 6th International Workshop, {STM}
               2010, Athens, Greece, September 23-24, 2010, Revised Selected Papers},
  series    = {Lecture Notes in Computer Science},
  volume    = {6710},
  publisher = {Springer},
  year      = {2011},
  url       = {https://doi.org/10.1007/978-3-642-22444-7},
  doi       = {10.1007/978-3-642-22444-7},
  isbn      = {978-3-642-22443-0},
  timestamp = {Wed, 24 May 2017 08:30:51 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/stm/2010},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/2009,
  editor    = {Renate A. Schmidt},
  title     = {Automated Deduction - CADE-22, 22nd International Conference on Automated
               Deduction, Montreal, Canada, August 2-7, 2009. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5663},
  publisher = {Springer},
  year      = {2009},
  url       = {https://doi.org/10.1007/978-3-642-02959-2},
  doi       = {10.1007/978-3-642-02959-2},
  isbn      = {978-3-642-02958-5},
  timestamp = {Sun, 21 May 2017 00:17:18 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/2009},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lics/2009,
  title     = {Proceedings of the 24th Annual {IEEE} Symposium on Logic in Computer
               Science, {LICS} 2009, 11-14 August 2009, Los Angeles, CA, {USA}},
  publisher = {{IEEE} Computer Society},
  year      = {2009},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=5230546},
  isbn      = {978-0-7695-3746-7},
  timestamp = {Fri, 21 Nov 2014 14:08:56 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/lics/2009},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/pepm/2009,
  editor    = {Germ{\'{a}}n Puebla and
               Germ{\'{a}}n Vidal},
  title     = {Proceedings of the 2009 {ACM} {SIGPLAN} Symposium on Partial Evaluation
               and Semantics-based Program Manipulation, {PEPM} 2009, Savannah, GA,
               USA, January 19-20, 2009},
  publisher = {{ACM}},
  year      = {2009},
  url       = {http://dl.acm.org/citation.cfm?id=1480945},
  isbn      = {978-1-60558-327-3},
  timestamp = {Tue, 22 May 2012 15:24:56 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/pepm/2009},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/tlca/2009,
  editor    = {Pierre{-}Louis Curien},
  title     = {Typed Lambda Calculi and Applications, 9th International Conference,
               {TLCA} 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5608},
  publisher = {Springer},
  year      = {2009},
  url       = {https://doi.org/10.1007/978-3-642-02273-9},
  doi       = {10.1007/978-3-642-02273-9},
  isbn      = {978-3-642-02272-2},
  timestamp = {Wed, 17 May 2017 14:24:41 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tlca/2009},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/csfw/2008,
  title     = {Proceedings of the 21st {IEEE} Computer Security Foundations Symposium,
               {CSF} 2008, Pittsburgh, Pennsylvania, 23-25 June 2008},
  publisher = {{IEEE} Computer Society},
  year      = {2008},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=4556666},
  isbn      = {978-0-7695-3182-3},
  timestamp = {Fri, 13 May 2016 11:48:05 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/csfw/2008},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/icalp/2008-2,
  editor    = {Luca Aceto and
               Ivan Damg{\aa}rd and
               Leslie Ann Goldberg and
               Magn{\'{u}}s M. Halld{\'{o}}rsson and
               Anna Ing{\'{o}}lfsd{\'{o}}ttir and
               Igor Walukiewicz},
  title     = {Automata, Languages and Programming, 35th International Colloquium,
               {ICALP} 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part
               {II} - Track {B:} Logic, Semantics, and Theory of Programming {\&}
               Track {C:} Security and Cryptography Foundations},
  series    = {Lecture Notes in Computer Science},
  volume    = {5126},
  publisher = {Springer},
  year      = {2008},
  url       = {https://doi.org/10.1007/978-3-540-70583-3},
  doi       = {10.1007/978-3-540-70583-3},
  isbn      = {978-3-540-70582-6},
  timestamp = {Tue, 13 Jun 2017 10:37:56 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/icalp/2008-2},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/2008,
  editor    = {Iliano Cervesato and
               Helmut Veith and
               Andrei Voronkov},
  title     = {Logic for Programming, Artificial Intelligence, and Reasoning, 15th
               International Conference, {LPAR} 2008, Doha, Qatar, November 22-27,
               2008. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5330},
  publisher = {Springer},
  year      = {2008},
  url       = {https://doi.org/10.1007/978-3-540-89439-1},
  doi       = {10.1007/978-3-540-89439-1},
  isbn      = {978-3-540-89438-4},
  timestamp = {Tue, 13 Jun 2017 10:37:56 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/2008},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/icfp/2007,
  editor    = {Ralf Hinze and
               Norman Ramsey},
  title     = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
               Functional Programming, {ICFP} 2007, Freiburg, Germany, October 1-3,
               2007},
  publisher = {{ACM}},
  year      = {2007},
  isbn      = {978-1-59593-815-2},
  timestamp = {Tue, 06 Nov 2007 12:48:33 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/icfp/2007},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/icra/2007,
  title     = {2007 {IEEE} International Conference on Robotics and Automation, {ICRA}
               2007, 10-14 April 2007, Roma, Italy},
  publisher = {{IEEE}},
  year      = {2007},
  timestamp = {Wed, 20 Jun 2007 15:07:54 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/icra/2007},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/ndss/2007,
  title     = {Proceedings of the Network and Distributed System Security Symposium,
               {NDSS} 2007, San Diego, California, USA, 28th February - 2nd March
               2007},
  publisher = {The Internet Society},
  year      = {2007},
  timestamp = {Thu, 16 Apr 2009 21:25:40 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ndss/2007},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/rta/2007,
  editor    = {Franz Baader},
  title     = {Term Rewriting and Applications, 18th International Conference, {RTA}
               2007, Paris, France, June 26-28, 2007, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4533},
  publisher = {Springer},
  year      = {2007},
  url       = {https://doi.org/10.1007/978-3-540-73449-9},
  doi       = {10.1007/978-3-540-73449-9},
  isbn      = {978-3-540-73447-5},
  timestamp = {Fri, 02 Jun 2017 13:01:07 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/rta/2007},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/tlca/2007,
  editor    = {Simona Ronchi Della Rocca},
  title     = {Typed Lambda Calculi and Applications, 8th International Conference,
               {TLCA} 2007, Paris, France, June 26-28, 2007, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4583},
  publisher = {Springer},
  year      = {2007},
  url       = {https://doi.org/10.1007/978-3-540-73228-0},
  doi       = {10.1007/978-3-540-73228-0},
  isbn      = {978-3-540-73227-3},
  timestamp = {Fri, 02 Jun 2017 13:01:07 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tlca/2007},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/2006,
  editor    = {Ulrich Furbach and
               Natarajan Shankar},
  title     = {Automated Reasoning, Third International Joint Conference, {IJCAR}
               2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4130},
  publisher = {Springer},
  year      = {2006},
  url       = {https://doi.org/10.1007/11814771},
  doi       = {10.1007/11814771},
  isbn      = {3-540-37187-7},
  timestamp = {Fri, 02 Jun 2017 13:01:06 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/2006},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/csfw/2006,
  title     = {19th {IEEE} Computer Security Foundations Workshop, {(CSFW-19} 2006),
               5-7 July 2006, Venice, Italy},
  publisher = {{IEEE} Computer Society},
  year      = {2006},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=10965},
  isbn      = {0-7695-2615-2},
  timestamp = {Fri, 13 May 2016 11:50:11 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/csfw/2006},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/esorics/2006,
  editor    = {Dieter Gollmann and
               Jan Meier and
               Andrei Sabelfeld},
  title     = {Computer Security - {ESORICS} 2006, 11th European Symposium on Research
               in Computer Security, Hamburg, Germany, September 18-20, 2006, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4189},
  publisher = {Springer},
  year      = {2006},
  url       = {https://doi.org/10.1007/11863908},
  doi       = {10.1007/11863908},
  isbn      = {3-540-44601-X},
  timestamp = {Fri, 02 Jun 2017 13:01:07 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/esorics/2006},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/2005,
  editor    = {Robert Nieuwenhuis},
  title     = {Automated Deduction - CADE-20, 20th International Conference on Automated
               Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {3632},
  publisher = {Springer},
  year      = {2005},
  url       = {https://doi.org/10.1007/11532231},
  doi       = {10.1007/11532231},
  isbn      = {3-540-28005-7},
  timestamp = {Tue, 30 May 2017 16:36:52 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/2005},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/concur/2005,
  editor    = {Mart{\'{\i}}n Abadi and
               Luca de Alfaro},
  title     = {{CONCUR} 2005 - Concurrency Theory, 16th International Conference,
               {CONCUR} 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {3653},
  publisher = {Springer},
  year      = {2005},
  url       = {https://doi.org/10.1007/11539452},
  doi       = {10.1007/11539452},
  isbn      = {3-540-28309-9},
  timestamp = {Tue, 30 May 2017 16:36:53 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/concur/2005},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/csl/2005,
  editor    = {C.{-}H. Luke Ong},
  title     = {Computer Science Logic, 19th International Workshop, {CSL} 2005, 14th
               Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {3634},
  publisher = {Springer},
  year      = {2005},
  url       = {https://doi.org/10.1007/11538363},
  doi       = {10.1007/11538363},
  isbn      = {3-540-28231-9},
  timestamp = {Tue, 30 May 2017 16:36:53 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/csl/2005},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/icfp/2005merlin,
  editor    = {Randy Pollack},
  title     = {{ACM} {SIGPLAN} International Conference on Functional Programming,
               Workshop on Mechanized reasoning about languages with variable binding,
               {MERLIN} 2005, Tallinn, Estonia, September 30, 2005},
  publisher = {{ACM}},
  year      = {2005},
  timestamp = {Wed, 23 Apr 2008 15:32:32 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/icfp/2005merlin},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/popl/2005,
  editor    = {Jens Palsberg and
               Mart{\'{\i}}n Abadi},
  title     = {Proceedings of the 32nd {ACM} {SIGPLAN-SIGACT} Symposium on Principles
               of Programming Languages, {POPL} 2005, Long Beach, California, USA,
               January 12-14, 2005},
  publisher = {{ACM}},
  year      = {2005},
  url       = {http://dl.acm.org/citation.cfm?id=1040305},
  isbn      = {1-58113-830-X},
  timestamp = {Tue, 22 May 2012 15:24:56 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/popl/2005},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/ppdp/2005,
  editor    = {Pedro Barahona and
               Amy P. Felty},
  title     = {Proceedings of the 7th International {ACM} {SIGPLAN} Conference on
               Principles and Practice of Declarative Programming, July 11-13 2005,
               Lisbon, Portugal},
  publisher = {{ACM}},
  year      = {2005},
  isbn      = {1-59593-090-6},
  timestamp = {Thu, 21 Jul 2005 07:39:25 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ppdp/2005},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/aplas/2004,
  editor    = {Wei{-}Ngan Chin},
  title     = {Programming Languages and Systems: Second Asian Symposium, {APLAS}
               2004, Taipei, Taiwan, November 4-6, 2004. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {3302},
  publisher = {Springer},
  year      = {2004},
  url       = {https://doi.org/10.1007/b102225},
  doi       = {10.1007/b102225},
  isbn      = {3-540-23724-0},
  timestamp = {Tue, 30 May 2017 16:36:52 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/aplas/2004},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lics/2004,
  title     = {19th {IEEE} Symposium on Logic in Computer Science {(LICS} 2004),
               14-17 July 2004, Turku, Finland, Proceedings},
  publisher = {{IEEE} Computer Society},
  year      = {2004},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=9221},
  isbn      = {0-7695-2192-4},
  timestamp = {Fri, 21 Nov 2014 14:08:55 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/lics/2004},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/popl/2004,
  editor    = {Neil D. Jones and
               Xavier Leroy},
  title     = {Proceedings of the 31st {ACM} {SIGPLAN-SIGACT} Symposium on Principles
               of Programming Languages, {POPL} 2004, Venice, Italy, January 14-16,
               2004},
  publisher = {{ACM}},
  year      = {2004},
  url       = {http://dl.acm.org/citation.cfm?id=964001},
  isbn      = {1-58113-729-X},
  timestamp = {Tue, 22 May 2012 15:24:56 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/popl/2004},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/tphol/2004,
  editor    = {Konrad Slind and
               Annette Bunker and
               Ganesh Gopalakrishnan},
  title     = {Theorem Proving in Higher Order Logics, 17th International Conference,
               TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {3223},
  publisher = {Springer},
  year      = {2004},
  url       = {https://doi.org/10.1007/b100400},
  doi       = {10.1007/b100400},
  isbn      = {3-540-23017-3},
  timestamp = {Tue, 30 May 2017 12:57:44 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tphol/2004},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/2003,
  editor    = {Franz Baader},
  title     = {Automated Deduction - CADE-19, 19th International Conference on Automated
               Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2741},
  publisher = {Springer},
  year      = {2003},
  url       = {https://doi.org/10.1007/b11829},
  doi       = {10.1007/b11829},
  isbn      = {3-540-40559-3},
  timestamp = {Mon, 29 May 2017 16:53:43 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/2003},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/fossacs/2003,
  editor    = {Andrew D. Gordon},
  title     = {Foundations of Software Science and Computational Structures, 6th
               International Conference, {FOSSACS} 2003 Held as Part of the Joint
               European Conference on Theory and Practice of Software, {ETAPS} 2003,
               Warsaw, Poland, April 7-11, 2003, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2620},
  publisher = {Springer},
  year      = {2003},
  url       = {https://doi.org/10.1007/3-540-36576-1},
  doi       = {10.1007/3-540-36576-1},
  isbn      = {3-540-00897-7},
  timestamp = {Mon, 29 May 2017 16:53:44 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/fossacs/2003},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/icfp/2003merlin,
  title     = {Eighth {ACM} {SIGPLAN} International Conference on Functional Programming,
               Workshop on Mechanized reasoning about languages with variable binding,
               {MERLIN} 2003, Uppsala, Sweden, August 2003},
  publisher = {{ACM}},
  year      = {2003},
  timestamp = {Wed, 21 Apr 2004 14:02:37 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/icfp/2003merlin},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/ijcai/2003,
  editor    = {Georg Gottlob and
               Toby Walsh},
  title     = {IJCAI-03, Proceedings of the Eighteenth International Joint Conference
               on Artificial Intelligence, Acapulco, Mexico, August 9-15, 2003},
  publisher = {Morgan Kaufmann},
  year      = {2003},
  url       = {http://ijcai.org/proceedings/2003},
  timestamp = {Tue, 19 Jul 2016 16:02:31 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ijcai/2003},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/popl/2003,
  editor    = {Alex Aiken and
               Greg Morrisett},
  title     = {Conference Record of {POPL} 2003: The 30th {SIGPLAN-SIGACT} Symposium
               on Principles of Programming Languages, New Orleans, Louisisana, USA,
               January 15-17, 2003},
  publisher = {{ACM}},
  year      = {2003},
  url       = {http://dl.acm.org/citation.cfm?id=604131},
  isbn      = {1-58113-628-5},
  timestamp = {Mon, 18 Mar 2013 08:37:45 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/popl/2003},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/tphol/2003,
  editor    = {David A. Basin and
               Burkhart Wolff},
  title     = {Theorem Proving in Higher Order Logics, 16th International Conference,
               TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2758},
  publisher = {Springer},
  year      = {2003},
  url       = {https://doi.org/10.1007/b11935},
  doi       = {10.1007/b11935},
  isbn      = {3-540-40664-6},
  timestamp = {Mon, 29 May 2017 16:53:44 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tphol/2003},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/types/2003,
  editor    = {Stefano Berardi and
               Mario Coppo and
               Ferruccio Damiani},
  title     = {Types for Proofs and Programs, International Workshop, {TYPES} 2003,
               Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers},
  series    = {Lecture Notes in Computer Science},
  volume    = {3085},
  publisher = {Springer},
  year      = {2004},
  url       = {https://doi.org/10.1007/b98246},
  doi       = {10.1007/b98246},
  isbn      = {3-540-22164-6},
  timestamp = {Thu, 15 Jun 2017 21:39:32 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/types/2003},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/grid/2002,
  editor    = {Manish Parashar},
  title     = {Grid Computing - {GRID} 2002, Third International Workshop, Baltimore,
               MD, USA, November 18, 2002, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2536},
  publisher = {Springer},
  year      = {2002},
  url       = {https://doi.org/10.1007/3-540-36133-2},
  doi       = {10.1007/3-540-36133-2},
  isbn      = {3-540-00133-6},
  timestamp = {Fri, 26 May 2017 00:50:43 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/grid/2002},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lics/2001,
  title     = {16th Annual {IEEE} Symposium on Logic in Computer Science, Boston,
               Massachusetts, USA, June 16-19, 2001, Proceedings},
  publisher = {{IEEE} Computer Society},
  year      = {2001},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=7424},
  isbn      = {0-7695-1281-X},
  timestamp = {Fri, 21 Nov 2014 14:08:56 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/lics/2001},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@book{DBLP:books/el/RobinsonV01,
  editor    = {John Alan Robinson and
               Andrei Voronkov},
  title     = {Handbook of Automated Reasoning (in 2 volumes)},
  publisher = {Elsevier and {MIT} Press},
  year      = {2001},
  isbn      = {0-444-50813-9},
  timestamp = {Wed, 29 Mar 2017 16:45:21 +0200},
  biburl    = {http://dblp.org/rec/bib/books/el/RobinsonV01},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/icfp/2000,
  editor    = {Martin Odersky and
               Philip Wadler},
  title     = {Proceedings of the Fifth {ACM} {SIGPLAN} International Conference
               on Functional Programming {(ICFP} '00), Montreal, Canada, September
               18-21, 2000},
  publisher = {{ACM}},
  year      = {2000},
  isbn      = {1-58113-202-6},
  timestamp = {Tue, 11 Jun 2013 13:51:25 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/icfp/2000},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/pepm/2000,
  editor    = {Julia L. Lawall},
  title     = {Proceedings of the 2000 {ACM} {SIGPLAN} Workshop on Partial Evaluation
               and Semantics-Based Program Manipulation {(PEPM} '00), Boston, Massachusetts,
               USA, January 22-23, 2000},
  publisher = {{ACM}},
  year      = {2000},
  url       = {http://dl.acm.org/citation.cfm?id=328690},
  isbn      = {1-58113-201-8},
  timestamp = {Tue, 22 May 2012 15:24:56 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/pepm/2000},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/saig/2000,
  editor    = {Walid Taha},
  title     = {Semantics, Applications, and Implementation of Program Generation,
               International Workshop {SAIG} 2000, Montreal, Canada, September 20,
               2000, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1924},
  publisher = {Springer},
  year      = {2000},
  url       = {https://doi.org/10.1007/3-540-45350-4},
  doi       = {10.1007/3-540-45350-4},
  isbn      = {3-540-41054-6},
  timestamp = {Wed, 24 May 2017 15:40:45 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/saig/2000},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/agp/1999,
  editor    = {Maria Chiara Meo and
               Manuel Vilares Ferro},
  title     = {1999 Joint Conference on Declarative Programming, AGP'99, L'Aquila,
               Italy, September 6-9, 1999},
  year      = {1999},
  timestamp = {Wed, 01 Dec 2004 15:33:47 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/agp/1999},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/1999,
  editor    = {Harald Ganzinger},
  title     = {Automated Deduction - CADE-16, 16th International Conference on Automated
               Deduction, Trento, Italy, July 7-10, 1999, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1632},
  publisher = {Springer},
  year      = {1999},
  url       = {https://doi.org/10.1007/3-540-48660-7},
  doi       = {10.1007/3-540-48660-7},
  isbn      = {3-540-66222-7},
  timestamp = {Wed, 24 May 2017 15:40:41 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/1999},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/iclp/1999,
  editor    = {Danny De Schreye},
  title     = {Logic Programming: The 1999 International Conference, Las Cruces,
               New Mexico, USA, November 29 - December 4, 1999},
  publisher = {{MIT} Press},
  year      = {1999},
  isbn      = {0-262-54104-1},
  timestamp = {Mon, 02 Dec 2013 17:40:45 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/iclp/1999},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/popl/1999,
  editor    = {Andrew W. Appel and
               Alex Aiken},
  title     = {{POPL} '99, Proceedings of the 26th {ACM} {SIGPLAN-SIGACT} Symposium
               on Principles of Programming Languages, San Antonio, TX, USA, January
               20-22, 1999},
  publisher = {{ACM}},
  year      = {1999},
  url       = {http://dl.acm.org/citation.cfm?id=292540},
  isbn      = {1-58113-095-3},
  timestamp = {Mon, 21 May 2012 16:19:51 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/popl/1999},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/ppdp/1999,
  editor    = {Gopalan Nadathur},
  title     = {Principles and Practice of Declarative Programming, International
               Conference PPDP'99, Paris, France, September 29 - October 1, 1999,
               Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1702},
  publisher = {Springer},
  year      = {1999},
  url       = {https://doi.org/10.1007/10704567},
  doi       = {10.1007/10704567},
  isbn      = {3-540-66540-4},
  timestamp = {Wed, 24 May 2017 15:40:43 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ppdp/1999},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/tlca/1999,
  editor    = {Jean{-}Yves Girard},
  title     = {Typed Lambda Calculi and Applications, 4th International Conference,
               TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1581},
  publisher = {Springer},
  year      = {1999},
  url       = {https://doi.org/10.1007/3-540-48959-2},
  doi       = {10.1007/3-540-48959-2},
  isbn      = {3-540-65763-0},
  timestamp = {Tue, 23 May 2017 14:54:58 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tlca/1999},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/1998,
  editor    = {Claude Kirchner and
               H{\'{e}}l{\`{e}}ne Kirchner},
  title     = {Automated Deduction - CADE-15, 15th International Conference on Automated
               Deduction, Lindau, Germany, July 5-10, 1998, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1421},
  publisher = {Springer},
  year      = {1998},
  url       = {https://doi.org/10.1007/BFb0054239},
  doi       = {10.1007/BFb0054239},
  isbn      = {3-540-64675-2},
  timestamp = {Tue, 23 May 2017 11:53:57 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/1998},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/pldi/1998,
  editor    = {Jack W. Davidson and
               Keith D. Cooper and
               A. Michael Berman},
  title     = {Proceedings of the {ACM} {SIGPLAN} '98 Conference on Programming Language
               Design and Implementation (PLDI), Montreal, Canada, June 17-19, 1998},
  publisher = {{ACM}},
  year      = {1998},
  url       = {http://dl.acm.org/citation.cfm?id=277650},
  isbn      = {0-89791-987-4},
  timestamp = {Mon, 21 May 2012 16:19:53 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/pldi/1998},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/types/1998,
  editor    = {Thorsten Altenkirch and
               Wolfgang Naraschewski and
               Bernhard Reus},
  title     = {Types for Proofs and Programs, International Workshop {TYPES} '98,
               Kloster Irsee, Germany, March 27-31, 1998, Selected Papers},
  series    = {Lecture Notes in Computer Science},
  volume    = {1657},
  publisher = {Springer},
  year      = {1999},
  url       = {https://doi.org/10.1007/3-540-48167-2},
  doi       = {10.1007/3-540-48167-2},
  isbn      = {3-540-66537-4},
  timestamp = {Wed, 24 May 2017 15:40:43 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/types/1998},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lics/1997,
  title     = {Proceedings, 12th Annual {IEEE} Symposium on Logic in Computer Science,
               Warsaw, Poland, June 29 - July 2, 1997},
  publisher = {{IEEE} Computer Society},
  year      = {1997},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=4856},
  isbn      = {0-8186-7925-5},
  timestamp = {Fri, 21 Nov 2014 14:08:56 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/lics/1997},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/tlca/1997,
  editor    = {Philippe de Groote},
  title     = {Typed Lambda Calculi and Applications, Third International Conference
               on Typed Lambda Calculi and Applications, {TLCA} '97, Nancy, France,
               April 2-4, 1997, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1210},
  publisher = {Springer},
  year      = {1997},
  url       = {https://doi.org/10.1007/3-540-62688-3},
  doi       = {10.1007/3-540-62688-3},
  isbn      = {3-540-62688-3},
  timestamp = {Mon, 22 May 2017 17:11:16 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tlca/1997},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/caap/1996,
  editor    = {H{\'{e}}l{\`{e}}ne Kirchner},
  title     = {Trees in Algebra and Programming - CAAP'96, 21st International Colloquium,
               Link{\"{o}}ping, Sweden, April, 22-24, 1996, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1059},
  publisher = {Springer},
  year      = {1996},
  url       = {https://doi.org/10.1007/3-540-61064-2},
  doi       = {10.1007/3-540-61064-2},
  isbn      = {3-540-61064-2},
  timestamp = {Mon, 22 May 2017 16:14:06 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/caap/1996},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/elp/1996,
  editor    = {Roy Dyckhoff and
               Heinrich Herre and
               Peter Schroeder{-}Heister},
  title     = {Extensions of Logic Programming, 5th International Workshop, ELP'96,
               Leipzig, Germany, March 28-30, 1996, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1050},
  publisher = {Springer},
  year      = {1996},
  url       = {https://doi.org/10.1007/3-540-60983-0},
  doi       = {10.1007/3-540-60983-0},
  isbn      = {3-540-60983-0},
  timestamp = {Mon, 22 May 2017 16:14:04 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/elp/1996},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/esop/1996,
  editor    = {Hanne Riis Nielson},
  title     = {Programming Languages and Systems - ESOP'96, 6th European Symposium
               on Programming, Link{\"{o}}ping, Sweden, April 22-24, 1996, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1058},
  publisher = {Springer},
  year      = {1996},
  url       = {https://doi.org/10.1007/3-540-61055-3},
  doi       = {10.1007/3-540-61055-3},
  isbn      = {3-540-61055-3},
  timestamp = {Mon, 22 May 2017 16:14:04 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/esop/1996},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/iclp/1996,
  editor    = {Michael J. Maher},
  title     = {Logic Programming, Proceedings of the 1996 Joint International Conference
               and Symposium on Logic Programming, Bonn, Germany, September 2-6,
               1996},
  publisher = {{MIT} Press},
  year      = {1996},
  url       = {http://ieeexplore.ieee.org/xpl/bkabstractplus.jsp?bkn=6267515},
  isbn      = {0-262-63173-3},
  timestamp = {Thu, 17 Aug 2017 12:43:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/iclp/1996},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lics/1996,
  title     = {Proceedings, 11th Annual {IEEE} Symposium on Logic in Computer Science,
               New Brunswick, New Jersey, USA, July 27-30, 1996},
  publisher = {{IEEE} Computer Society},
  year      = {1996},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=4265},
  isbn      = {0-8186-7463-6},
  timestamp = {Fri, 21 Nov 2014 14:08:55 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/lics/1996},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/popl/1996,
  editor    = {Hans{-}Juergen Boehm and
               Guy L. Steele Jr.},
  title     = {Conference Record of POPL'96: The 23rd {ACM} {SIGPLAN-SIGACT} Symposium
               on Principles of Programming Languages, Papers Presented at the Symposium,
               St. Petersburg Beach, Florida, USA, January 21-24, 1996},
  publisher = {{ACM} Press},
  year      = {1996},
  url       = {http://dl.acm.org/citation.cfm?id=237721},
  isbn      = {0-89791-769-3},
  timestamp = {Mon, 21 May 2012 16:19:50 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/popl/1996},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lics/1995,
  title     = {Proceedings, 10th Annual {IEEE} Symposium on Logic in Computer Science,
               San Diego, California, USA, June 26-29, 1995},
  publisher = {{IEEE} Computer Society},
  year      = {1995},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=3961},
  isbn      = {0-8186-7050-9},
  timestamp = {Fri, 21 Nov 2014 14:08:56 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/lics/1995},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/1994,
  editor    = {Alan Bundy},
  title     = {Automated Deduction - CADE-12, 12th International Conference on Automated
               Deduction, Nancy, France, June 26 - July 1, 1994, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {814},
  publisher = {Springer},
  year      = {1994},
  url       = {https://doi.org/10.1007/3-540-58156-1},
  doi       = {10.1007/3-540-58156-1},
  isbn      = {3-540-58156-1},
  timestamp = {Sat, 20 May 2017 15:32:47 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/1994},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lics/1993,
  title     = {Proceedings of the Eighth Annual Symposium on Logic in Computer Science
               {(LICS} '93), Montreal, Canada, June 19-23, 1993},
  publisher = {{IEEE} Computer Society},
  year      = {1993},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=899},
  isbn      = {0-8186-3140-6},
  timestamp = {Fri, 21 Nov 2014 14:08:56 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/lics/1993},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/slp/1993,
  editor    = {Dale Miller},
  title     = {Logic Programming, Proceedings of the 1993 International Symposium,
               Vancouver, British Columbia, Canada, October 26-29, 1993},
  publisher = {{MIT} Press},
  year      = {1993},
  isbn      = {0-262-63152-0},
  timestamp = {Sun, 12 Nov 2017 16:01:30 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/slp/1993},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/tphol/1993,
  editor    = {Jeffrey J. Joyce and
               Carl{-}Johan H. Seger},
  title     = {Higher Order Logic Theorem Proving and its Applications, 6th International
               Workshop, {HUG} '93, Vancouver, BC, Canada, August 11-13, 1993, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {780},
  publisher = {Springer},
  year      = {1994},
  url       = {https://doi.org/10.1007/3-540-57826-9},
  doi       = {10.1007/3-540-57826-9},
  isbn      = {3-540-57826-9},
  timestamp = {Sat, 20 May 2017 15:32:54 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tphol/1993},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/1992,
  editor    = {Deepak Kapur},
  title     = {Automated Deduction - CADE-11, 11th International Conference on Automated
               Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {607},
  publisher = {Springer},
  year      = {1992},
  url       = {https://doi.org/10.1007/3-540-55602-8},
  doi       = {10.1007/3-540-55602-8},
  isbn      = {3-540-55602-8},
  timestamp = {Sat, 20 May 2017 15:32:46 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/1992},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lics/1992,
  title     = {Proceedings of the Seventh Annual Symposium on Logic in Computer Science
               {(LICS} '92), Santa Cruz, California, USA, June 22-25, 1992},
  publisher = {{IEEE} Computer Society},
  year      = {1992},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=402},
  isbn      = {0-8186-2735-2},
  timestamp = {Fri, 21 Nov 2014 14:08:56 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/lics/1992},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/elp/1991,
  editor    = {Lars{-}Henrik Eriksson and
               Lars Halln{\"{a}}s and
               Peter Schroeder{-}Heister},
  title     = {Extensions of Logic Programming, Second International Workshop, ELP'91,
               Stockholm, Sweden, January 27-29, 1991, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {596},
  publisher = {Springer},
  year      = {1992},
  url       = {https://doi.org/10.1007/BFb0013601},
  doi       = {10.1007/BFb0013601},
  isbn      = {3-540-55498-X},
  timestamp = {Sat, 20 May 2017 15:32:49 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/elp/1991},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lics/1991,
  title     = {Proceedings of the Sixth Annual Symposium on Logic in Computer Science
               {(LICS} '91), Amsterdam, The Netherlands, July 15-18, 1991},
  publisher = {{IEEE} Computer Society},
  year      = {1991},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=360},
  isbn      = {0-8186-2230-X},
  timestamp = {Fri, 21 Nov 2014 14:08:56 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/lics/1991},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/pepm/1991,
  editor    = {Charles Consel and
               Olivier Danvy},
  title     = {Proceedings of the Symposium on Partial Evaluation and Semantics-Based
               Program Manipulation, PEPM'91, Yale University, New Haven, Connecticut,
               USA, June 17-19, 1991},
  publisher = {{ACM}},
  year      = {1991},
  url       = {http://dl.acm.org/citation.cfm?id=115865},
  isbn      = {0-89791-433-3},
  timestamp = {Tue, 22 May 2012 15:24:56 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/pepm/1991},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/pldi/1991,
  editor    = {David S. Wise},
  title     = {Proceedings of the {ACM} SIGPLAN'91 Conference on Programming Language
               Design and Implementation (PLDI), Toronto, Ontario, Canada, June 26-28,
               1991},
  publisher = {{ACM}},
  year      = {1991},
  url       = {http://dl.acm.org/citation.cfm?id=113445},
  isbn      = {0-89791-428-7},
  timestamp = {Mon, 21 May 2012 16:19:52 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/pldi/1991},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/slp/1991,
  editor    = {Vijay A. Saraswat and
               Kazunori Ueda},
  title     = {Logic Programming, Proceedings of the 1991 International Symposium,
               San Diego, California, USA, Oct. 28 - Nov 1, 1991},
  publisher = {{MIT} Press},
  year      = {1991},
  isbn      = {0-262-69147-7},
  timestamp = {Wed, 04 Dec 2013 14:42:58 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/slp/1991},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/1990,
  editor    = {Mark E. Stickel},
  title     = {10th International Conference on Automated Deduction, Kaiserslautern,
               FRG, July 24-27, 1990, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {449},
  publisher = {Springer},
  year      = {1990},
  url       = {https://doi.org/10.1007/3-540-52885-7},
  doi       = {10.1007/3-540-52885-7},
  isbn      = {3-540-52885-7},
  timestamp = {Fri, 19 May 2017 13:10:45 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/1990},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/iclp/1990,
  editor    = {David H. D. Warren and
               P{\'{e}}ter Szeredi},
  title     = {Logic Programming, Proceedings of the Seventh International Conference,
               Jerusalem, Israel, June 18-20, 1990},
  publisher = {{MIT} Press},
  year      = {1990},
  isbn      = {0-262-73090-1},
  timestamp = {Fri, 29 Nov 2013 14:57:24 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/iclp/1990},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/icml/1989,
  editor    = {Alberto Maria Segre},
  title     = {Proceedings of the Sixth International Workshop on Machine Learning
               {(ML} 1989), Cornell University, Ithaca, New York, USA, June 26-27,
               1989},
  publisher = {Morgan Kaufmann},
  year      = {1989},
  isbn      = {1-55860-036-1},
  timestamp = {Thu, 05 Dec 2002 12:38:01 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/icml/1989},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lics/1989,
  title     = {Proceedings of the Fourth Annual Symposium on Logic in Computer Science
               {(LICS} '89), Pacific Grove, California, USA, June 5-8, 1989},
  publisher = {{IEEE} Computer Society},
  year      = {1989},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=249},
  isbn      = {0-8186-1954-6},
  timestamp = {Fri, 21 Nov 2014 14:08:56 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/lics/1989},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/mfps/1989,
  editor    = {Michael G. Main and
               Austin Melton and
               Michael W. Mislove and
               David A. Schmidt},
  title     = {Mathematical Foundations of Programming Semantics, 5th International
               Conference, Tulane University, New Orleans, Louisiana, USA, March
               29 - April 1, 1989, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {442},
  publisher = {Springer},
  year      = {1990},
  url       = {https://doi.org/10.1007/BFb0040251},
  doi       = {10.1007/BFb0040251},
  isbn      = {3-540-97375-3},
  timestamp = {Fri, 19 May 2017 13:10:47 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/mfps/1989},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/tapsoft/1989-2,
  editor    = {Josep D{\'{\i}}az and
               Fernando Orejas},
  title     = {TAPSOFT'89: Proceedings of the International Joint Conference on Theory
               and Practice of Software Development, Barcelona, Spain, March 13-17,
               1989, Volume 2: Advanced Seminar on Foundations of Innovative Software
               Development {II} and Colloquium on Current Issues in Programming Languages
               {(CCIPL)}},
  series    = {Lecture Notes in Computer Science},
  volume    = {352},
  publisher = {Springer},
  year      = {1989},
  url       = {https://doi.org/10.1007/3-540-50940-2},
  doi       = {10.1007/3-540-50940-2},
  isbn      = {3-540-50940-2},
  timestamp = {Fri, 19 May 2017 13:10:47 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tapsoft/1989-2},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/1988,
  editor    = {Ewing L. Lusk and
               Ross A. Overbeek},
  title     = {9th International Conference on Automated Deduction, Argonne, Illinois,
               USA, May 23-26, 1988, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {310},
  publisher = {Springer},
  year      = {1988},
  url       = {https://doi.org/10.1007/BFb0012819},
  doi       = {10.1007/BFb0012819},
  isbn      = {3-540-19343-X},
  timestamp = {Fri, 19 May 2017 13:10:45 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/1988},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/pldi/1988,
  editor    = {Richard L. Wexelblat},
  title     = {Proceedings of the {ACM} SIGPLAN'88 Conference on Programming Language
               Design and Implementation (PLDI), Atlanta, Georgia, USA, June 22-24,
               1988},
  publisher = {{ACM}},
  year      = {1988},
  url       = {http://dl.acm.org/citation.cfm?id=53990},
  isbn      = {0-89791-269-1},
  timestamp = {Mon, 21 May 2012 16:19:53 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/pldi/1988},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/sde/1988,
  editor    = {Peter B. Henderson},
  title     = {Proceedings of the {ACM} {SIGSOFT/SIGPLAN} Software Engineering Symposium
               on Practical Software Development Environments, Boston, Massachusetts,
               USA, November 28-30, 1988},
  publisher = {{ACM}},
  year      = {1989},
  url       = {http://dl.acm.org/citation.cfm?id=64135},
  isbn      = {0-89791-290-X},
  timestamp = {Tue, 22 May 2012 15:24:55 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/sde/1988},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/1986,
  editor    = {J{\"{o}}rg H. Siekmann},
  title     = {8th International Conference on Automated Deduction, Oxford, England,
               July 27 - August 1, 1986, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {230},
  publisher = {Springer},
  year      = {1986},
  url       = {https://doi.org/10.1007/3-540-16780-3},
  doi       = {10.1007/3-540-16780-3},
  isbn      = {3-540-16780-3},
  timestamp = {Fri, 19 May 2017 12:26:18 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/1986},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/1984,
  editor    = {Robert E. Shostak},
  title     = {7th International Conference on Automated Deduction, Napa, California,
               USA, May 14-16, 1984, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {170},
  publisher = {Springer},
  year      = {1984},
  url       = {https://doi.org/10.1007/978-0-387-34768-4},
  doi       = {10.1007/978-0-387-34768-4},
  isbn      = {3-540-96022-8},
  timestamp = {Fri, 19 May 2017 00:43:55 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/1984},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
maintained by Schloss Dagstuhl LZI at University of Trier