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},
}