BOOK {sheaves.geometry.logic,
author="Saunders MacLane and Ieke Moerdijk",
title="Sheaves in Geometry and Logic",
publisher="Springer-Verlag",
year="1992"}

@BOOK {category.theory.computing.science,
author="Michael Barr and Charles Wells",
title="Category Theory for Computing Science",
publisher="Centre de Recherches Math\'ematiques",
year="1999"}

@InProceedings{proof.irrelevance,
  author =       "Frank Pfenning",
  title =        "Intensionality, Extensionality, and Proof Irrelevance in
                  Modal Type Theory",
  editor =       "J. Halpern",
  booktitle =    "Proceedings of the 16th Annual Symposium on Logic in
                  Computer Science (LICS'01)",
  pages =        "221--230",
  year =         2001,
  publisher =    "IEEE Computer Society Press",
  address =      "Boston, Massachusetts",
  month =        jun,
  keywords =     "LF, Elf",
  urlpdf =       "http://www.cs.cmu.edu/~fp/papers/lics01.pdf",
  urlps =        "http://www.cs.cmu.edu/~fp/papers/lics01.ps"
}

@UNPUBLISHED {andrzej.cccs,
author="Andrzej Filinksi",
title="{CCC}s and Typed $\lambda$-calculi",
year="1992",
note="Unpublished manuscript"}

@UNPUBLISHED {jcreed.cd01,
author="Jason Reed",
title="Formalizing the Construction of Exponentials in an Elementary Topos",
year="2001",
note="Unpublished manuscript"}

@INBOOK {kelley.duality,
author="G. M. Kelley",
title="Basic Concepts of Enriched Category Theory",
year="1982",
pages="30-31",
publisher="Cambridge University Press"}

@ARTICLE {module,
author="Robert Harper and Frank Pfenning",
title="A Module System for a Programming Language
Based on the {LF} Logical Framework",
year="1998",
journal="J. Logic Computat.",
volume="8",
number="1",
pages="5-31"}

@BOOK {lambek.scott,
author="J. Lambek and P. J. Scott",
title="Higher Order Categorical Logic",
year="1986",
publisher="Cambridge University Press"}

@BOOK {jacobs,
author="B. Jacobs",
title="Categorical Logic and Type Theory",
year="1999",
publisher="Elsevier"}

@TECHREPORT {andrej.bracket,
author="Steve Awodey and Andrej Bauer",
title="Propositions as {[Types]}",
year="2001",
institution="Institut Mittag-Leffler"
}

@TECHREPORT {canonical.forms,
author="Robert Harper and Frank Pfenning",
title="On the Equivalence and Canonical Forms in the {LF} Type Theory",
year="2001",
institution="Carnegie Mellon University"
}

@article{canonical.forms05,
  title={{On Equivalence and Canonical Forms in the LF Type Theory}},
  author={Harper, R. and Pfenning, F.},
  journal={ACM Transactions on Computational Logic},
  volume={6},
  number={1},
  pages={61-101},
  year={2005}
}

@InProceedings{pfenning.strictness,
  author =       "Frank Pfenning and Carsten Sch{\"u}rmann",
  title =        "Algorithms for Equality and Unification in the
                  Presence of Notational Definitions",
  editor =       "T. Altenkirch and W. Naraschewski and B. Reus",
  booktitle =    "Types for Proofs and Programs",
  month =        mar,
  year =         1998,
  pages =        "179--193",
  address =      "Kloster Irsee, Germany",
  publisher =    "Springer-Verlag LNCS 1657",
  keywords =     "LF, Elf",
  urlps =        "http://www.cs.cmu.edu/~fp/papers/types98.ps.gz"
}

@InProceedings{mode.check,
  author =       "Ekkehard Rohwedder and Frank Pfenning",
  title =        "Mode and Termination Checking for Higher-Order Logic
                  Programs",
  editor =       "Hanne Riis Nielson",
  booktitle =    "Proceedings of the European Symposium on Programming",
  year =         1996,
  publisher =    "Springer-Verlag LNCS 1058",
  address =      "Link{\"o}ping, Sweden",
  month =        apr,
  pages =        "296--310",
  keywords =     "LF, Elf",
  urlps =        "http://www.cs.cmu.edu/~fp/papers/esop96.ps.gz"
}

@InProceedings{termination.check,
author="Brigitte Pientka and Frank Pfenning",
title="Termination and Reduction Checking in the Logical Framework",
booktitle="Workshop on Automation of Proofs by Mathematical Induction",
year=2000,
}

@TechReport{linear.spine.calculus,
  author = 	 "Iliano Cervesato and Frank Pfenning",
  title = 	 "A Linear Spine Calculus",
  institution =  "Department of Computer Science, Carnegie Mellon University",
  year = 	 1997,
  number =	 "CMU-CS-97-125",
  month =	 apr,
  keywords =	 "LF, Elf, linear",
  urlps =	 "http://www.cs.cmu.edu/~fp/papers/CMU-CS-97-125.ps.gz"
}

@Book{Constable86,
  author =	"Robert L. Constable and others",
  title	=	"Implementing Mathematics with the Nuprl Proof Development
		  System",
  publisher =	"Prentice-Hall",
  address =	"Englewood Cliffs, New Jersey",
  year =	"1986",
  keywords = 	"misc"
}

@Article{Harper93jacm,
  author =	"Robert Harper and Furio Honsell and Gordon Plotkin",
  title =	"A Framework for Defining Logics",
  journal =	"Journal of the Association for Computing Machinery",
  volume =	"40",
  number =	"1",
  month =	jan,
  year =	"1993",
  pages =	"143--184",
  urldvi =	"http://www.cs.cmu.edu/~fp/elf-papers/jacm93.dvi.gz",
  keywords = 	"LF"
}

@InProceedings{hoas,
  author = 	 "Frank Pfenning and Conal Elliott.",
  title = 	 "Higher-order abstract syntax",
  pages =        "199--208",
  booktitle =	 "Proceedings of the ACM SIGPLAN '88 Symposium on Language Design and
Implementation",
  year =	 1989,
  address =	 "Atlanta, Georgia",
  month =	 jun,
}

@UNPUBLISHED {appel.twelf,
author="Andrew Appel",
title="Hints on Proving Theorems in {Twelf}",
year="2000",
note="Web page. {\hfil\break}URL: {\tt http://www.cs.princeton.edu/$\sim$appel/twelf-tutorial/}",
institution = "Princeton University"
}

@InProceedings {barthe.relevance,
author = "G. Barthe",
title = "The relevance of proof-irrelevance.",
editor = "K. Larsen, S. Skyum and G. Winskel",
booktitle = "Proceedings of ICALP'98, LNCS",
year = 1998
}

@InProceedings{dowek.expsubs,
  author = 	 "Gilles Dowek and Th{\'e}r{\`e}se Hardin and Claude
		  Kirchner",
  title = 	 "Higher-Order Unification via Explicit Substitutions",
  editor =	 "D. Kozen",
  booktitle =	 "Proceedings of the Tenth Annual Symposium on Logic in
		  Computer Science",
  year =	 1995,
  publisher =	 "IEEE Computer Society Press",
  address =	 "San Diego, California",
  month =	 "June",
  pages =	 "366--374",
  keywords =     "unification"
}

@InProceedings{dowek.patterns,
  author = 	 "Gilles Dowek and Th{\'e}r{\`e}se Hardin and Claude Kirchner
                  and Frank Pfenning",
  title = 	 "Unification via Explicit Substitutions: The Case of
                  Higher-Order Patterns",
  booktitle = 	 "Proceedings of the Joint International Conference and
                  Symposium on Logic Programming",
  editor = 	 "M. Maher",
  year = 	 "1996",
  publisher =    "MIT Press",
  address = 	 "Bonn, Germany",
  month = 	 sep,
  pages =        "259--273",
  notes =        "Extended version available as Rapport de Recherche No.~3591,
		  INRIA, December 1998",
  keywords =     "unification",
  urldvi = 	 "http://www.cs.cmu.edu/~fp/papers/jicslp96.dvi.gz",
  urlps = 	 "http://www.cs.cmu.edu/~fp/papers/jicslp96.ps.gz"
}

@inproceedings{ expsubs,
    author = "Mart\'{\i}n Abadi and Luca Cardelli and Pierre-Louis Curien and Jean-Jacques L\`{e}vy",
    title = "Explicit Substitutions",
    booktitle = "Conference Record of the Seventeenth Annual {ACM} Symposium on Principles of Programming Languages, San Francisco, California",
    publisher = "ACM",
    pages = "31--46",
    year = "1990",
    url = "citeseer.nj.nec.com/abadi91explicit.html" 
}



@techreport {jcreed.st02,
author="Jason Reed",
title="Proof Irrelevance and Strict Definitions in a Logical Framework",
year="2002",
institution = "Carnegie Mellon University",
number =	 "CMU-CS-02-153"
}

@inproceedings{ necula.pcc,
  author =       "George C. Necula and Peter Lee",
  title =        "Proof-Carrying Code",
  booktitle =    "Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Langauges (POPL '97)",
  month =        Jan,
  address =      "Paris",
  pages =        "106--119",
  year =         1997,
  url = "citeseer.nj.nec.com/50371.html" 
}

@InProceedings{optimizing.ho.unification,
  author =       {Brigitte Pientka and Frank Pfenning},
  title =        {Optimizing Higher-Order Pattern Unification},
  booktitle =    {Proceedings of the 19th Conference on Automated Deduction
                  (CADE-19)},
  OPTpages =     {},
  year =         2003,
  editor =       {F. Baader},
  address =      {Miami Beach, Florida},
  month =        jul,
  publisher =    {Springer-Verlag LNCS},
  note =         {To appear},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/optunif03.pdf},
  urlps =        {http://www.cs.cmu.edu/~fp/papers/optunif03.ps}
}

@techreport {crary.sarkar.03,
author = "Karl Crary and Susmit Sarkar",
title = {A Metalogical Approach to Foundational Certified Code},
institution = "Carnegie Mellon University",
number = {CMU-CS-03-108},
month = Jan,
year = 2003,
}

@unpublished{jcreed.hopu,
author="Jason Reed",
title="Higher-Order Pattern Unification and Proof Irrelevance",
year="2002",
note = "Appears in TPHOLs 2002 Track B proceedings, NASA tech report CP-2002-211736"
}

@article{ miller.pats,
  Author = "Dale Miller",
  Title = "A Logic Programming Language with Lambda-Abstraction,
    Function Variables, and Simple Unification",
  Journal = "Journal of Logic and Computation",
  Volume = "1",
  Number = "4",
  Pages = "497-536",
  Year = "1991",
  URL = "citeseer.nj.nec.com/miller91logic.html",
  URL = "file://ftp.cis.upenn.edu/pub/papers/miller/jlc91.dvi.Z" 
}

@article{ rlf98,
    author = "Samin S. Ishtiaq and David J. Pym",
    title = "A Relevant Analysis of Natural Deduction",
    journal = "Journal of Logic and Computation",
    volume = "8",
    number = "6",
    pages = "809-838",
    year = "1998",
}

@phdthesis{ishtiaq.thesis,
  title={A Relevant Analysis of Natural Deduction},
  author={Samin S. Ishtiaq},
  school={Queen Mary and Westfield College, University of London},
  year={1999},
}

@unpublished{mllf03,
author = {Andrew McCreight and Carsten Sch{\"u}rmann},
title = "A Meta Linear Logical Framework",
year = 2003,
url = {http://www.itu.dk/people/carsten/papers/mllf.pdf},
note = {Draft manuscript.},
}

@article{ andreoli.focusing92,
    author = "Andreoli, J. M.",
    title = "Logic programming with focusing proofs in linear logic",
    journal = "Journal of Logic and Computation",
    volume = "2",
    number = "3",
    pages = "297--347",
    year = "1992",
}

@article{galmiche.mery03,
  title={{Semantic Labelled Tableaux for Propositional BI}},
  author={Didier Galmiche and Daniel M{\'e}ry},
  journal={Journal of Logic and Computation},
  volume={13},
  number={5},
  pages={707-753},
  year={2003}
}

@article{depaiva.towards03,
  title={{Towards constructive hybrid logic}},
  author={Bra{\"u}ner, T. and de Paiva, V.},
  journal={Elec. Proc. of Methods for Modalities},
  volume={3},
  year={2003}
}

@unpublished{depaiva.ihl,
title = {Intuitionistic Hybrid Logic},
author = {Torben Bra{\"u}ner and Valeria de Paiva.},
year = {2006},
journal = {Journal of Applied Logic.},
note={To appear.},
}

% URL={{http://www.cs.bham.ac.uk/~vdp/publications/IntuitionisticHybrid.pdf}},
@techreport{jia.walker03,
  author = 	 "Limin Jia and David Walker",
  title = 	 "Modal Proofs as Distributed Programs",
  institution =  "Princeton University",
  year = 	 2003,
  number =	 "TR-671-03",
  month =	 aug,

}

@TechReport{moody03,
  author = 	 {Jonathan Moody},
  title = 	 {Modal Logic as a Basis for Distributed Computation},
  institution =  {Carnegie Mellon University},
  year = 	 {2003},
  OPTkey = 	 {},
  OPTtype = 	 {},
  number = 	 {CMU-CS-03-194},
  OPTaddress = 	 {},
  month = 	 oct,
  OPTnote = 	 {},
  OPTannote = 	 {}
}


@article{chadha06,
  title={{A Hybrid Intuitionistic Logic: Semantics and Decidability}},
  author={Chadha, R. and Macedonio, D. and Sassone, V.},
  journal={Journal of Logic and Computation},
  volume={16},
  number={1},
  pages={27},
  year={2006}
}

% deprecated in favor of Murphy04lics
% article{smlc04,
%   title={{A Symmetric Modal Lambda Calculus for Distributed Computing}},
%   author={Murphy, VII, Thomas and Crary, K. and Harper, R. and Pfenning, F.},
%   journal={Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04)-Volume 00},
%   pages={286-295},
%   year={2004},
%   publisher={IEEE Computer Society Washington, DC, USA}
% }

@inproceedings{ coverage.check,
  author =	 "Carsten Sch{\"u}rmann and Frank Pfenning",
  title =	 "A coverage checking algorithm for {LF}",
  booktitle =	 {Proceedings of the Theorem Proving in Higher Order
                  Logics 16th International Conference},
  pages =	 {120--135},
  year =	 2003,
  editor =	 {Basin, D. and Wolff, B.},
  volume =	 2758,
  series =	 {LNCS},
  publisher =	 {Springer},
  address =	 {Rome, Italy},
  month =	 sep,
}

@techreport{clf1,
  title={{A concurrent logical framework I: Judgments and properties}},
  author={Kevin Watkins and Iliano Cervesato and Frank Pfenning and David Walker},
  number={CMU-CS-02-101},
  institution ={Department of Computer Science},
  year=2003,
}

@techreport{clf2,
  title={{A concurrent logical framework II: Examples and applications}},
  author={Kevin Watkins and Iliano Cervesato and Frank Pfenning and David Walker},
  number={CMU-CS-02-102},
  institution ={Department of Computer Science},
  year=2003,
}


@Book{fitting69,
title = "Intuitionistic Logic, Model Theory, and Forcing",
publisher = "North-Holland Publishing Co.",
city = "Amsterdam",
year = "1969",
author = "Melvin Fitting",
}

@TechReport{gabbay90,
title = "Labelled Deductive Systems",
author = "Dov Gabbay",
institution = "University of Munich",
number = "90-22",
year = "1990",
}

@article{llf02,
 author = {Iliano Cervesato and Frank Pfenning},
 title = {A linear logical framework},
 journal = {Inf. Comput.},
 volume = {179},
 number = {1},
 year = {2002},
 issn = {0890-5401},
 pages = {19--75},
 doi = {http://dx.doi.org/10.1006/inco.2001.2951},
 publisher = {Academic Press, Inc.},
 address = {Duluth, MN, USA},
 }


@article{bi99,
author = "P.W. O'Hearn and D.J. Pym",
title ="The Logic of Bunched Implications",
journal ="Bulletin of Symbolic Logic",
volume="5",
number="2",
pages ="215-244",
year = "1999",
}

@TechReport{carsten.thesis,
  author = 	 "Carsten Sch{\"u}rmann",
  title = 	 "Automating the Meta-Theory of Deductive Systems",
  institution =  "Department of Computer Science, Carnegie Mellon University",
  year = 	 2000,
  number =	 "CMU-CS-00-146",
}


@article{hybrid01,
  title={{Hybrid logics: Characterization, interpolation and complexity}},
  author={Areces, C. and Blackburn, P. and Marx, M.},
  journal={Journal of Symbolic Logic},
  volume={66},
  number={3},
  pages={977--1010},
  year={2001}
}

@article{hybrid.manifesto00,
  title={{Representation, reasoning, and relational structures: a hybrid logic manifesto}},
  author={Blackburn, P.},
  journal={Logic Journal of IGPL},
  volume={8},
  number={3},
  pages={339-365},
  year={2000}
}

@book{vigano.book00,
  title={{Labelled Non-Classical Logics}},
  author={Vigan{\`o}, L.},
  year={2000},
  publisher={Kluwer Academic Publishers}
}

@article{fibring02,
  title={{Fibring labelled deduction systems}},
  author={Rasga, J. and Sernadas, A. and Sernadas, C. and Vigano, L.},
  journal={Journal of Logic and Computation},
  volume={12},
  number={3},
  pages={443-473},
  year={2002}
}

@article{linear87,
  title={{Linear logic}},
  author={Girard, J.Y.},
  journal={Theoretical Computer Science},
  volume={50},
  number={1},
  pages={1-102},
  year={1987},
  publisher={Elsevier Science Publishers Ltd. Essex, UK}
}

@inproceedings{wright93,
  title={{Usage Analysis with Natural Reduction Types}},
  author={Wright, D.A. and Baker-Finch, C.A.},
  booktitle={Proceedings of the Third International Workshop on Static Analysis},
  pages={254-266},
  year={1993},
  publisher={Springer-Verlag London, UK}
}

@techreport{ judgmental.linear03,
  author = "Bor-Yuh Evan Chang and Kaustuv Chaudhuri and Frank Pfenning",
  title = "A judgmental analysis of linear logic",
  number = "CMU-CS-03-131",
  institution = "Carnegie Mellon University",
  year = "2003",
}

@unpublished{jcreed.hlfdraft,
author = {Jason Reed},
title = "Canonical Forms in A Hybrid Logical Framework",
year = 2006,
url = {http://www.cs.cmu.edu/~jcreed/papers/cfhlf.pdf},
note = {Draft manuscript.},
}

@INPROCEEDINGS{HardtSmolkaHOSHybrid06,
  title = {Higher-Order Syntax and Saturation Algorithms for Hybrid  Logic},
  year = {2006},
  author = {Moritz Hardt and Gert Smolka},
  booktitle = {Proceedings of HyLo 2006},
  note = {To Appear},
  series = {Electronic Notes in Theoretical Computer Science},
  label = {HardtSmolkaHOSHybrid06}
}

@article{fruhwirth1998tap,
  title={{Theory and practice of constraint handling rules}},
  author={Fr{\"u}hwirth, T.},
  journal={The Journal of Logic Programming},
  volume={37},
  number={1},
  pages={95--138},
  year={1998},
  publisher={Elsevier Science}
}

@inproceedings{ linear-hounif,
    author = "Iliano Cervesato and Frank Pfenning",
    title = "Linear Higher-Order Pre-Unification",
    booktitle = "Twelfth Annual Symposium on Logic in Computer Science --- {LICS}'97",
    month = "29 -- 2",
    publisher = "IEEE Computer Society Press",
    address = "Warsaw, Poland",
    editor = "G. Winskel",
    pages = "422--433",
    year = "1997",
    url = "citeseer.ist.psu.edu/article/cervesato97linear.html" }

@article{pfenning91lp,
  title={{Logic programming in the LF logical framework}},
  author={Pfenning, F.},
  journal={Logical Frameworks},
  pages={149--181},
  year={1991}
}


@InProceedings{hodas92,
  title={{Lolli: an extension of $\lambda$Prolog with linear logic context management}},
  author={Hodas, J.S.},
  booktitle={Proceedings of the 1992 workshop on the $\lambda$Prolog programming language, Philadelphia},
  year={1992}
}

@phdthesis{polakowthesis,
  title={Ordered Linear Logic and Applications},
  author={Jeff Polakow},
  school={Carnegie Mellon University School of Computer Science},
  year={2001}
}


@inproceedings{polakow00olp,
 author = {Jeff Polakow},
 title = {Linear logic programming with an ordered context},
 booktitle = {PPDP '00: Proceedings of the 2nd ACM SIGPLAN international conference on Principles and practice of declarative programming},
 year = {2000},
 isbn = {1-58113-265-4},
 pages = {68--79},
 location = {Montreal, Quebec, Canada},
 doi = {http://doi.acm.org/10.1145/351268.351277},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }

@article{hodasmiller91,
  title={{Logic programming in a fragment of intuitionistic linear logic}},
  author={Hodas, Joshua S. and Miller, D.},
  journal={Logic in Computer Science, 1991. LICS'91., Proceedings of Sixth Annual IEEE Symposium on},
  pages={32--42},
  year={1991}
}

@phdthesis{hodasthesis,
  title={{Logic Programming in Intuitionistic Linear Logic}},
  author={Hodas, J.},
  school={University of Pennsylvania, Department of Computer and Information Science},
  year={1994}
}


@article{ miller95survey,
    author = "Dale Miller",
    title = "A Survey of Linear Logic Programming",
    journal = "Computational Logic: The Newsletter of the European Network in Computational Logic",
    volume = "2",
    number = "2",
    pages = "63--67",
    year = "1995",
    url = "citeseer.ist.psu.edu/miller95survey.html" }

@misc{ miller04survey,
  author = "D. Miller",
  title = "An overview of linear logic programming",
  note = "To appear in a book
    on linear logic, edited by Thomas Ehrhard, Jean-Yves Girard, Paul Ruet,
    and Phil Scott. Cambridge University Press.",
  url = "citeseer.ist.psu.edu/636770.html",
  year = "2004", }


@article {lambek58,
 author = "Joachim Lambek",
 title = "The Mathematics of Sentence Structure",
 journal = "American Mathematical Monthly",
 number = 3,
 volume = 65,
 pages = "154-170",
 year = "1958",
}

@inproceedings{debruijn90plea,
  title={{A plea for weaker frameworks}},
  author={de Bruijn, NG},
  booktitle={Proc. First Workshop on Logical Frameworks: Design, Implementation, and Experiment},
  year={1990},
}

@article {gentzen35,
author = "Gerhard Gentzen",
title = "Untersuchungen {\"u}ber das logische Schlieen",
 journal = "Mathematische Zeitschrift",
 volume = "39", pages = "176-210, 405-431", year ="1935",
}

@article{stickel81,
author = "Mark E. Stickel",
journal = "Journal of the ACM",
volume = "28",
number = "3",
pages = "423-434",
year = "1981",
title = "A Unification Algorithm for Associative-Commutative Functions",
}

@inproceedings{jcreed06.hlf,
  title={Hybridizing a Logical Framework},
  author={Jason Reed},
  booktitle={Proceedings of the International Workshop on Hybrid Logic 2006},
  publisher={Elsevier},
  note={To be published},
  year={2006},
}

@article{ ohearn02bunched,
  journal = "Journal of Functional Programming",
  author = "P. O'Hearn",
  title = "On bunched typing",
  year = "2003",
  volume= 13,
  number = 4,
  month = {July},
}

@inproceedings{ pym99bunched,
    author = "David J. Pym",
    title = "On Bunched Predicate Logic",
    booktitle = "Proceedings of the 14th Annual Symposium on Logic in Computer Science ({LICS}'99)",
    publisher = "IEEE Computer Society Press",
    address = "Trento, Italy",
    editor = "G. Longo",
    pages = "183--192",
    year = "1999",
    url = "citeseer.ist.psu.edu/pym99bunched.html" }

@book{PymMono,
title={The Semantics and Proof Theory of the Logic of the Logic of Bunched Implications},
author={D.J. Pym},
year={2002},
publisher={Kluwer Academic Publishers},
series={Applied Logic Series},
volume={26},
}

@article{POY,
author = "D.J. Pym and P.W. O'Hearn and H. Yang",
title = "Possible Worlds and Resources: The Semantics of {BI}",
year = "2004",
journal="Theoretical Computer Science",
volume="315",
number="1",
pages="257--305"
}

@article{duggan.extended,
title = "Unification with Extended Patterns",
author = "Dominic Duggan",
journal = "Theoretical Computer Science",
volume = "206",
number = "1",
pages = "1-50",
year = "1998",
}

@article{girard2001lsr,
  title={{Locus Solum: From the rules of logic to the logic of rules}},
  author={Girard, J.Y.},
  journal={Mathematical Structures in Computer Science},
  volume={11},
  number={03},
  pages={301--506},
  year={2001},
  publisher={CambridgeUnivPress}
}

@inproceedings{lollimon,
 author = {Pablo L{\'o}pez and Frank Pfenning and Jeff Polakow and Kevin Watkins},
 title = {Monadic concurrent linear logic programming},
 booktitle = {PPDP '05: Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming},
 year = {2005},
 isbn = {1-59593-090-6},
 pages = {35--46},
 location = {Lisbon, Portugal},
 doi = {http://doi.acm.org/10.1145/1069774.1069778},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }

% deprecated in favor of Pfenning00ic, Pfenning95lics
% article{structural.cut,
% author = {Frank Pfenning},
% title = {Structural Cut Elimination},
% journal = {lics},
% volume = {00},
% year = {1995},
% issn = {1043-6871},
% pages = {156},
% doi = {http://doi.ieeecomputersociety.org/10.1109/LICS.1995.523253},
% publisher = {IEEE Computer Society},
% address = {Los Alamitos, CA, USA},
% }

@techreport{ pfenning94structural,
    author = "Frank Pfenning",
    title = "Structural cut elimination in linear logic",
    number = "CS-94-222",
    year = "1994",
    url = "citeseer.ist.psu.edu/pfenning94structural.html",
    institution = "Carnegie Mellon University",
 }

@article{miller.forum,
 author = "D. Miller",
 title = "A Multiple-Conclusion Meta-Logic",
 journal = "Theoretical Computer Science",
 volume = "165",
 number = "1",
 pages = "201-232",
 year = "1996",
}

@phdthesis{ virga.thesis,
    author = "Roberto Virga",
    title = "Higher-Order Rewriting with Dependent Types",
    year = "1999",
    url = "citeseer.ist.psu.edu/virga99higherorder.html",
    school = "Carnegie Mellon University", }

@inproceedings{andreoli.lo,
 author = {Jean-Marc Andreoli and Remo Pareschi},
 title = {LO and behold! Concurrent structured processes},
 booktitle = {OOPSLA/ECOOP '90: Proceedings of the European conference on object-oriented programming on Object-oriented programming systems, languages, and applications},
 year = {1990},
 isbn = {0-201-52430-X},
 pages = {44--56},
 location = {Ottawa, Canada},
 doi = {http://doi.acm.org/10.1145/97945.97953},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }

% from frank
		  
@Article{Cervesato00tcs,
  author = 	 "Iliano Cervesato and Joshua S. Hodas and Frank Pfenning",
  title = 	 "Efficient Resource Management for Linear Logic Proof Search",
  journal =	 "Theoretical Computer Science",
  year =	 2000,
  volume =       232,
  number =       "1--2",
  month =        feb,
  pages =        "133--163",
  note =	 "Special issue on Proof Search in
		  Type-Theoretic Languages, D. Galmiche and D. Pym, editors",
  keywords =	 "LF, Elf, linear",
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/erm97.pdf",
  urlps =	 "http://www.cs.cmu.edu/~fp/papers/erm97.ps"
}

@Article{Hodas94ic,
  author =	"Joshua Hodas and Dale Miller",
  title =	"Logic Programming in a Fragment of Intuitionistic Linear
		  Logic", 
  journal =	"Information and Computation",
  year =	"1994",
  volume=	"110",
  number=	"2",
  pages=	"327--365",
  note =	"A preliminary version appeared in the Proceedings of the
		  Sixth Annual IEEE Symposium on Logic in Computer Science,
		  pages 32--42, Amsterdam, The Netherlands, July 1991",
  urlps =	"file://ftp.cis.upenn.edu/pub/papers/miller/ic94.ps.Z",
  keywords =	"linear"
}

@Article{Harper05tocl,
  author = 	 {Robert Harper and Frank Pfenning},
  title = 	 {On Equivalence and Canonical Forms in the {LF} Type Theory},
  journal = 	 {Transactions on Computational Logic},
  year = 	 2005,
  month =        jan,
  volume =       6,
  issue =        1,
  pages =        {61--101},
  keywords =     {LF, Elf},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/tocl05.pdf},
  urlps =        {http://www.cs.cmu.edu/~fp/papers/tocl05.ps}
}

@InProceedings{Murphy04lics,
  author = 	 {Tom Murphy~VII and Karl Crary and Robert Harper and Frank Pfenning},
  title = 	 {A Symmetric Modal Lambda Calculus for Distributed Computing},
  booktitle = 	 {Proceedings of the 19th Annual Symposium on Logic in
                  Computer Science (LICS'04)},
  pages =	 {286--295},
  year =	 2004,
  editor =	 {H. Ganzinger},
  address =	 {Turku, Finland},
  month =	 jul,
  publisher =	 {IEEE Computer Society Press},
  note =         {Extended version available as Technical Report
                  CMU-CS-04-105},
  urlpdf =       {http://www.cs.cmu.edu/~fp/papers/lics04.pdf},
  urlps =        {http://www.cs.cmu.edu/~fp/papers/lics04.ps}
}

@Article{Pfenning00ic,
  author = 	 "Frank Pfenning",
  title = 	 "Structural Cut Elimination {I}.  Intuitionistic and
		  Classical Logic",
  journal =	 "Information and Computation",
  year =	 2000,
  volume =	 157,
  number =	 "1/2",
  pages =	 "84--141",
  month =	 mar,
  urlpdf =	 "http://www.idealibrary.com/links/artid/inco.1999.2832/production/pdf",
  keywords =	 "LF, Elf"
}

@InProceedings{Pfenning95lics,
  author = 	 "Frank Pfenning",
  title = 	 "Structural Cut Elimination",
  editor =	 "D. Kozen",
  booktitle =	 "Proceedings of the Tenth Annual Symposium on Logic in
		  Computer Science",
  year =	 1995,
  publisher =	 "IEEE Computer Society Press",
  address =	 "San Diego, California",
  month =	 "June",
  pages =	 "156--166",
  keywords =     "LF, Elf, linear",
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/lics95.pdf",
  urlps =	 "http://www.cs.cmu.edu/~fp/papers/lics95.ps"
}

@PhdThesis{Schurmann00phd,
  author = 	 "Carsten Sch{\"u}rmann",
  title = 	 "Automating the Meta Theory of Deductive Systems",
  school = 	 "Department of Computer Science, Carnegie Mellon University",
  year = 	 2000,
  month =	 aug,
  note =	 "Available as Technical Report CMU-CS-00-146",
  keywords =	 "LF, Elf",
  urlps =	 "http://cs-www.cs.yale.edu/homes/carsten/papers/S00b.ps"
}

@InProceedings{Pfenning99cade,
  author = 	 "Frank Pfenning and Carsten Sch{\"u}rmann",
  title = 	 "System Description: Twelf --- A Meta-Logical Framework for
		  Deductive Systems",
  editor =	 "H. Ganzinger",
  pages =        "202--206",
  booktitle =	 "Proceedings of the 16th International Conference on
		  Automated Deduction (CADE-16)",
  year =	 1999,
  publisher =	 "Springer-Verlag LNAI 1632",
  address =	 "Trento, Italy",
  month =	 jul,
  keywords =	 "LF, Elf",
  urlpdf =	 "http://www.cs.cmu.edu/~fp/papers/cade99.pdf",
  urlps =	 "http://www.cs.cmu.edu/~fp/papers/cade99.ps"
}

@Article{siena.lectures,
  author = 	 "Per Martin-L{\"o}f",
  title = 	 "On the meanings of the logical constants and the justifications of the logical laws",
  journal =	 "Nordic Journal of Philosophical Logic",
  year =	 1996,
  volume =	 1,
  number =	 "1",
  pages =	 "11--60",
}

@inproceedings{httsep,
 author = {Aleksandar Nanevski and Greg Morrisett and Lars Birkedal},
 title = {Polymorphism and separation in hoare type theory},
 booktitle = {ICFP '06: Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming},
 year = {2006},
 isbn = {1-59593-309-3},
 pages = {62--73},
 location = {Portland, Oregon, USA},
 doi = {http://doi.acm.org/10.1145/1159803.1159812},
 publisher = {ACM},
 address = {New York, NY, USA},
 }