AA00

@techreport{AA00,
	author = "Jesse Alt and Sergei Artemov",
	institution = {Cornell University},
	number = {CFIS 2000-06},
	title = "Reflective $\lambda$-calculus",
	year = 2000,
}

AA01

@string{LNCS = "Lecture Notes in Computer Science"}
@inproceedings{AA01,
	author = "Jesse Alt and Sergei Artemov",
	booktitle = "Proceedings of the Dagstuhl-Seminar on Proof Theory in Computer Science",
	pages = "22--37",
	publisher = "Springer",
	series = LNCS,
	title = "Reflective $\lambda$-calculus",
	volume = 2183,
	year = 2001,
}

AA99

@string{Sep = "September"}
@techreport{AA99,
	address = {Ithaca, New York},
	author = {Eric Aaron and Stuart Allen},
	institution = {Cornell University},
	month = Sep,
	number = {TR99-1771},
	title = {Justifying Calculational Logic by a Conventional Metalinguistic Semantics},
	url = {http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR99-1771},
	year = 1999,
}

aastudy

@misc{aastudy,
	key = "NSF01",
	title = "National {S}cience {F}oundation. {B}lack Issues in Higher Education, 2001 Annual Survey",
}

AAW03

@string{nov = "November"}
@techreport{AAW03,
	author = {Albrecht, K. and Arnold, R. and Wattenhofer, R.},
	institution = {Department of Computer Science, ETH Zurich},
	month = nov,
	number = 427,
	title = {Join and Leave in Peer-to-Peer Systems:  The {DASIS} Approach},
	year = 2003,
}

Aba94

@string{Apr = "April"}
@string{JFP = "Journal of Functional Programming"}
@article{Aba94,
	author = {Martin Abadi},
	journal = JFP,
	month = Apr,
	number = 2,
	title = {Baby {M}odula--3 and a theory of objects},
	volume = 4,
	year = 1994,
}

ABB93

@incollection{ABB93,
	author = {Anderson, J. R. and F. S. Bellezza and C. F. Boyle},
	booktitle = {Rules of the Mind},
	chapter = 8,
	editor = {J. R. Anderson},
	publisher = {Erlbaum},
	title = {The Geometry Tutor and Skill Acquisition},
	year = 1993,
}

ABC02

@string{May = "May"}
@misc{ABC02,
	author = {Stuart Allen and Mark Bickford and Robert Constable and others},
	howpublished = {PostScript document on website},
	month = May,
	note = {\url{http://www.nuprl.org/html/FDLProject/02cucs-fdl.html}},
	title = {{FDL}: A Prototype Formal Digital Library},
	year = 2002,
}

ABC06

@techreport{ABC06,
	address = {Ithaca, NY},
	author = {Allen, Stuart F. and Mark Bickford and Robert L. Constable},
	institution = {Cornell University},
	note = {To be published, March 2006},
	title = {An Abstract Account of Atoms},
	year = 2006,
}

ABC82

@string{Jun = "June"}
@article{ABC82,
	author = {Adrion, W. R. and M. A. Branstad and J. C. Cherniavsy},
	journal = {Computing Surveys},
	month = Jun,
	number = 2,
	pages = {159--192},
	title = {Validation, Verification, and Testing of Computer Software},
	volume = 14,
	year = 1982,
}

ABCEK03

@techreport{ABCEK03,
	address = {Ithaca, New York},
	author = {Allen, Stuart F. and Mark Bickford and Robert Constable and Richard Eaton and Christoph Kreitz},
	institution = {Cornell University},
	number = {TR2003-1889},
	title = {A {\Nuprl}--{\PVS} Connection: {I}ntegrating Libraries of Formal Mathematics},
	year = 2003,
}

ABCEKLM05

@unpublished{ABCEKLM05,
	author = {Allen, Stuart F. and Mark Bickford and Robert Constable and Richard Eaton and Christoph Kreitz and Lori Lorigo and Evan Moran},
	journal = {Journal of Applied Logic},
	note = {To appear in 2006},
	publisher = {Elsevier Science},
	title = {Innovations in Computational Type Theory using {\Nuprl}},
	year = 2006,
}

Abe91

@string{Nov = "November"}
@techreport{Abe91,
	address = {Berkeley, CA  94704},
	author = {K. Aberer},
	institution = {International Computer Science Institute},
	month = Nov,
	note = {Submitted to Journal of Symbolic Computation},
	number = {TR-91-061},
	title = {Combinatory Differential Fields:  An Algebraic Approach to Approximate Computation and Constructive Analysis},
	year = 1991,
}

ABF+05

@misc{ABF+05,
	author = {Brian E. Aydemir and Aaron Bohannon and Matthew Fairbairn and J. Nathan Foster and Benjamin C. Pierce and Peter Sewell and Dimitrios Vytiniotis and Geoffrey Washburn and Stephanie Weirich and Steve Zdancewic},
	howpublished = {Available from \url{http://www.cis.upenn.edu/group/proj/plclub/mmm/}},
	title = {Mechanized Metatheory for the Masses: {T}he {\POPLmark} Challenge},
	year = 2005,
}

ABFR87

@incollection{ABFR87,
	author = {Anderson, J. R. and C. F. Boyle and R. Farrell and B. J. Reiser},
	booktitle = {Modeling Cognition},
	editor = {P. Morris},
	publisher = {Wiley},
	title = {Cognitive Principles in the Design of Computer Tutors},
	year = 1987,
}

ABI94

@string{Jun = "June"}
@techreport{ABI94,
	address = {Pittsburgh, PA},
	author = {Andrews, P. B. and M. Bishop and S. Issar and D. Nesmith and F. Pfenning and H. Xi},
	institution = {Carnegie Mellon University},
	month = Jun,
	number = {94--166},
	title = {{\TPS}: {A} Theorem Proving System For Classical Type Theory},
	type = {Department of Mathematics},
	year = 1994,
}

Abr00

@inproceedings{Abr00,
	author = {Abramsky, S.},
	booktitle = {Foundations of Secure Computation: Proceedings of the 1999 Marktoberdorf Summer School},
	editor = {F. L. Bauer and R. Steinbr{\"u}ggen},
	pages = {167--180},
	publisher = {IOS Press},
	title = {Process Realizability},
	year = 2000,
}

Abr00b

@incollection{Abr00b,
	author = {Abramsky, S.},
	booktitle = {Millennial Perspectives in Computer Science},
	editor = {J. Davies, A. W. Roscoe and J. Woodcock},
	pages = {1--12},
	publisher = {Palgrave},
	title = {Concurrent Interaction Games},
	year = 2000,
}

Abr90

@incollection{Abr90,
	author = {Abramsky, S.},
	booktitle = {Logical Foundations of Functional Programming},
	editor = {D.~A.~Turner},
	pages = {65--116},
	publisher = {Addison-Wesley},
	title = {The lazy $\lambda$-calculus},
	year = 1990,
}

Abr93

@string{TCS = "Journal of Theoretical Computer Science"}
@article{Abr93,
	author = {Abramsky, S.},
	journal = TCS,
	number = {1--2},
	pages = {3--57},
	title = {Computational Interpretations of Linear Logic},
	volume = 111,
	year = 1993,
}

Abr94

@string{TCS = "Journal of Theoretical Computer Science"}
@article{Abr94,
	author = {Abramsky, S.},
	journal = TCS,
	number = 1,
	pages = {5--9},
	title = {Proofs as Processes},
	volume = 135,
	year = 1994,
}

Abr95

@string{TCS = "Journal of Theoretical Computer Science"}
@article{Abr95,
	author = {Uri Abraham},
	journal = TCS,
	pages = {257--298},
	title = {On interprocess communication and the implementation of multi-writer atomic registers},
	volume = 149,
	year = 1995,
}

Abr97

@incollection{Abr97,
	author = {S. Abramsky},
	booktitle = {Semantics and Logics of Computation},
	editor = {P. Dybjer and A. M. Pitts},
	publisher = {Cambridge Univ. Press},
	title = {Semantics of interaction: an introduction to game semantics},
	year = 1997,
}

Abr99

@book{Abr99,
	author = {Uri Abraham},
	publisher = {Gordon and Breach},
	series = {Algebra, Logic and Applications Series},
	title = {Models for Concurrency},
	volume = 11,
	year = 1999,
}

ABY86

@article{ABY86,
	author = {Anderson, J. R. and C. F. Boyle and G. Yost},
	journal = {The Journal of Mathematical Behavior},
	number = 20,
	title = {The Geometry Tutor},
	volume = 5,
	year = 1986,
}

AC03

@techreport{AC03,
	author = {Stuart Allen and Robert L. Constable},
	institution = {Cornell University, Computer Science Department},
	title = {Enabling Large Scale Coherency Among Mathematical Texts in the {NSDL}},
	year = 2003,
}

AC05

@unpublished{AC05,
	author = "Allen, Stuart and Constable, Robert",
	note = "Submitted to Journal of Digital Information, sponsored by British Computer Society and Oxford University Press.   This paper elaborates ideas from our previous NSDL targeted research proposal, \url{http://www.nuprl.org/documents/Allen/EnablingLargeScale.html}",
	title = "Enabling Large Scale Coherency Among Mathematical Texts",
	year = 2005,
}

AC06

@string{Feb = "February"}
@techreport{AC06,
	address = {Ithaca, NY},
	author = {Allen, Stuart F. and Robert L. Constable},
	institution = {Cornell University},
	month = Feb,
	number = {TR2006-2014},
	title = {Enabling Large Scale Coherency Among Mathematics Texts},
	type = {Department of Computer Science},
	year = 2006,
}

AC92

@techreport{AC92,
	author = {Aitken, William and Robert L. Constable},
	institution = {Cornell University, Computer Science Department, Ithaca, NY},
	title = {Reflecting on {\Nuprl} : {L}essons 1--4},
	year = 1992,
}

AC92a

@unpublished{AC92a,
	author = {Aitken, William and Robert L. Constable},
	note = {Unpublished, {C}ornell {U}niversity},
	title = {An inductive definition of evaluation in {\Nuprl}},
	year = 1993,
}

AC94

@inproceedings{AC94,
	author = {Abadi, Mart{\'i}n and Luca Cardelli},
	crossref = {LICS94},
	pages = {332--341},
	title = {A Semantics of Object Types},
}

Fully expanded entry:

@string{Jul = "July"}
@inproceedings{AC94,
	address = {Paris, France},
	author = {Abadi, Mart{\'i}n and Luca Cardelli},
	booktitle = {Proceedings of 9$^{th}$ IEEE Symposium on Logic in Computer Science},
	key = {LICS94},
	month = Jul,
	pages = {332--341},
	publisher = {IEEE Computer Society Press},
	title = {A Semantics of Object Types},
	year = 1994,
}

AC96

@book{AC96,
	author = {Abadi, Mart{\'i}n and Luca Cardelli},
	publisher = {Springer},
	title = {A Theory of Objects},
	year = 1996,
}

AC96a

@inproceedings{AC96a,
	author = {David Aspinall and Adriana Compagnoni},
	crossref = {LICS96},
	note = {Final draft to appear in Theoretical Computer Science, 2000},
	pages = {86--97},
	title = {Subtyping Dependent Types},
}

Fully expanded entry:

@inproceedings{AC96a,
	address = "New Brunswick, New Jersey",
	author = {David Aspinall and Adriana Compagnoni},
	booktitle = {Proceedings of 11$^{th}$ IEEE Symposium on Logic in Computer Science},
	editor = "E. Clarke",
	key = {LICS96},
	month = "July 27--30",
	note = {Final draft to appear in Theoretical Computer Science, 2000},
	pages = {86--97},
	publisher = "IEEE Computer Society Press",
	title = {Subtyping Dependent Types},
	year = 1996,
}

AC98

@book{AC98,
	address = {Cambridge},
	author = {Amadio, Roberto M. and Pierre-Louis Curien},
	number = 46,
	publisher = {Cambridge University Press},
	series = {Cambridge Tracts in Theoretical Computer Science},
	title = {Domains and lambda-calculi},
	year = 1998,
}

ACC01

@misc{ACC01,
	author = {Stuart Allen and James Caldwell and Robert Constable},
	howpublished = {Extended abstract of presentation originally entitled \emph{Interactive Digital Libraries of Formalized Algorithmic Knowledge,} given at the First International Workshop on Mathematical Knowledge Management},
	note = {\url{http://www.nuprl.org/documents/Allen/01mkm-diglib.html}},
	title = {Logical Aspects of Digital Mathematics Libraries},
	year = 2001,
}

ACCL91

@string{JFP = "Journal of Functional Programming"}
@article{ACCL91,
	author = {Abadi, Mart{\'i}n and Luca Cardelli and Pierre-Louis Curien and Jean-Jacques L{\'e}vy},
	journal = JFP,
	number = 4,
	pages = {375--416},
	title = {Explicit Substitutions},
	volume = 1,
	year = 1991,
}

ACEKL00

@inproceedings{ACEKL00,
	author = {Stuart Allen and Robert Constable and Richard Eaton and Christoph Kreitz and Lori Lorigo},
	crossref = {CADE00},
	pages = {170--176},
	title = {The {\Nuprl} Open Logical Environment},
}

Fully expanded entry:

@string{LNAI = "Lecture Notes in Artificial Intelligence"}
@inproceedings{ACEKL00,
	author = {Stuart Allen and Robert Constable and Richard Eaton and Christoph Kreitz and Lori Lorigo},
	booktitle = {Proceedings of the 17$^{th}$ International Conference on Automated Deduction},
	editor = {David McAllester},
	pages = {170--176},
	publisher = {Springer Verlag},
	series = LNAI,
	title = {The {\Nuprl} Open Logical Environment},
	volume = 1831,
	year = 2000,
}

ACF04

@techreport{ACF04,
	author = {Stuart F. Allen and  Robert L. Constable and Matthew Fluet},
	institution = {Department Computer Science, Cornell University},
	number = {TR2004-1933},
	title = {Expressing and Implementing the Computational Content Implicit in Smullyan's Account of Boolean Valuations},
	year = 2004,
}

ACHA90

@inproceedings{ACHA90,
	author = {Allen, Stuart F. and Robert L. Constable and Douglas J. Howe and William Aitken},
	crossref = {LICS90},
	pages = {95--197},
	title = {The Semantics of Reflected Proof},
}

Fully expanded entry:

@string{Jun = "June"}
@inproceedings{ACHA90,
	author = {Allen, Stuart F. and Robert L. Constable and Douglas J. Howe and William Aitken},
	booktitle = {Proceedings of the 5$^{th}$ Symposium on Logic in Computer Science},
	key = {LICS90},
	month = Jun,
	pages = {95--197},
	publisher = {IEEE Computer Society Press},
	title = {The Semantics of Reflected Proof},
	year = 1990,
}

ACHH93

@string{LNCS = "Lecture Notes in Computer Science"}
@inproceedings{ACHH93,
	author = {Alur, R. and C. Courcoubetis and Thomas A. Henzinger and Pei-Hsin Ho},
	booktitle = {Proceedings of Hybrid Systems Workshop},
	pages = {209--229},
	publisher = {Springer-Verlag},
	series = LNCS,
	title = {Hybrid Automata:  An Algorithmic Approach to the Specification and Verification of Hybrid Systems},
	volume = 736,
	year = 1993,
}

ACHH94

@inproceedings{ACHH94,
	crossref = {ACHH93},
}

Fully expanded entry:

@string{LNCS = "Lecture Notes in Computer Science"}
@inproceedings{ACHH94,
	author = {Alur, R. and C. Courcoubetis and Thomas A. Henzinger and Pei-Hsin Ho},
	booktitle = {Proceedings of Hybrid Systems Workshop},
	pages = {209--229},
	publisher = {Springer-Verlag},
	series = LNCS,
	title = {Hybrid Automata:  An Algorithmic Approach to the Specification and Verification of Hybrid Systems},
	volume = 736,
	year = 1993,
}

ACKP94

@string{May = "May"}
@unpublished{ACKP94,
	author = {Anderson, J. R. and A. T. Corbett and K. R. Koedinger and R. Pelletier},
	month = May,
	note = {Manuscript},
	title = {Cognitive Tutors: Lessons Learned},
	year = 1994,
}

ACL06

@article{ACL06,
	author = {Allen, Stuart F. and Constable, Robert L. and Lorigo, Lori},
	journal = {Journal of Electronic Publishing},
	note = {To appear in January},
	title = {Using Formal Reference to Enhance Authority and Integrity in Online Mathematical Texts},
	year = 2006,
}

ACL2-URL

@unpublished{ACL2-URL,
	author = {Matt Kaufmann and J Strother Moore},
	note = {\url{http://www.cs.utexas.edu/users/moore/acl2/}},
	title = {{\ACLt} Home Page},
}

ACM02

@inproceedings{ACM02,
	author = {Simon Ambler and Roy L. Crole and Alberto Momigliano},
	crossref = {tphols2002},
	pages = {13--30},
	title = {Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction},
}

Fully expanded entry:

@string{LNCS = "Lecture Notes in Computer Science"}
@inproceedings{ACM02,
	author = {Simon Ambler and Roy L. Crole and Alberto Momigliano},
	booktitle = {Proceedings of the 15$^{th}$ International Conference on Theorem Proving in Higher Order Logics ({TPHOLs} 2002)},
	editor = {Victor A. Carre{\~n}o and C{\'e}zar A. Mu{\~n}oz and Sophi{\`e}ne Tahar},
	isbn = {3-540-44039-9},
	key = {TPHOLs02},
	pages = {13--30},
	publisher = {Springer-Verlag},
	series = LNCS,
	title = {Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction},
	volume = 2410,
	year = 2002,
}

ACM03

@inproceedings{ACM03,
	author = {S. J. Ambler and R. L. Crole and Alberto Momigliano},
	crossref = {Merlin03},
	doi = {http://doi.acm.org/10.1145/976571.976572},
	pages = {1--11},
	title = {A Definitional Approach to Primitive Recursion over Higher Order Abstract Syntax},
}

Fully expanded entry:

@inproceedings{ACM03,
	author = {S. J. Ambler and R. L. Crole and Alberto Momigliano},
	booktitle = {Proceedings of the 2003 workshop on {M}echanized reasoning about languages with variable binding},
	doi = {http://doi.acm.org/10.1145/976571.976572},
	isbn = {1-58113-800-8/03/0008},
	key = {Merlin03},
	location = {Uppsala, Sweden},
	pages = {1--11},
	publisher = {{ACM} Press},
	title = {A Definitional Approach to Primitive Recursion over Higher Order Abstract Syntax},
	year = 2003,
}

ACM:1973:CRF

@proceedings{ACM:1973:CRF,
	address = "New York, NY, USA",
	bibdate = "Thu Dec 3 07:11:18 MST 1998",
	booktitle = "Conference record of Fifth Annual {ACM} Symposium on                  Theory of Computing: papers presented at the Symposium,                  Austin, Texas, April 30--May 2, 1973",
	editor = "{ACM}",
	keywords = "electronic digital computers --- programming ---                  congresses; computational complexity --- congresses;                  machine theory --- congresses",
	lccn = "QA76.6 .A16 1973",
	pages = "iv + 277",
	publisher = "{ACM} Press",
	title = "Conference record of Fifth Annual {ACM} Symposium on                  Theory of Computing: papers presented at the Symposium,                  Austin, Texas, April 30--May 2, 1973",
	year = 1973,
}

ACN90

@inproceedings{ACN90,
	address = {Sophia-Antipolis, France},
	author = {Augustsson, Lennart and Thierry Coquand and Bengt Nordstr{\"o}m},
	booktitle = {Proceedings of the First Annual Workshop on Logical Frameworks},
	pages = {39--42},
	title = {A Short Description of Another Logical Framework},
	year = 1990,
}

ACR98

@string{Oct = "October"}
@inproceedings{ACR98,
	address = {Vancouver},
	author = {Isabelle Attalli and Denise Caromel and Marjorie Russo},
	booktitle = {OOPSLA'98 Workshop on the Formal Underpinnings of Java},
	month = Oct,
	title = {A Formal Executable Semantics for Java},
	year = 1998,
}

ACT01

@inproceedings{ACT01,
	author = {D. A. Agarwal and O. Chevassut and M. R. Thompson and G. Tsudik},
	booktitle = {Proceedings of the 6th IEEE Symposium on Computers and Communications, Hammamet, Tunisia, July 3--5},
	pages = {22--28},
	title = {An Integrated Solution for Secure Group Communication in Wide-Area Networks},
	year = 2001,
}

ACU93

@string{JAR = "Journal of Automated Reasoning"}
@article{ACU93,
	author = {Aitken, William and Robert L. Constable and Judith Underwood},
	journal = JAR,
	number = 2,
	pages = {171--221},
	title = {Metalogical {F}rameworks {II}: Using Reflected Decision Procedures},
	volume = 22,
	year = 1993,
}

ACV96

@inproceedings{ACV96,
	address = {St. Petersburg, FL},
	author = {Abadi, Mart{\'i}n and Luca Cardelli and Ramesh Viswanathan},
	booktitle = {Proceedings of the 23rd Annual Symposium on Principles of Programming Languages},
	pages = {296--409},
	title = {An Interpretation of Objects and Object Types},
	year = 1996,
}

Acz00

@techreport{Acz00,
	author = "Peter Aczel and Michael Rathjen",
	institution = "Mittag-Leffler",
	number = 40,
	title = "Notes on Constructive Set Theory",
	year = 2000/2001,
}

Acz77

@inproceedings{Acz77,
	author = {Aczel, Peter},
	booktitle = {Handbook of Mathematical Logic},
	editor = {J. Barwise},
	pages = {739--782},
	publisher = {North-Holland},
	title = {An Introduction to Inductive Definitions},
	year = 1977,
}

Acz78

@inproceedings{Acz78,
	author = {Aczel, Peter},
	booktitle = {Logic Colloquium '77},
	editor = {MacIntyre, A. and L. Pacholski and J. Paris},
	publisher = {North Holland},
	title = {The type theoretic interpretation of constructive set theory},
	year = 1978,
}

Acz80

@incollection{Acz80,
	author = {Aczel, Peter},
	booktitle = {The Kleene Symposium},
	editor = {J. Barwise and H. Keisler and K. Kunen},
	pages = {31--59},
	publisher = {North Holland},
	title = {Frege Structures and the Notion of Proposition, Truth and Set},
	year = 1980,
}

Acz82

@inproceedings{Acz82,
	author = {Aczel, Peter},
	booktitle = {The L.E.J. Brouwer Centenary Symposium},
	editor = {Troelstra, S.S. and D. van Dalen},
	publisher = {North Holland},
	title = {The type theoretic interpretation of constructive set theory: Choice principles},
	year = 1982,
}

Acz86

@inproceedings{Acz86,
	author = {Aczel, Peter},
	booktitle = {Logic, Methodology and Philosophy of Science {VII}},
	pages = {17--49},
	publisher = {Elsevier Science Publishers},
	title = {The Type Theoretic Interpretation of Constructive Set Theory: Inductive Definition},
	year = 1986,
}

Acz97

@string{may = "May"}
@misc{Acz97,
	author = "Aczel, Peter",
	month = may,
	note = "Unpublished manuscript",
	title = "Notes on Constructive Type Theory",
	year = 1997,
}

Acz99

@inproceedings{Acz99,
	author = {Aczel, Peter},
	booktitle = {Proceedings of Types for Proofs and Programs},
	crossref = {Marktoberdorf97},
	pages = {57--97},
	title = {Notes on the Simply Typed Lambda Calculus},
}

Fully expanded entry:

@inproceedings{Acz99,
	address = {Berlin},
	author = {Aczel, Peter},
	booktitle = {Proceedings of Types for Proofs and Programs},
	editor = {Ulrich Berger and H. Schwichtenberg},
	pages = {57--97},
	publisher = {Springer},
	series = {Series {F}: Computer and Systems Sciences},
	title = {Notes on the Simply Typed Lambda Calculus},
	volume = 165,
	year = 1999,
}

Acz99a

@inproceedings{Acz99a,
	author = {Aczel, Peter},
	crossref = {TYPES98},
	pages = {1--18},
	title = {On relating type theories and set theories},
	url = {http://www.springerlink.com/link.asp?id=jkt3tlf6kdh8la8b},
}

Fully expanded entry:

@string{LNCS = "Lecture Notes in Computer Science"}
@inproceedings{Acz99a,
	author = {Aczel, Peter},
	booktitle = "Types for Proofs and Programs: International Workshop, TYPES '98, Kloster Irsee, Germany, March 1998",
	editor = "T. Altenkirch and W. Naraschewski and B. Reus",
	key = "TYPES98",
	pages = {1--18},
	series = LNCS,
	title = {On relating type theories and set theories},
	url = {http://www.springerlink.com/link.asp?id=jkt3tlf6kdh8la8b},
	volume = 1657,
	year = 1999,
}

AD96

@incollection{AD96,
	author = "R. Alur and D. L. Dill",
	booktitle = "Formal Methods for RealTime Computing",
	editor = "C. Heitmeyer and D. Mandrioli",
	pages = {55--82},
	publisher = {Wiley},
	title = "Automata-theoretic verification of real-time systems",
	year = 1996,
}

ADG+01

@inproceedings{ADG+01,
	author = {Andrew Adams and Martin Dunstan and Hanne Gottliebsen and Tom Kelsey and Ursula Martin and Sam Owre},
	crossref = {tphols2001},
	pages = {27--42},
	title = {Computer Algebra Meets Automated Theorem Proving: {I}ntegrating {\Maple} and {\PVS}},
}

Fully expanded entry:

@string{LNCS = "Lecture Notes in Computer Science"}
@string{Sep = "September"}
@inproceedings{ADG+01,
	address = {Edinburgh, Scotland},
	author = {Andrew Adams and Martin Dunstan and Hanne Gottliebsen and Tom Kelsey and Ursula Martin and Sam Owre},
	booktitle = {14$^{th}$ International Conference on Theorem Proving in Higher Order Logics},
	editor = {Richard Boulton and Paul Jackson},
	key = {TPHOLs01},
	month = Sep,
	pages = {27--42},
	publisher = {Springer-Verlag},
	series = LNCS,
	title = {Computer Algebra Meets Automated Theorem Proving: {I}ntegrating {\Maple} and {\PVS}},
	volume = 2152,
	year = 2001,
}

ADHK01

@string{TCS = "Journal of Theoretical Computer Science"}
@article{ADHK01,
	author = {Uri Abraham and Shlomi Dolev and Ted Herman and Irit Koll},
	journal = TCS,
	pages = {653--692},
	title = {Self-stabilizing $\ell$-exclusion},
	volume = 266,
	year = 2001,
}

ADKM92

@string{Jul = "July"}
@conference{ADKM92,
	author = {Y.~Amir and D.~Dolev and S.~Kramer and D.~Malki},
	booktitle = {22nd Annual International Symposium on Fault-Tolerant Computing},
	month = Jul,
	pages = {76--84},
	title = {Transis: A Communication Sub-System for High Availability},
	year = 1992,
}

ADKM92b

@string{LNCS = "Lecture Notes in Computer Science"}
@string{Nov = "November"}
@inproceedings{ADKM92b,
	author = {Y.~Amir and D.~Dolev and S.~Kramer and D.~Malki},
	booktitle = {Sixth International Workshop on Distributed Algorithms proceedings (WDAG-6)},
	month = Nov,
	pages = {292--312},
	series = LNCS,
	title = {Membership Algorithms for Multicast Communication Groups},
	volume = 647,
	year = 1992,
}

ADN97

@techreport{ADN97,
	author = {Sergei Artemov and J.M. Davoren and Anil Nerode},
	institution = {Cornell University},
	number = {MSI 97-05},
	title = {Modal logics and topological semantics for Hybrid Systems},
	year = 1997,
}

AFH94

@string{LNCS = "Lecture Notes in Computer Science"}
@inproceedings{AFH94,
	author = {R. Alur and L. Fix and T. A. Henzinger},
	booktitle = {Proc. 6th Int. Conf. Computer Aided Verification (CAV'94)},
	pages = {11--13},
	publisher = {Springer-Verlag},
	series = LNCS,
	title = {Event-Clock Automata: a Determinizable Class of Timed Automata},
	volume = 818,
	year = 1994,
}

AFST94

@string{May = "May"}
@unpublished{AFST94,
	author = {Alvisi, Lorenzo and Alan Fekete and Scott Stoller and Sam Toueg},
	month = May,
	note = {Draft.},
	title = {What is a group membership service?},
	year = 1994,
}

AFY93

@incollection{AFY93,
	author = {Archer, M. and G. Fink and L. Yang},
	booktitle = {Higher Order Logic Theorem Proving and Its Applications},
	editor = {Claesen, L. J. M. and M. J. C. Gordon},
	pages = {539--549},
	publisher = {Elsevier Science Publishers B. V. (North-Holland)},
	title = {Linking Other Theorem Provers to {\HOL} Using {PM}: Proof Manager},
	year = 1993,
}

AGH02

@inproceedings{AGH02,
	author = {Brian Aydemir and Adam Granicz and Jason Hickey},
	crossref = {tphols2002b},
	optwwwps = {papers/tphols02.ps},
	pages = {12--22},
	title = {Formal Design Environments},
}

Fully expanded entry:

@inproceedings{AGH02,
	author = {Brian Aydemir and Adam Granicz and Jason Hickey},
	booktitle = {Theorem Proving in Higher Order Logics; Track B Proceedings of the 15$^{th}$ International Conference on Theorem Proving in Higher Order Logics ({TPHOLs} 2002), Hampton, VA, August 2002},
	editor = {Victor A. Carre{\~n}o and C{\'e}zar A. Mu{\~n}oz and Sophi{\`e}ne Tahar},
	optwwwps = {papers/tphols02.ps},
	pages = {12--22},
	publisher = {National Aeronautics and Space Administration},
	title = {Formal Design Environments},
	year = 2002,
}

AGLM99

@inproceedings{AGLM99,
	address = "Vancouver, British Columbia, Canada",
	author = "Andrew A. Adams and Hanne Gottliebsen and Steve Linton and Ursula Martin",
	booktitle = "Proceedings of International Symposium on Symbolic and Algebraic Computation {(ISSAC'99)}",
	pages = "253--260",
	publisher = "{ACM}",
	title = "Automated Theorem Proving in Support of Computer Algebra: Symbolic Definite Integration as a Case Study",
	year = 1999,
}

AGOM04

@string{LNCS = "Lecture Notes in Computer Science"}
@inproceedings{AGOM04,
	author = {S. Abramsky and D. Ghica and L. Ong and A. Murawski},
	booktitle = {TACAS 2004: Tools and Algorithms for the Construction and Analysis of Systems, 10 International Conference},
	pages = {421--435},
	publisher = {Springer},
	series = LNCS,
	title = {Applying Game Semantics to Compositional Software Modelling and Verification},
	volume = 2988,
	year = 2004,
}

AH01a

@inproceedings{AH01a,
	author = {Luca de Alfaro and Thomas A. Henzinger},
	booktitle = {Proceedings of the Ninth Annual Symposium on Foundations of Software Engineering},
	organization = {{ACM} Press},
	title = {Interface Automata},
	year = 2001,
}

AH01b

@string{LNCS = "Lecture Notes in Computer Science"}
@inproceedings{AH01b,
	author = {Luca de Alfaro and Thomas A. Henzinger},
	booktitle = {Proceedings of the First International Workshop on Embedded Software(EMSOFT)},
	pages = {148--165},
	publisher = {Springer-Verlag},
	series = LNCS,
	title = {Interface Theories for Component-Based Design},
	volume = 2211,
	year = 2001,
}

AH76

@article{AH76,
	author = {Appel, K. I. and W. Haken},
	journal = {Bulletin of the American Mathematical Society},
	pages = {711--712},
	title = {Every Planar Map is Four Colorable},
	volume = 82,
	year = 1976,
}

AH97

@techreport{AH97,
	address = {Washington, DC 20375},
	author = {Archer, Myla and Constance Heitmeyer},
	institution = {Naval Research Laboratory},
	month = {May 19,},
	note = {A shorter version of this report was presented at RTAS '96, Boston, MA, June 10--13, 1996},
	title = {Mechanical Verification of Timed Automata: A Case Study},
	year = 1997,
}

AHH93

@inproceedings{AHH93,
	author = {Alur, R. and Thomas A.~Henzinger and Pei-Hsin Ho},
	booktitle = {IEEE Trans. on Software Engineering},
	note = {preliminary version appeared in Proc. 14th RTSS, 1993},
	pages = {181--201},
	title = {Automatic Symbolic Verification of Embedded Systems},
	volume = {22(3)},
	year = 1996,
}

AHR02

@article{AHR02,
	author = {Myla Archer and Constance Heitmeyer and Elvinia Riccobene},
	journal = {Automated Software Engineering},
	number = 3,
	pages = {201--232},
	publisher = {Kluwer Academic Publishers},
	title = {Proving Invariants of {I/O} Automata with {\TAME}},
	volume = 9,
	year = 2002,
}

AHS98

@string{Jul = "July"}
@inproceedings{AHS98,
	address = {Eindhoven, The Netherlands},
	author = {Archer, Myla and Constance Heitmeyer and Steve Sims},
	booktitle = {User Interfaces for Theorem Provers},
	month = Jul,
	note = {Informal proceedings available at \url{http://www.win.tue.nl/cs/ipa/uitp/proceedings.html}},
	title = {{\TAME}: {A} {\PVS} Interface to Simplify Proofs for Automata},
	year = 1998,
}

AHU74

@book{AHU74,
	author = {Aho, A. V. and J. E. Hopcroft and J. D. Ullman},
	publisher = {Addison-Wesley, Reading, MA},
	title = {The Design and Analysis of Computer Algorithms},
	year = 1974,
}

Ait93

@unpublished{Ait93,
	author = {Aitken, William},
	note = {Computer Science Department, Cornell University, Ithaca, NY},
	title = {A Formal Introduction to the Lambda Calculus},
	year = 1993,
}

Ait94

@phdthesis{Ait94,
	author = {Aitken, William},
	school = {Computer Science Department, Cornell University, Ithaca, NY},
	title = {Metaprogramming in {\Nuprl} Using Reflection},
	year = 1994,
}

AK94

@string{LNCS = "Lecture Notes in Computer Science"}
@inproceedings{AK94,
	author = {Sergei Artemov and Vladimir N. Krupski},
	booktitle = {Proceedings of the 3$^{rd}$ International Symposium on Logical Foundations of Computer Science},
	pages = {23--33},
	publisher = {Springer-Verlag},
	series = LNCS,
	title = {Referential data structures and labeled modal logic},
	volume = 813,
	year = 1994,
}

AK96

@string{APAL = "Annals of Pure and Applied Logic"}
@article{AK96,
	author = {Sergei Artemov and Vladimir N. Krupski},
	journal = APAL,
	pages = {57--71},
	title = {Data storage interpretation of labeled modal logic},
	volume = 78,
	year = 1996,
}

AL03

@string{LNCS = "Lecture Notes in Computer Science"}
@incollection{AL03,
	author = {Abadi, Martin and Rustan M. Leino},
	booktitle = {Verification: Theory and Practice, Essay dedicated to Zohar Manna on the occasion of his 64th birthday},
	editor = {Dershowitz, Nachum},
	pages = {11--41},
	publisher = {Springer},
	series = LNCS,
	title = {A logic of object-oriented programs},
	year = 2003,
}

AL90

@string{Apr = "April"}
@article{AL90,
	author = {Attiya, Hagit and Nancy A. Lynch},
	journal = {Information and Computation},
	month = Apr,
	number = 1,
	pages = {183--232},
	title = {Time Bounds for Real-Time Process Control in the Presence of Timing Uncertainty},
	volume = 110,
	year = 1994,
}

AL92

@string{Jun = "June"}
@inproceedings{AL92,
	author = {Aagaard, Mark and Miriam Leeser},
	booktitle = {Proceedings of Workshop on Computer-Aided Verification},
	editor = {Gregor Bochmann and David Probst},
	month = Jun,
	pages = {72--83},
	publisher = {Springer-Verlag},
	title = {Verifying a Logic Synthesis Tool in {\Nuprl}},
	year = 1992,
}

AL93

@string{Jun = "June"}
@techreport{AL93,
	address = {School of Electrical Engineering},
	author = {Aagaard, Mark and Miriam Leeser},
	institution = {Cornell University},
	month = Jun,
	number = {TR EE-CEG-93-5},
	title = {A Framework for Specifying and Designing Pipelines},
	year = 1993,
}

AL94

@string{LNCS = "Lecture Notes in Computer Science"}
@inproceedings{AL94,
	author = {Mark Aagaard and Miriam Leeser},
	booktitle = {1994 International Conference on Theorem Provers in Circuit Design},
	editor = {T. Kropf and R. Kumar},
	pages = {13--32},
	publisher = {Springer Verlag},
	series = LNCS,
	title = {Reasoning About Pipelines with Structural Hazards},
	volume = 901,
	year = 1995,
}

AL95

@string{May = "May"}
@string{TOPLAS = "{ACM} Transactions of Programming Language Systems"}
@article{AL95,
	author = {Abadi, Martin and Lamport, Leslie},
	journal = TOPLAS,
	month = May,
	number = 3,
	title = {Conjoining Specifications},
	volume = 17,
	year = 1995,
}

alfaweb

@misc{alfaweb,
	author = "Thomas Hallgren",
	note = "Alfaweb homepage: \url{http://www.cs.chalmers.se/~hallgren/Alfa/}",
	title = "Alfaweb",
}

All02

@techreport{All02,
	address = {Ithaca, New York},
	author = {Allen, Stuart F.},
	institution = {Cornell University},
	number = {TR2002-1885},
	title = {Abstract Identifiers and Textual Reference},
	year = 2002,
}

All02a

@misc{All02a,
	author = {Stuart Allen},
	howpublished = {\url{http://www.nuprl.org/FDLProject/FDLnotes/}},
	title = {Notes on the Design and Purpose of the {FDL}},
	year = {Ongoing, beginning 2002},
}

All03

@unpublished{All03,
	author = {Allen, Stuart F. and Robert Constable and Matthew Fluet},
	note = {To be published},
	title = {Expressing and Implementing the Computational Content Implicit in Smullyan's Account of Boolean Valuations},
	year = 2003,
}

All04

@article{All04,
	author = {Allen, Stuart},
	journal = {First Monday},
	note = {\url{http://www.firstmonday.org/issues/issue9_2/allen/index.html}},
	number = 2,
	title = {Abstract Identifiers, Intertextual Reference and a Computational Basis for Recordkeeping},
	volume = 9,
	year = 2004,
}

All84

@string{Jul = "July"}
@article{All84,
	author = {James F. Allen},
	journal = {Artificial Intelligence},
	month = Jul,
	number = 2,
	pages = {123--154},
	title = {Towards a general theory of action and time},
	volume = 23,
	year = 1984,
}

All87a

@inproceedings{All87a,
	author = {Allen, Stuart F.},
	crossref = {LICS87},
	pages = {215--224},
	title = {A {N}on-Type-Theoretic {D}efinition of {M}artin-{L}{\"{o}}f's {T}ypes},
}

Fully expanded entry:

@string{Jun = "June"}
@inproceedings{All87a,
	author = {Allen, Stuart F.},
	booktitle = {Proceedings of the 2$^{nd}$ IEEE Symposium on Logic in Computer Science},
	editor = {D. Gries},
	key = {LICS87},
	month = Jun,
	pages = {215--224},
	publisher = {IEEE Computer Society Press},
	title = {A {N}on-Type-Theoretic {D}efinition of {M}artin-{L}{\"{o}}f's {T}ypes},
	year = 1987,
}

All87b

@phdthesis{All87b,
	author = {Allen, Stuart F.},
	school = {Cornell University},
	title = {A Non-Type-Theoretic Semantics for Type-Theoretic Language},
	year = 1987,
}

All92

@unpublished{All92,
	author = {Allen, Stuart F.},
	note = {Unpublished note, Computer Science Department, Cornell University},
	title = {A Definition of the {P}olya Transform in {\Nuprl}},
	year = 1992,
}

All93

@unpublished{All93,
	author = {Stuart F.~Allen},
	note = {section of {\Nuprl} 4.2 library},
	title = {An imperative language in {\Nuprl}},
	year = 1995,
}

All98

@inproceedings{All98,
	address = {Eindhoven, The Netherlands},
	author = {Allen, Stuart F.},
	booktitle = {Proceedings of the Conference on User Interfaces for Theorem Provers},
	title = {From dy/dx to [ ]P: a matter of notation},
	year = 1998,
}

Alt93

@string{Nov = "November"}
@phdthesis{Alt93,
	address = {Department of Computer Science, The King's Blgs, Mayfield Rd, Edinburgh EH9 3JZ},
	author = {Thorsten Altenkirch},
	month = Nov,
	school = {University of Edinburgh},
	title = {Constructions, Inductive Types and Strong Normalization},
	year = 1993,
}

Alt93a

@string{LNCS = "Lecture Notes in Computer Science"}
@incollection{Alt93a,
	author = {Thorsten Altenkirch},
	booktitle = {Typed Lambda Claculi and Applications},
	editor = {J. F. Groote M. Benzen},
	publisher = {Springer-Verlag},
	series = LNCS,
	title = {A formalization of the strong normalization proof for System F in LEGO},
	volume = 664,
	year = 1993,
}

ALW89

@inproceedings{ALW89,
	author = {M. Abadi and  L. Lamport and P. Wolper},
	booktitle = {Proceedings of Sixteenth International Colloquium on Automata Languages and Programming},
	pages = {1--17},
	publisher = {Springer-Verlag},
	title = {Realizable and Unrealizable Concurrent Program Specifications},
	volume = 372,
	year = 1989,
}

ALW93

@inproceedings{ALW93,
	author = {Aagaard, Mark D. and Miriam E. Leeser and Phillip J. Windley},
	booktitle = {{\HOL} Theorem Proving System and its Applications},
	editor = {Jeffrey J. Joyce and Carl-Johan H. Seger},
	pages = {400--413},
	publisher = {Springer-Verlag},
	title = {Towards a Super Duper Hardware Tactic},
	year = 1993,
}

AMMAC93

@string{May = "May"}
@article{AMMAC93,
	author = {Y.~Amir and L.~E.~Moser and P.~M.~Melliar-Smith and D.~A.~Agarwal and P.~Ciarfella},
	journal = {International Conference on Distributed Computing Systems},
	month = May,
	pages = {551--560},
	title = {Fast Message Ordering and Membership Using a Logical Token-Passing Ring},
	year = 1993,
}

AMPR01

@inproceedings{AMPR01,
	author = {Natasha Alechina and Michael Mendler and Valeria de Paiva and Eike Ritter},
	crossref = {CSL01},
	pages = {292--307},
	title = {Categorical and {Kripke} Semantics for Constructive {S4} Modal Logic},
}

Fully expanded entry:

@string{LNCS = "Lecture Notes in Computer Science"}
@inproceedings{AMPR01,
	author = {Natasha Alechina and Michael Mendler and Valeria de Paiva and Eike Ritter},
	booktitle = {Computer Science Logic, Proceedings of the 10$^{th}$ Annual Conference of the EACSL},
	editor = {L. Fribourg},
	pages = {292--307},
	publisher = {Springer-Verlag},
	series = LNCS,
	title = {Categorical and {Kripke} Semantics for Constructive {S4} Modal Logic},
	url = {http://link.springer-ny.com/link/service/series/0558/tocs/t2142.htm},
	volume = 2142,
	year = 2001,
}

AN94

@string{Jun = "June"}
@techreport{AN94,
	address = {Palo Alto, CA},
	author = {Martin Abadi and Roger Needham},
	institution = {Digital Equipment Corporation},
	month = Jun,
	number = 125,
	title = {Prudent Engineering Practice for Cryptographic Protocols},
	type = {SRC Research Report},
	year = 1994,
}

And86

@book{And86,
	author = {Andrews, Peter B.},
	publisher = {Academic Press, Inc., New York},
	title = {An Introduction to Mathematical Logic and Type Theory:  to Truth through Proof},
	year = 1986,
}

And99

@book{And99,
	address = {New York},
	author = {Andrews, Gregory R.},
	publisher = {Addison Wesley},
	title = {Foundation of Multithreaded, Parallel, and Distributed Programming},
	year = 1999,
}

AO97

@book{AO97,
	author = {Apt, K. and E.-R. Oderog},
	publisher = {Springer},
	title = {Verification of Sequential and Concurrent Programs},
	year = 1997,
}

APC94

@inproceedings{APC94,
	author = {Abadi, Martin and G. Plotkin and Luca Cardelli},
	crossref = {LICS94},
	pages = {310--319},
	title = {Subtyping and Parametricity},
}

Fully expanded entry:

@string{Jul = "July"}
@inproceedings{APC94,
	address = {Paris, France},
	author = {Abadi, Martin and G. Plotkin and Luca Cardelli},
	booktitle = {Proceedings of 9$^{th}$ IEEE Symposium on Logic in Computer Science},
	key = {LICS94},
	month = Jul,
	pages = {310--319},
	publisher = {IEEE Computer Society Press},
	title = {Subtyping and Parametricity},
	year = 1994,
}

APCFS03

@article{APCFS03,
	author = {A. Asperti and L. Padovani and C. Sacerdoti Coen and G. Ferruccio and I. Schena},
	journal = {Annals of Mathematics and Artificial Intelligence, Special Issue on Mathematical Knowledge Management},
	number = {1--3},
	pages = {27--46},
	title = {Mathematical Knowledge Management in {HELM}},
	volume = 38,
	year = 2003,
}

Apo57

@book{Apo57,
	author = {Apostol, Tom M.},
	publisher = {Addison-Wesley Publishing Company, Inc.},
	series = {Addison-Wesley Series in Mathematics},
	title = {Mathematical Analysis: A Modern Approach to Advanced Calculus},
	year = 1957,
}

App01

@inproceedings{App01,
	author = "Andrew W. Appel",
	crossref = "LICS01",
	pages = "247--258",
	title = "Foundational Proof-Carrying Code",
	url = citeseer.ist.psu.edu/appel01foundational.html,
}

Fully expanded entry:

@inproceedings{App01,
	author = "Andrew W. Appel",
	booktitle = {Proceedings of 16$^{th}$ IEEE Symposium on Logic in Computer Science},
	key = {LICS01},
	pages = "247--258",
	publisher = "IEEE Computer Society Press",
	title = "Foundational Proof-Carrying Code",
	url = citeseer.ist.psu.edu/appel01foundational.html,
	year = 2001,
}

App92

@book{App92,
	author = {Appel, Andrew W.},
	publisher = {Cambridge University Press},
	title = {Compiling with Continuations},
	year = 1992,
}

APSS01

@inproceedings{APSS01,
	author = {A. Asperti and L. Padovani and C. Sacerdoti Coen and I. Schena},
	crossref = {tphols2001},
	pages = {59--74},
	title = {{HELM} and the Semantic Math-Web},
}

Fully expanded entry:

@string{LNCS = "Lecture Notes in Computer Science"}
@string{Sep = "September"}
@inproceedings{APSS01,
	address = {Edinburgh, Scotland},
	author = {A. Asperti and L. Padovani and C. Sacerdoti Coen and I. Schena},
	booktitle = {14$^{th}$ International Conference on Theorem Proving in Higher Order Logics},
	editor = {Richard Boulton and Paul Jackson},
	key = {TPHOLs01},
	month = Sep,
	pages = {59--74},
	publisher = {Springer-Verlag},
	series = LNCS,
	title = {{HELM} and the Semantic Math-Web},
	volume = 2152,
	year = 2001,
}

Apt81

@string{TOPLAS = "{ACM} Transactions of Programming Language Systems"}
@article{Apt81,
	author = {Apt, K.},
	journal = TOPLAS,
	number = 4,
	pages = {431--483},
	title = {Ten years of {H}oare's logic: a survey--part 1},
	volume = 3,
	year = 1981,
}

Arm00

@book{Arm00,
	address = {Cambridge, Massachusetts},
	author = {Arms, William Y.},
	publisher = {MIT Press},
	title = {Digital Libraries},
	year = 2000,
}

Arms00

@article{Arms00,
	author = "William Y. Arms",
	journal = "D-Lib Magazine",
	month = " July--August",
	note = "\url{http://www.dlib.org/dlib/july00/arms/07arms.html}",
	number = 7/8,
	title = "Automated Digital Libraries. {How} Effectively Can Computers Be Used for the Skilled Tasks of Professional Librarianship?",
	volume = 6,
	year = 2000,
}

Art00

@incollection{Art00,
	address = {Stanford University},
	author = "Sergei Artemov",
	booktitle = {Advances in Modal Logic},
	publisher = {CSLI Publications},
	title = "Operations on proofs that can be specified by means of modal logic",
	volume = 2,
	year = 2000,
}

Art01

@article{Art01,
	author = {Sergei Artemov},
	journal = {The Bulletin for Symbolic Logic},
	number = 1,
	pages = {1--36},
	title = {Explicit provability and constructive semantics},
	volume = 6,
	year = 2001,
}

Art02

@incollection{Art02,
	author = {Sergei Artemov},
	booktitle = {Algebras, Diagrams and Decisions in Language, Logic and Computation},
	editor = {Kees Vermeulen and Ann Copestake},
	pages = {89--117},
	publisher = {Stanford University},
	series = {CSLI Publications},
	title = {Unified semantics for modality and $\lambda$-terms via proof polynomials},
	year = 2002,
}

Art04

@string{Nov = "November"}
@techreport{Art04,
	author = {Sergei Artemov},
	institution = {CUNY Ph.D. Program in Computer Science Technical Reports},
	month = Nov,
	number = {TR-2004018},
	title = {Evidence-Based Common Knowledge},
	url = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=140},
	year = 2004,
}

Art82

@incollection{Art82,
	address = "Moscow",
	author = "Sergei Artemov",
	booktitle = "{Voprosy Kibernetiki: Nonclassical logics and application}",
	note = "(in Russian)",
	pages = {3--20},
	publisher = {Nauka},
	title = "Applications of modal logic in proof theory",
	year = 1982,
}

Art85

@article{Art85,
	author = "Sergei Artemov ",
	journal = {Soviet Mathematics Doklady},
	number = 2,
	pages = {403--405},
	title = "Non-arithmeticity of truth predicate logics of provability",
	volume = 32,
	year = 1985,
}

Art88

@string{Mar = "March"}
@article{Art88,
	author = {Artalejo, M. R.},
	journal = {Computerised Logic Teaching Bulletin},
	month = Mar,
	number = 1,
	pages = {48--50},
	title = {Computerised Logic Teaching with {M}izar},
	volume = 1,
	year = 1988,
}

Art90

@inproceedings{Art90,
	author = "Sergei Artemov ",
	booktitle = "Theoretical Aspects of Reasoning about Knowledge - {III Proceedings}",
	pages = {257--272},
	publisher = {Morgan Kaufman Pbl.},
	title = "Kolmogorov logic of problems and a provability interpretation of intuitionistic logic",
	year = 1990,
}

Art91

@string{LNCS = "Lecture Notes in Computer Science"}
@incollection{Art91,
	author = {Arthan, R. D.},
	booktitle = {VDM '91 Formal Software Development Methods},
	editor = {S. Prehn and W. J. Toctenel},
	pages = {356--370},
	publisher = {Springer-Verlag, NY},
	series = LNCS,
	title = {Formal Specification of a {P}roof {T}ool},
	volume = 551,
	year = 1991,
}

Art93

@string{LNCS = "Lecture Notes in Computer Science"}
@article{Art93,
	author = {S.~Artemov and T.~Strassen},
	journal = LNCS,
	note = {Springer Verlag},
	pages = {14--28},
	title = {The Basic Logic of Proofs},
	volume = 702,
	year = 1993,
}

Art94

@string{APAL = "Annals of Pure and Applied Logic"}
@article{Art94,
	author = "Sergei Artemov ",
	journal = APAL,
	number = 1,
	pages = {29--59},
	title = "Logic of Proofs",
	volume = 67,
	year = 1994,
}

Art95

@techreport{Art95,
	author = "Sergei Artemov ",
	institution = {Cornell University},
	number = {MSI 95-29},
	title = "Operational Modal Logic",
	year = 1995,
}

Art96

@techreport{Art96,
	author = {S.~Artemov},
	institution = {Cornell University, Computer Science Department},
	number = {MSI 96-06},
	title = {Proof realization of intuitionistic and modal logics},
	year = 1996,
}

Art97

@techreport{Art97,
	author = "Sergei Artemov ",
	institution = {Cornell University},
	number = {MSI 95-02},
	title = "Proof realizations of typed $\lambda$-calculi",
	year = 1997,
}

Art98a

@techreport{Art98a,
	author = "Sergei Artemov",
	institution = {Cornell University},
	number = {CFIS 98-06},
	title = "Logic of Proofs: a Unified Semantics for Modality and $\lambda$-terms",
	year = 1998,
}

Art98b

@incollection{Art98b,
	author = "Sergei Artemov",
	booktitle = {Logic, Language and Computation},
	publisher = {CSLI Publications, Stanford University},
	title = "Unified Semantics for Modality and $\lambda$-terms via Proof Polynomials",
	volume = 3,
	year = 1998,
}

Art99

@inproceedings{Art99,
	author = "Sergei Artemov",
	crossref = "CADE99",
	pages = {267--281},
	title = "On explicit reflection in theorem proving and formal verification",
}

Fully expanded entry:

@string{LNAI = "Lecture Notes in Artificial Intelligence"}
@inproceedings{Art99,
	address = {Berlin},
	author = "Sergei Artemov",
	booktitle = {Proceedings of the 16$^{th}$ International Conference on Automated Deduction},
	editor = {Harald Ganzinger},
	isbn = {3-540-66222-7},
	month = {July 7--10},
	pages = {267--281},
	publisher = {Trento, Italy},
	series = LNAI,
	title = "On explicit reflection in theorem proving and formal verification",
	volume = 1632,
	year = 1999,
}

Art99a

@techreport{Art99a,
	author = {S.~Artemov},
	institution = {Cornell University, Computer Science Department},
	note = {Proceedings of the Workshop Intuitionistic Modal Logic and Applications, Trento, Italy, 1999},
	title = {Deep isomorphism of modal derivations and lambda-terms},
	year = 1999,
}

Art99b

@article{Art99b,
	author = {Sergei Artemov},
	journal = {Electronic Notes on Theoretical Computer Science},
	note = {\url{http://www.elsevier.nl/entcs/}},
	number = 1,
	title = {Uniform Provability Realization of Intuitionistic Logic, Modality and Lambda-terms},
	volume = 23,
	year = 1999,
}

AS85

@book{AS85,
	author = {Abelson, H. and G. J. Sussman},
	publisher = {MIT Press, Cambridge, MA},
	title = {Structure and Interpretation of Computer Programs},
	year = 1985,
}

AS85a

@string{Oct = "October"}
@article{AS85a,
	author = "Bowen Alpern and Fred B. Schneider",
	day = 7,
	journal = "Information Processing Letters",
	month = Oct,
	number = 4,
	pages = "181--185",
	title = "Defining Liveness",
	volume = 21,
	year = 1985,
}

AS87

@article{AS87,
	author = {Bowen Alpern and Fred B. Schneider},
	journal = {Distributed Computing},
	pages = {117--126},
	title = {Recognizing Safety and Liveness},
	volume = 2,
	year = 1987,
}

AS89

@string{TOPLAS = "{ACM} Transactions of Programming Language Systems"}
@article{AS89,
	author = {Alpern, Bowen and Fred B.~Schneider},
	journal = TOPLAS,
	pages = {147--167},
	title = {Verifying Temporal Properties Without Temporal Logic},
	volume = 11,
	year = 1989,
}

AS93

@string{Aug = "August"}
@string{LNCS = "Lecture Notes in Computer Science"}
@inproceedings{AS93,
	author = {Sergei Artemov and Tyko Stra{\ss}en},
	booktitle = {Computational Logic and Proof Theory, Proceedings of the Third Kurt G{\"o}del Colloquium},
	editor = {Georg Gottlob and Alexander Leitsch and Daniele Mundici},
	month = Aug,
	pages = {71--82},
	publisher = {Springer},
	series = LNCS,
	title = {The logic of the {G\"o}del proof predicate},
	volume = 713,
	year = 1993,
}

Ash75

@unpublished{Ash75,
	author = {Ashcroft, E. A.},
	note = {Preprint},
	title = {Program Verification Tableaus},
	year = 1975,
}

Asp00

@string{LNCS = "Lecture Notes in Computer Science"}
@inproceedings{Asp00,
	author = {David Aspinall},
	booktitle = {Proceedings of TACAS},
	note = {\url{http://zermelo.dcs.ed.ac.uk/home/da/papers/pgoutline/}},
	series = LNCS,
	title = {Proof {G}eneral --- {A} Generic Tool for Proof Development},
	volume = 1785,
	year = 2000,
}

Asp95

@string{May = "May"}
@string{TCS = "Journal of Theoretical Computer Science"}
@article{Asp95,
	author = {Asperti, Andrea},
	journal = TCS,
	month = May,
	number = 2,
	pages = {277--297},
	title = {Paths, Computations and Labels in the $\lambda$-Calculus},
	volume = 142,
	year = 1995,
}

Asp96

@inproceedings{Asp96,
	author = {Asperti, Andrea},
	booktitle = {1996 {ACM} Symposium on Principles of Programming Languages},
	pages = {110--118},
	title = {On the Complexity of beta-Reduction},
	year = 1996,
}

AU92

@book{AU92,
	address = {New York},
	author = {Aho, A. V. and J. D. Ullman},
	publisher = {Computer Science Press},
	title = {Foundations of Computer Science},
	year = 1992,
}

Aud91

@inproceedings{Aud91,
	author = {Audebaud, P.},
	crossref = {LICS91},
	pages = {86--95},
	title = {Partial Objects in the Calculus of Constructions},
}

Fully expanded entry:

@string{Jul = "July"}
@inproceedings{Aud91,
	address = {Vrije University, Amsterdam, The Netherlands},
	author = {Audebaud, P.},
	booktitle = {Proceedings of the 6$^{th}$ Symposium on Logic in Computer Science},
	key = {LICS91},
	month = Jul,
	pages = {86--95},
	publisher = {IEEE Computer Society Press},
	title = {Partial Objects in the Calculus of Constructions},
	year = 1991,
}

Aug98

@inproceedings{Aug98,
	author = "Lennart Augustsson",
	booktitle = "International Conference on Functional Programming",
	pages = "239--250",
	title = "Cayenne --- a Language with Dependent Types",
	url = citeseer.nj.nec.com/augustsson98cayenne.html,
	year = 1998,
}

autoconf

@string{Nov = "November"}
@book{autoconf,
	author = "David MacKenzie and Ben Elliston and Akim Demaille",
	month = Nov,
	note = "\url{http://www.gnu.org/software/autoconf/manual/index.html}",
	publisher = "Free Software Foundation",
	title = "\textsf{Autoconf}: Creating Automatic Configuration Scripts",
	year = 2003,
}

automake

@string{Sep = "September"}
@book{automake,
	author = "David MacKenzie and Tom Tromey",
	month = Sep,
	note = "\url{http://www.gnu.org/software/automake/manual/index.html}",
	publisher = "Free Software Foundation",
	title = "{GNU} {Automake}",
	year = 2003,
}

AW04

@book{AW04,
	address = {New York},
	author = {Attiya, H. and Welch, J.},
	edition = {2nd},
	publisher = {Wiley Interscience},
	title = {Distributed Computing: Fundamentals, Simulations, and Advanced Topics},
	year = 2004,
}

AW80

@string{Jul = "July"}
@string{LNCS = "Lecture Notes in Computer Science"}
@inproceedings{AW80,
	author = {Aiello, L. and Weyhrauch, R. W.},
	booktitle = {Proceedings of 5th International Conference on Automated Deduction, {\rm Les Arcs, France}},
	editor = {W. Bibel and R. Kowalski},
	month = Jul,
	pages = {1--11},
	publisher = {Springer-Verlag},
	series = LNCS,
	title = {Using meta-theoretic reasoning to do algebra},
	volume = 87,
	year = 1980,
}

AW93

@inproceedings{AW93,
	author = {Aiken, Alexander and Edward L. Wimmers},
	booktitle = {Conference on Functional Programming Languages and Computer Architecture},
	pages = {31--41},
	title = {Type Inclusion Constraints and Type Inference},
	year = 1993,
}

Awe85

@string{Oct = "October"}
@article{Awe85,
	author = {Baruch Awerbuch},
	journal = {Journal of the Association of Computing Machinery},
	month = Oct,
	number = 4,
	pages = {804--823},
	title = {Complexity of Network Synchronization},
	volume = 32,
	year = 1985,
}

axiomweb

@misc{axiomweb,
	author = "Timothy Daly",
	key = "AXIOM",
	note = {\url{http://savannah.nongnu.org/projects/axiom}},
	title = {{\Axiom} Home Page},
}

B+88

@string{LNCS = "Lecture Notes in Computer Science"}
@book{B+88,
	author = {Bauer, F. L. and others},
	publisher = {Springer-Verlag, New York},
	series = LNCS,
	title = {The Munich Project CIP:  Volume {II}},
	volume = 292,
	year = 1988,
}

B-JBS03

@misc{B-JBS03,
	author = {Ben-Jacob, E and I. Becker and Y. Shapira and H. Levine},
	howpublished = {\emph{Draft article,} Tel Aviv University School of Physics and Astronomy},
	title = {Collective Intelligence in Bacterial Organization},
	year = 2003,
}

B-OCG93

@inproceedings{B-OCG93,
	author = {M.~Ben-Or and R.~Canetti and O.~Goldreich},
	booktitle = {Proceedings 25th STOC},
	pages = {52--61},
	title = {Asynchronous Secure Computations},
	year = 1993,
}

B-OGW88

@article{B-OGW88,
	author = {M.~Ben-Or and S.~Goldwasser and A.~Widgerson},
	journal = {20th STOC},
	pages = {1--10},
	title = {Completeness Theorems for Non-Cryptographic Fault-Tolerant Distributed Computation},
	year = 1988,
}

B-OKR94

@article{B-OKR94,
	author = {M.~Ben-Or and B.~Kelmer and T.~Rabin},
	journal = {PODC},
	title = {Asynchronous Secure Computations with Optimal Resilience},
	year = 1994,
}

B-TGS90

@inproceedings{B-TGS90,
	author = {Breazu-Tannen, Val and Carl A. Gunter and Andre Scedrov},
	booktitle = {{ACM} Conference on {Lisp} and Functional Programming},
	pages = {44--60},
	title = {Computing with Coercions},
	year = 1990,
}

BA02

@inproceedings{BA02,
	author = {Eli Barzilay and Stuart Allen},
	crossref = {tphols2002b},
	pages = {23--32},
	title = {Reflecting Higher-Order Abstract Syntax in {\Nuprl}},
}

Fully expanded entry:

@inproceedings{BA02,
	author = {Eli Barzilay and Stuart Allen},
	booktitle = {Theorem Proving in Higher Order Logics; Track B Proceedings of the 15$^{th}$ International Conference on Theorem Proving in Higher Order Logics ({TPHOLs} 2002), Hampton, VA, August 2002},
	editor = {Victor A. Carre{\~n}o and C{\'e}zar A. Mu{\~n}oz and Sophi{\`e}ne Tahar},
	pages = {23--32},
	publisher = {National Aeronautics and Space Administration},
	title = {Reflecting Higher-Order Abstract Syntax in {\Nuprl}},
	year = 2002,
}

BA98

@inproceedings{BA98,
	author = {Gustavo Betarte and Alvaro Tasistro},
	booktitle = {Twenty-Five Years of Constructive Type Theory},
	chapter = 2,
	pages = {21--39},
	publisher = {Oxford University Press},
	title = {Extension of {M}artin-{L}{\"o}f's Type Theory with Record Types and Subtyping},
	year = 1998,
}

BAA00

@misc{BAA00,
	author = {Office of Naval Research},
	howpublished = {As published in the Commerce Business Daily; see also \url{http://www.onr.navy.mil/02/baa/expired/00_015.htm}},
	month = {June 19},
	note = {Solicitation Number: BAA 00-015},
	title = {{Critical Infrastructure Protection and High Confidence, Adaptable Software (CIP/SW) Research Program of the University Research Initiative (URI) -- Topic \#8 Digital Libraries for Constructive Mathematical Knowledge}},
	year = 2000,
}

BAC03

@misc{BAC03,
	author = {Eli Barzilay and Stuart Allen and Robert Constable},
	howpublished = {Short paper presented at 18th Annual {IEEE} Symposium on Logic in Computer Science, June 22--25, Ottawa, Canada},
	title = {Practical Reflection in {\Nuprl}},
	year = 2003,
}

Bac78

@string{Aug = "August"}
@inproceedings{Bac78,
	author = {Backus, J. W.},
	booktitle = {A Functional Style and its Algebra of Programs, Comm. Assoc. Comput. Mach.},
	month = Aug,
	pages = {613--641},
	title = {Can Programming be Liberated from the {V}on {N}eumann Style?},
	year = 1978,
}

Bac84

@string{Nov = "November"}
@techreport{Bac84,
	author = "Backhouse, Roland",
	institution = "University of Essex",
	month = Nov,
	number = "CSM-70",
	title = "o}f's Theory of Types",
	year = 1984,
}

Bac87

@string{May = "May"}
@inproceedings{Bac87,
	author = "Backhouse, Roland",
	booktitle = "Workshop on General Logic, Edinburgh, February 1987",
	editor = A.~Avron,
	month = May,
	number = "88-52",
	publisher = "Department of Computer Science, University of Edinburgh",
	series = "ECS-LFCS",
	title = "o}f's Theory of Types",
	year = 1988,
}

Bac88

@article{Bac88,
	author = {Back, R.},
	journal = {Acta Informatica},
	pages = {593--624},
	title = {A calculus of refinements for program derivations},
	year = 1988,
}

Bac89

@incollection{Bac89,
	author = {Backhouse, R. C.},
	booktitle = {Constructive Methods in Computer Science, {\rm NATO ASI Series, Vol.~F55}:  Computer \& System Sciences},
	editor = {M. Broy},
	pages = {6--92},
	publisher = {Springer-Verlag, New York},
	title = {Constructive Type Theory--an introduction},
	year = 1989,
}

Bac90

@string{LNCS = "Lecture Notes in Computer Science"}
@incollection{Bac90,
	author = {Back, R. J. R.},
	booktitle = {Stepwise Refinement of Distributed Systems},
	editor = {de Bakker, J. W. and W.-P. de Roever and G. Rozenberg},
	publisher = {Springer-Verlag},
	series = LNCS,
	title = {Refinement calculus, part {II}: Parallel and reactive programs},
	volume = 430,
	year = 1990,
}

Bai98

@phdthesis{Bai98,
	author = {Bailey, Antony J.},
	school = {University of Manchester},
	title = {The Machine-Checked Literate Formalization of Algebra in Type Theory},
	year = 1998,
}

Bal99

@phdthesis{Bal99,
	author = "Clemens Ballarin",
	note = "Available as Cambrigde Computer Laboratory technical report number 473",
	school = "University of Cambridge",
	title = "Computer Algebra and Theorem Proving",
	url = citeseer.nj.nec.com/ballarin99computer.html,
	year = 1999,
}

Bana

@book{Bana,
	author = {Banachowski, L. and others},
	publisher = {Banach Center Publications, Warsaw},
	title = {An introduction to algorithmic logic},
	volume = 2,
	year = 1977,
}

Bar01

@string{Jan = "January"}
@techreport{Bar01,
	address = {Ithaca, New York},
	author = {Eli Barzilay},
	institution = {Cornell University},
	month = Jan,
	number = {TR2001-1832},
	title = "Quotation and Reflection in {\Nuprl} and {S}cheme",
	year = 2001,
}

Bar03

@string{Jun = "June"}
@misc{Bar03,
	author = {Eli Barzilay},
	howpublished = {Talk given at LICS 2003, Ottawa, Canada},
	month = Jun,
	title = {Practical Reflection in {\Nuprl}},
	url = {http://www.nuprl.org/FDLProject/talks.html},
	year = 2003,
}

Bar05

@phdthesis{Bar05,
	crossref = {Bar06},
}

Fully expanded entry:

@phdthesis{Bar05,
	author = {Barzilay, Eli},
	school = {Cornell University},
	title = {Implementing Reflection in {\Nuprl}},
	year = 2006,
}

Bar06

@phdthesis{Bar06,
	author = {Barzilay, Eli},
	school = {Cornell University},
	title = {Implementing Reflection in {\Nuprl}},
	year = 2006,
}

Bar77

@incollection{Bar77,
	author = {Barendregt, Henk P.},
	booktitle = {Handbook of Mathematical Logic},
	editor = {Jon Barwise},
	pages = {1091--1132},
	publisher = {North-Holland, NY},
	title = {The Typed lambda calculus},
	year = 1977,
}

Bar81

@book{Bar81,
	author = {Barendregt, Henk P.},
	publisher = {North-Holland, Amsterdam},
	series = {Studies in Logic},
	title = {The Lambda Calculus: Its Syntax and Symantics},
	volume = 103,
	year = 1981,
}

Bar91

@string{Apr = "April"}
@article{Bar91,
	author = {Henk P. Barendregt},
	journal = {Journal Functional Programming},
	month = Apr,
	number = 2,
	pages = {125--154},
	title = {Introduction to Generalised Type Systems},
	volume = 1,
	year = 1991,
}

Bar92

@inbook{Bar92,
	author = {Henk P. Barendregt},
	chapter = {Lambda Calculi with Types},
	pages = {118--310},
	publisher = {Oxford University Press},
	title = {Handbook of Logic in Computer Science},
	volume = 2,
	year = 1992,
}

Bar93

@article{Bar93,
	author = {J. P. Barlow},
	journal = {Communication of the {ACM}},
	number = 11,
	pages = {21--26},
	title = {A Plain Text on Crypto Policy},
	volume = 36,
	year = 1993,
}

Bar99

@book{Bar99,
	address = {London},
	author = {John D. Barrow},
	publisher = {Vintage},
	title = {Impossibility: {The} Limits of Science and the Science of Limits},
	year = 1999,
}

Bas88

@inproceedings{Bas88,
	author = {Basin, David A.},
	crossref = {CADE88},
	pages = {101--110},
	title = {An environment for automated reasoning about partial functions},
}

Fully expanded entry:

@string{LNCS = "Lecture Notes in Computer Science"}
@inproceedings{Bas88,
	author = {Basin, David A.},
	booktitle = {9th International Conference on Automated Deduction},
	editor = {E. Lusk and R. Overbeek},
	pages = {101--110},
	publisher = {Springer-Verlag, NY},
	series = LNCS,
	title = {An environment for automated reasoning about partial functions},
	volume = 310,
	year = 1988,
}

Bas89

@string{LNCS = "Lecture Notes in Computer Science"}
@inproceedings{Bas89,
	author = {Basin, David A.},
	booktitle = {Proceedings of Logic at Botik '89, {\rm Pereslavl-Zalesky, USSR}},
	note = {(Cornell TR 88-932)},
	pages = {12--25},
	publisher = {Springer-Verlag},
	series = LNCS,
	title = {{Building Theories in {\Nuprl}}},
	volume = 363,
	year = 1989,
}

Bas90

@phdthesis{Bas90,
	author = {Basin, David A.},
	school = {Cornell University},
	title = {{Building Problem Solving Environments in Constructive Type Theory}},
	year = 1990,
}

Bas91

@techreport{Bas91,
	author = {Basin, David A.},
	institution = {Department of Artificial Intelligence, Edinburgh},
	note = {Also appeared in Proceedings of the IFIP-IEEE Int'l. Workshop on Formal Methods in VLSI Design, Miami USA, 1991.},
	number = {Research Paper 533},
	title = {Extracting circuits from constructive proofs.},
	year = 1991,
}

Bas98

@phdthesis{Bas98,
	address = {Ithaca, NY, USA},
	author = {Anindya Basu},
	order_no = {UMI Order No. GAX98-04994},
	school = {Cornell University},
	title = {A language-based approach to protocol construction},
	year = 1998,
}

Bat83

@techreport{Bat83,
	author = {Batali, J.},
	institution = {MIT},
	number = {AIM-TR-701},
	title = {Computational Introspection},
	year = 1983,
}

Bates79

@phdthesis{Bates79,
	author = {Bates, J. L.},
	school = {Cornell University},
	title = {A Logic for Correct Program Development},
	year = 1979,
}

Bates81

@techreport{Bates81,
	author = {Bates, J. L.},
	institution = {Cornell University},
	note = {Revision of Cornell University Ph.D. thesis submitted August 1979},
	number = {TR81-455},
	title = {A Logic for Correct Program Development},
	year = 1981,
}

Bay97

@inproceedings{Bay97,
	author = {Bayardo Jr., R. J. and R. C. Schrag},
	booktitle = {Proceedings of AAAI-97},
	title = {Using {CSP} look-back techniques to solve real-world {SAT} instances},
	year = 1997,
}

BB85

@book{BB85,
	author = {Bishop, E. and D. Bridges},
	publisher = {Springer, New York},
	title = {{Constructive Analysis}},
	year = 1985,
}

BB90

@inproceedings{BB90,
	author = {G. Berry and G. Boudol},
	booktitle = {Conference Record of the 17th Annual {ACM} Symposium on Principles of Programming Languages},
	pages = {81--94},
	title = {The Chemical Abstract Machine},
	year = 1990,
}

BB94

@string{Apr = "April"}
@string{LNCS = "Lecture Notes in Computer Science"}
@inproceedings{BB94,
	address = {Sendai, Japan},
	author = {Franco Barbanera and Stefano Berardi},
	booktitle = {Theoretical Aspects of Computer Software},
	editor = {Masami Hagiya and John C.~Mitchell},
	month = Apr,
	organization = {TACS '94},
	pages = {495--515},
	publisher = {Springer-Verlag},
	series = LNCS,
	title = {A Symmetric Lambda Calculus for "Classical" Program Extraction},
	year = 1994,
}

BBCGM97

@string{Feb = "February"}
@manual{BBCGM97,
	address = {Sophia Antipolis},
	author = {Bertot, J. and Y. Bertot and Y. Coscoy and H. Goguen and F. Montagnac},
	month = Feb,
	note = {System Revision 1.22; Documentation Revision 1.31},
	organization = {INRIA},
	title = {User Guide to the CTCOQ Proof Environment},
	year = 1997,
}

BBD+81

@article{BBD+81,
	author = {Bauer, F. L. and M. Broy and W. Dosch and R. Gnatz and B. Krieg-Br{\"{u}}kner and A. Laut and M. Luckman and T. Matzner and B. M{\"{o}}ller and H. Partsch and  P. Pepper and K. Samelson and R. Steinbr{\"{u}}cken and M. Wirsing and H. W{\"{o}}ssner},
	journal = {Science of Computer Programming},
	pages = {73--114},
	title = {Programming in a wide spectrum language:  a collection of examples},
	volume = 1,
	year = 1981,
}

BBL91

@article{BBL91,
	author = {Basin, David A. and G. Brown and Miriam Leeser},
	journal = {Integration: The International Journal of  VLSI Design},
	pages = {235--250},
	title = {{F}ormally {V}erified {S}ynthesis of {C}ombinational {CMOS}, {C}ircuits},
	volume = 11,
	year = 1991,
}

BBMS00

@article{BBMS00,
	author = {Baumslag, Gilbert and Bridson, Martin R. and Miller, III, Charles F. and Short, Hamish},
	issn = {0010-2571},
	journal = {Commentarii Mathematici Helvetici},
	number = 3,
	pages = {457--477},
	title = {Fibre products, non-positive curvature, and decision problems},
	volume = 75,
	year = 2000,
}

BBP94

@article{BBP94,
	author = {Buss, S. and Bonet, M. and Pitassi, T.},
	journal = {Feasible Mathematics {II}, {B}irkhauser},
	pages = {31--56},
	title = {Are there hard examples for {F}rege systems?},
	year = 1995,
}

BBS98

@incollection{BBS98,
	author = {H. Benl and U. Berger and H. Schwichtenberg and others},
	booktitle = {Automated Deduction},
	editor = {W. Bibel and P. G. Schmitt},
	publisher = {Kluwer},
	title = {Proof Theory at Work: Program Development in the {Minlog} System},
	volume = {II},
	year = 1998,
}

BC01

@article{BC01,
	author = {Henk Barendregt and Arjeh M. Cohen},
	journal = {Journal of Symbolic Computation},
	pages = {3--22},
	title = {Electronic Communication of Mathematics and the Interaction of Computer Algebras Systems and Proof Assistants},
	volume = 32,
	year = 2001,
}

BC03

@techreport{BC03,
	author = {Mark Bickford and Robert L. Constable},
	institution = {Cornell University},
	number = {TR2003-1893},
	title = {A Logic of Events},
	year = 2003,
}

BC03a

@string{Aug = "August"}
@unpublished{BC03a,
	author = {Nina Bohr and Robert L. Constable},
	month = Aug,
	note = {Draft},
	title = {Defining Inductive and Co-Inductive Types Using Union and intersection Types},
	year = 2003,
}

BC03b

@unpublished{BC03b,
	author = {Baumslag, Gilbert and Cleary, Sean},
	note = {To appear in the Journal of Group Theory},
	title = {Parafree one-relator groups},
}

BC03c

@unpublished{BC03c,
	author = {Baumslag, Gilbert and Cleary, Sean},
	note = {Submitted for publication},
	title = {Parafree groups, the isomorphism problem and computation: I},
}

BC04

@book{BC04,
	author = {Bertot, Yves and Cast{\'e}ran, Pierre},
	publisher = {Springer-Verlag},
	series = {Texts in Theoretical Computer Science},
	title = {Interactive Theorem Proving and Program Development;           Coq'Art: The Calculus of Inductive Constructions},
	year = 2004,
}

BC05

@techreport{BC05,
	address = {Ithaca, NY},
	author = {Bickford, Mark and Constable, Robert L.},
	institution = {Cornell University, Computer Science Department},
	title = {A Causal Logic of Events in Formalized Computational Type Theory},
	year = 2005,
}

BC06

@inproceedings{BC06,
	author = {Bickford, Mark and Constable, Robert L.},
	booktitle = {Logical Aspects of Secure Computer Systems, Proceedings of International Summer School Marktoberdorf 2005},
	note = {Earlier version available as Cornell University Technical Report TR2005-2010, 2005},
	title = {A Causal Logic of Events in Formalized Computational Type Theory},
	year = {to Appear 2006},
}

BC81

@techreport{BC81,
	address = {Ithaca, NY},
	author = {Bates, J. L. and Robert L.~Constable},
	institution = {Cornell University, Computer Science Department},
	number = {82--492},
	title = {Definition of Micro-{\PRL}},
	year = 1981,
}

BC85

@string{TOPLAS = "{ACM} Transactions of Programming Language Systems"}
@article{BC85,
	author = {Bates, J. L. and Robert L.~Constable},
	journal = TOPLAS,
	number = 1,
	pages = {53--71},
	title = {Proofs as Programs},
	volume = 7,
	year = 1985,
}

BC91

@string{Jun = "June"}
@inproceedings{BC91,
	address = {Edinburgh, UK},
	author = {Basin, David A. and Robert L.~Constable},
	booktitle = {Proceedings of the Second Annual Workshop on Logical Frameworks},
	month = Jun,
	title = {Metalogical Frameworks},
	year = 1991,
}

BC92

@article{BC92,
	author = {Bellantoni, Stephen J. and S.~Cook},
	journal = {Computational Complexity},
	pages = {97--110},
	title = {A New Recursion-Theoretic Characterization of the Poly-time Functions},
	volume = 2,
	year = 1992,
}

BC93

@incollection{BC93,
	address = {Great Britain},
	author = {Basin, David A. and Robert L.~Constable},
	booktitle = {Logical Environments},
	chapter = 1,
	editor = {G.~Huet and G.~Plotkin},
	pages = {1--29},
	publisher = {Cambridge University Press},
	title = {Metalogical Frameworks},
	year = 1993,
}

BC93a

@string{Nov = "November"}
@unpublished{BC93a,
	author = {Bridges, D. and C. Calude},
	month = Nov,
	note = {To appear},
	title = {On Recursive Bounds for the Exceptional Values in Speed-up},
	year = 1993,
}

BCCHOG96

@article{BCCHOG96,
	author = {Bruce, Kim B. and Luca Cardelli and Giuseppe Castagna and The Hopkins Objects Group and Gary T. Leavens and Benjamin C. Pierce},
	journal = {Theory and Practice of Object Systems},
	number = 3,
	pages = {221--242},
	title = {On Binary Methods},
	volume = 1,
	year = 1996,
}

BCCPZ92

@unpublished{BCCPZ92,
	author = {Berkooz, G. and Paul Chew and J. Cremer and Rick Palmer and Richard Zippel},
	note = {Computer Science Department, Cornell University, Ithaca, NY},
	title = {Generating Spectral Method Solvers for Partial Differential Equations},
	year = 1992,
}

BCD89

@article{BCD89,
	author = {Brown, J.~S. and A.~Collins and P.~Duguid},
	journal = {Educational Researcher},
	number = 1,
	pages = {32--41},
	title = {Situated Cognition and the Culture of Learning},
	volume = 18,
	year = 1989,
}

BCD91

@string{Jun = "June"}
@inproceedings{BCD91,
	address = {Gaithersburg, MD},
	author = {Butler, Ricky and James Caldwell and Ben Di~Vito},
	booktitle = {Sixth Annual Conference on Computer Assurance},
	month = Jun,
	series = {COMPASS91},
	title = {Design Strategy for a Formally Verified Reliable Computing Platform},
	year = 1991,
}

BCF+97

@inproceedings{BCF+97,
	author = {C. Benzm{\"u}ller and L. Cheikhrouhou and D. Fehrer and others},
	crossref = {CADE97},
	title = {\textsc{{$\Omega$mega}}: Towards a Mathematical Assistant},
}

Fully expanded entry:

@string{LNAI = "Lecture Notes in Artificial Intelligence"}
@inproceedings{BCF+97,
	author = {C. Benzm{\"u}ller and L. Cheikhrouhou and D. Fehrer and others},
	booktitle = {Proceedings of the 14$^{th}$ International Conference on Automated Deduction},
	editor = {William McCune},
	isbn = {3-540-63104-6},
	month = {July 13--17},
	publisher = {Springer},
	series = LNAI,
	title = {\textsc{{$\Omega$mega}}: Towards a Mathematical Assistant},
	volume = 1249,
	year = 1997,
}

BCG83

@string{Nov = "November"}
@article{BCG83,
	author = {Balzer, R. and T. E. Cheatham, Jr. and C. Green},
	journal = {Computer},
	month = Nov,
	pages = {39--45},
	title = {Software Technology in the 1990's:  Using a new paradigm},
	year = 1983,
}

BCGS91

@string{Jul = "July"}
@article{BCGS91,
	author = {Breazu-Tannen, V. and Thierry Coquand and Carl A. Gunter and Andre Scedrov},
	journal = {Information and Computation},
	month = Jul,
	number = 1,
	pages = {172--222},
	title = {Inheritance as Implicit Coercion},
	volume = 93,
	year = 1991,
}

BCHH00

@inproceedings{BCHH00,
	address = "Hilton Head, SC",
	author = "Ken Birman and Robert Constable and Mark Hayden and Jason                      Hickey and Christoph Kreitz and Robbert van Renesse and                      Ohad Rodeh and Werner Vogels",
	booktitle = "DARPA Information Survivability Conference and Exposition                      (DISCEX 2000)",
	optwwwref = {http://www.nuprl.org/documents/Constable/00discex-horus.html},
	pages = "149--161",
	publisher = "IEEE Computer Society Press",
	title = "The {\Horus} and {\Ensemble} Projects: Accomplishments and                     Limitations.",
	year = 2000,
}

BCHHKRRV00

@inproceedings{BCHHKRRV00,
	crossref = {BCHH00},
}

Fully expanded entry:

@inproceedings{BCHHKRRV00,
	address = "Hilton Head, SC",
	author = "Ken Birman and Robert Constable and Mark Hayden and Jason                      Hickey and Christoph Kreitz and Robbert van Renesse and                      Ohad Rodeh and Werner Vogels",
	booktitle = "DARPA Information Survivability Conference and Exposition                      (DISCEX 2000)",
	optwwwref = {http://www.nuprl.org/documents/Constable/00discex-horus.html},
	pages = "149--161",
	publisher = "IEEE Computer Society Press",
	title = "The {\Horus} and {\Ensemble} Projects: Accomplishments and                     Limitations.",
	year = 2000,
}

BCHP05

@string{LNCS = "Lecture Notes in Computer Science"}
@inproceedings{BCHP05,
	author = {Mark Bickford and Robert C. Constable and Joseph Y. Halpern and Sabina Petride},
	booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning},
	editor = {Franz Baader and Andreo Voronsky},
	pages = {449--465},
	series = LNCS,
	title = {Knowledge-Based Synthesis of Distributed Systems Using Event Structures},
	volume = 3452,
	year = 2005,
}

BCK97

@article{BCK97,
	author = "M. Bellare and R. Canetti and H. Krawczyk",
	journal = "RSA Laboratories' Cryptobytes",
	number = 1,
	title = "Message authentication using hash functions: The {HMAC} construction",
	volume = 2,
	year = 1997,
}

BCL83

@book{BCL83,
	address = {Wien},
	edition = {second},
	editor = {Buchberger, B. and G. E. Collins and R. G. K. Loos},
	publisher = {Springer-Verlag},
	title = {Computer Algebra --- Symbolic and Algebraic Computation},
	year = 1983,
}

BCLM88

@techreport{BCLM88,
	author = {Bose, S. and E. M. Clarke and D. E. Long and S. Michaylov},
	institution = {Carnegie Mellon University},
	title = {A Parallel Theorem Prover for Non-Horn Clauses},
	year = 1988,
}

BCLR04

@techreport{BCLR04,
	author = {Ball, Thomas and Byron Cook and Vladimir Levin and Sriram K. Rajamani},
	institution = {Microsoft},
	note = {To appear as invited paper for Integrated Formal Methods 2004},
	number = {MSF-TR-2004-8},
	title = {{SLAM} and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft},
	year = 2004,
}

BCM88

@article{BCM88,
	author = {Backhouse, R. C. and P. Chisholm and G. Malcolm},
	journal = {EATCS Bulletin},
	pages = {205--245},
	title = {Do-it-yourself Type theory (part {II})},
	volume = 35,
	year = 1988,
}

BCMDH90

@inproceedings{BCMDH90,
	author = {J. R. Burch and E. M. Clarke and K. L. McMillan and D. L. Dill and L. J. Hwang},
	crossref = {LICS90},
	title = {Symbolic model checking: {$10^20$} states and beyond},
}

Fully expanded entry:

@string{Jun = "June"}
@inproceedings{BCMDH90,
	author = {J. R. Burch and E. M. Clarke and K. L. McMillan and D. L. Dill and L. J. Hwang},
	booktitle = {Proceedings of the 5$^{th}$ Symposium on Logic in Computer Science},
	key = {LICS90},
	month = Jun,
	publisher = {IEEE Computer Society Press},
	title = {Symbolic model checking: {$10^20$} states and beyond},
	year = 1990,
}

BCMDH92

@string{Jun = "June"}
@article{BCMDH92,
	author = {J. R. Burch and E. M. Clarke and K. L. McMillan and D. L. Dill and L. J. Hwang},
	journal = {Information and Computation},
	month = Jun,
	number = 2,
	pages = {142--170},
	title = {Symbolic model checking: $10^20$ states and beyond},
	volume = 98,
	year = 1992,
}

BCMS89

@article{BCMS89,
	author = {Roland C. Backhouse and Paul Chisholm and Grant Malcolm and Erik Saaman},
	journal = {Formal Aspects of Computing},
	pages = {19--84},
	title = {Do-it-yourself Type theory},
	volume = 1,
	year = 1989,
}

BCP96

@inproceedings{BCP96,
	author = {Bruce, Kim B. and Luca Cardelli and Benjamin C. Pierce},
	booktitle = {Proceedings of FOOL 3},
	title = {Comparing Object Encodings},
	year = 1996,
}

BCR86

@inproceedings{BCR86,
	author = {Boehm, Hans-J. and Robert Cartwright and Mark Riggle and Michael J. O'Donnell},
	booktitle = {{ACM} Symposium on Lisp and Functional Programming},
	publisher = {ACM},
	title = {Exact Real Arithmetic: {A} Case Study in Higher Order Programming},
	year = 1986,
}

BCS01

@article{BCS01,
	author = {Burillo, J. and Cleary, S. and Stein, M. I.},
	issn = {0002-9947},
	journal = {Transactions of the American Mathematical Society},
	number = 4,
	pages = {1677--1689},
	title = {Metrics and embeddings of generalizations of {T}hompson's group ${F}$},
	volume = 353,
	year = 2001,
}

BCZ98

@article{BCZ98,
	author = {Andrej Bauer and Edmund M. Clarke and Xudong Zhao},
	journal = {Journal of Automated Reasoning},
	number = 3,
	pages = {295--325},
	title = {{\Analytica} --- An Experiment in Combining Theorem Proving and Symbolic Computation},
	volume = 21,
	year = 1998,
}

BD77

@string{Jan = "January"}
@article{BD77,
	author = {Burstall, R. and J. Darlington},
	journal = {J. Assoc. Comput. Mach.},
	month = Jan,
	pages = {44--67},
	title = {A Transformation System for Developing Recursive Programs},
	volume = 24,
	year = 1977,
}

BD89

@techreport{BD89,
	author = {Basin, David A. and P. Del Vecchio},
	institution = {Cornell University},
	number = {89--1018},
	title = {Verification of Combinational Logic in {\Nuprl}},
	year = 1989,
}

BD89a

@string{LNCS = "Lecture Notes in Computer Science"}
@inproceedings{BD89a,
	author = {Basin, David A. and P. Del Vecchio},
	booktitle = {Hardware Specification, Verification and Synthesis:  Mathematical Aspects},
	pages = {333--357},
	publisher = {Springer-Verlag},
	series = LNCS,
	title = {Verification of Combinational Logic in {\Nuprl}},
	volume = 408,
	year = 1989,
}

BDGB98

@string{May = "May"}
@article{BDGB98,
	author = {Babaoglu, O. and Davoli, R. and Giachini, L. and Baker, G.},
	journal = {Proceedings of the 18th IEEE International Conference on Distributed Computing Systems},
	month = May,
	title = {System support for partition-aware network applications},
	year = 1998,
}

BDI88

@inproceedings{BDI88,
	author = {Borras, P. and D.~Cl{\'e}ment and T.~Despeyroux and J.~Incerpi and G.~Kahn and B.~Lang and V.~Pascual},
	booktitle = {Software Engineering Notes},
	organization = {Third Symposium on Software Development Environments},
	title = {Centaur:  the system},
	volume = {13(5)},
	year = 1988,
}

BDL89

@book{BDL89,
	address = {New York},
	author = {Baxter, Nancy and Ed Dubinsky and Gary Levin},
	publisher = {Springer-Verlag},
	title = {Learning Discrete Mathematics with ISETL},
	year = 1989,
}

BDOPV95

@article{BDOPV95,
	author = "B. Bacci  and M. Danelutto and S. Orlando and S.  Pelagatti and M. Vanneschi",
	journal = "Concurrency: Practice and Experience",
	month = "May",
	number = 3,
	pages = {225--255},
	title = "{P$^3$L}: A Structured High level programming language and its structured support",
	volume = 7,
	year = 1995,
}

BE91

@book{BE91,
	address = {Stanford University},
	author = {Barwise, John and John Etchemendy},
	edition = {Second},
	publisher = {Center for the Study of Language and Information},
	series = {Lecture Notes Number 23},
	title = {The Language of First-Order Logic},
	year = 1991,
}

BE94

@book{BE94,
	address = {Stanford, California},
	author = {Barwise, John and John Etchemendy},
	publisher = {Center for the Study of Language and Information, Stanford University},
	title = {Hyperproof},
	year = 1994,
}

Bee81

@string{LNM = "Lecture Notes in Mathematics"}
@inproceedings{Bee81,
	author = {Beeson, Michael J.},
	booktitle = {Constructive Mathematics},
	editor = {F. Richman},
	pages = {146--90},
	publisher = {Springer, Berlin},
	series = LNM,
	title = {Formalizing Constructive Mathematics: Why and How?},
	volume = 873,
	year = 1981,
}

Bee82

@article{Bee82,
	author = {Beeson, Michael J.},
	journal = {Anals of Math Logic},
	pages = {127--78},
	title = {Recursive models for constructive set theory},
	volume = 23,
	year = 1982,
}

Bee83

@inproceedings{Bee83,
	author = {Beeson, Michael J.},
	booktitle = {International Congress on Logic, Methodology and Philosophy Science},
	publisher = {North-Holland, Salzburg, Austria},
	title = {Proving Programs and Programming Proofs},
	year = 1983,
}

Bee85

@book{Bee85,
	author = {Beeson, Michael J.},
	publisher = {Springer-Verlag},
	title = {Foundations of Constructive Mathematics},
	year = 1985,
}

Bee88

@article{Bee88,
	author = {Beeson, Michael J.},
	journal = {Theoretical Computing Science},
	pages = {247--340},
	title = {Towards a Computation System Based on Set Theory},
	volume = 60,
	year = 1988,
}

Bee94

@misc{Bee94,
	author = {Beeson, Michael J.},
	note = {Personal Communication},
	title = {The {M}ath{P}ert {S}ystem},
	year = 1994,
}

BEGK87

@string{LNCS = "Lecture Notes in Computer Science"}
@article{BEGK87,
	author = {Barendregt, H. P. and M. C. D. J. van Eekelen and J. R. W. Glauert and J. R. Kennaway and M. J. Plasmeijer and M. R. Sleep},
	journal = {Parallel Architectures and Languages Europe, Volume~{II}},
	pages = {141--158},
	series = LNCS,
	title = {Term Graph Rewriting},
	volume = 256,
	year = 1987,
}

Bei64

@book{Bei64,
	address = {New York},
	author = {Albert H.~Beiler},
	publisher = {Dover Publications Inc.},
	title = {Recreations in the Theory of Numbers},
	year = 1964,
}

Bel88

@book{Bel88,
	address = {Oxford},
	author = {John L.~Bell},
	publisher = {Oxford University Press},
	series = {Oxford Logic Guides},
	title = {Toposes and Local Set Theories},
	volume = 14,
	year = 1988,
}

BEL98

@article{BEL98,
	author = {M.~Baaz and U.~Egly and A.~Leitsch},
	journal = {Chapter 12 in Automated Deduction. A basis for applications},
	note = {Kluwer Academic Publishers},
	title = {Extension Methods in Automated Deduction},
	volume = {Vol. II},
	year = 1998,
}

Ben00

@string{JFP = "Journal of Functional Programming"}
@string{Jan = "January"}
@article{Ben00,
	author = "Ralph Benzinger",
	journal = JFP,
	month = Jan,
	number = 1,
	pages = "3--31",
	title = "Automated Complexity Analysis of {\Nuprl} Extracted Programs",
	volume = 11,
	year = 2001,
}

Ben01

@phdthesis{Ben01,
	author = {Ralph Benzinger},
	note = {Cornell Technical Report TR2002-1880},
	school = {Cornell University},
	title = {Automated Computational Complexity Analysis},
	year = 2001,
}

Ben82

@book{Ben82,
	author = {Bentley, J. L.},
	publisher = {Prentice-Hall, Englewood Cliffs, NJ},
	title = {Writing Efficient Programs},
	year = 1982,
}

Ber04

@phdthesis{Ber04,
	author = {Berghofer, Stefan},
	school = {Technische Universit{\"a}t M{\"u}nchen},
	title = {Proofs, Programs and Executable Specifications in Higher Order Logic},
	year = 2004,
}

Ber85

@incollection{Ber85,
	address = {Voaron},
	author = {Berman, R.~H.},
	booktitle = {Applications of computer algebra},
	editor = {Richard Pavelle},
	pages = {210--241},
	publisher = {Kluwer Academic Publishers},
	title = {Fourier transform algorithms for spectral analysis derived with {M}acsyma},
	year = 1985,
}

Ber90

@inproceedings{Ber90,
	address = {Sophia-Antipolis, France},
	author = {S. Berardi},
	booktitle = {Draft Proceedings of the First Annual Workshop on Logical Frameworks},
	pages = {??},
	title = {Girard Normalization Proof in LEGO},
	year = 1990,
}

BF03

@article{BF03,
	author = {D. Boneh and M. Franklin},
	journal = {SIAM J. of Computing},
	number = 3,
	pages = {586--615},
	title = {Identity based encryption from the Weil pairing},
	volume = 32,
	year = 2003,
}

BF58

@book{BF58,
	address = {Amsterdam},
	author = {Paul Bernays and A.~A.~Fraenkel},
	publisher = {North-Holland Publishing Company},
	title = {Axiomatic Set Theory},
	year = 1958,
}

BF95

@inproceedings{BF95,
	author = {Bodeveix, J. P. and M. Filali},
	booktitle = {Proceedings of the Workshop on TACAS},
	title = {A framework for parallel program refinement},
	year = 1995,
}

BFPS81

@string{LNM = "Lecture Notes in Mathematics"}
@article{BFPS81,
	author = {Buchholtz, W. and others},
	journal = {Recent Proof-Theoretical Studies},
	pages = {16--77},
	publisher = {Springer-Verlag, NY},
	series = LNM,
	title = {Iterated Inductive Definitions and Subsystems of Analysis},
	volume = 897,
	year = 1981,
}

BG01

@incollection{BG01,
	author = "Henk Barendregt and Herman Geuvers",
	booktitle = "Handbook of Automated Reasoning",
	editor = "A. Robinson and A. Voronkov",
	pages = "1149--1238",
	publisher = "Elsevier",
	title = "Proof-Assistants Using Dependent Type Systems",
	year = 2001,
}

BG03a

@article{BG03a,
	author = {Blass, Andreas and Gurevich, Yuri},
	journal = {ACM Transactions on Computational Logic},
	number = 4,
	pages = {578--651},
	title = {Abstract state machines capture parallel algorithms},
	volume = 4,
	year = 2003,
}

BG03b

@string{Oct = "October"}
@article{BG03b,
	author = {Blass, Andreas and Gurevich, Yuri},
	journal = {Bulletin of the European Association for Theoretical Computer Science},
	month = Oct,
	pages = {195--225},
	title = {Algorithms: A Quest for Absolute Definitions},
	volume = 81,
	year = 2003,
}

BG05

@techreport{BG05,
	author = {Bickford, Mark and Guaspari, David},
	institution = {ATC-NY},
	title = {A Programming Logic for Distributed Systems},
	year = 2005,
}

BG89

@string{LNCS = "Lecture Notes in Computer Science"}
@inproceedings{BG89,
	author = {Breazu-Tannen, V. and J. Gallier},
	booktitle = {Automata, Languages and Programming --- 16th International Colloquium (Stresa, Italy)},
	editor = {G. Ausiello and M. Dezani-Ciancaglini and S. Ronchi Della Rocca},
	pages = {137--150},
	publisher = {Springer-Verlag},
	series = LNCS,
	title = {Polymorphic rewriting conserves algebraic strong normalization and confluence},
	volume = 372,
	year = 1989,
}

BG90

@inproceedings{BG90,
	author = {Blaine, Lee and Allen Goldberg},
	booktitle = {Proceedings of the IFIP TC2 working conference on Constructing Programs from Specifications},
	editor = {B.~M{\"o}ller},
	publisher = {Elsevier},
	title = {{DTRE}---A Semi-Automatic Transformation System},
	year = 1991,
}

BG96

@techreport{BG96,
	address = {PO Box 513 5600 MB Eindhoven, The Netherlands},
	author = {Bloo, R. and Geuvers, J. H.},
	institution = {Eindhoven University of Technology},
	number = {Computing Science Reports 96-10},
	title = {Explicit Substituion: On the Edge of Strong Normalisation},
	year = 1996,
}

BGHP98

@inproceedings{BGHP98,
	author = {Andrew Barber and Philippa Gardner and Masahito Hasegawa and Gordon D. Plotkin},
	crossref = {CSL98},
	pages = {78--97},
	title = {From Action Calculi to Linear Logic},
}

Fully expanded entry:

@string{LNCS = "Lecture Notes in Computer Science"}
@inproceedings{BGHP98,
	author = {Andrew Barber and Philippa Gardner and Masahito Hasegawa and Gordon D. Plotkin},
	booktitle = {Computer Science Logic, 11$^{th}$ International Workshop, Annual Conference of the EACSL, Aarhus, Denmark, August 23--29, 1997, Selected Papers},
	editor = {Mogens Nielsen and Wolfgang Thomas},
	pages = {78--97},
	publisher = {Springer},
	series = LNCS,
	title = {From Action Calculi to Linear Logic},
	volume = 1414,
	year = 1998,
}

BGL+00

@string{Jun = "June"}
@inproceedings{BGL+00,
	address = {Hampton, {VA}},
	author = {Saddek Bensalem and Vijay Ganesh and Yassine Lakhnech and C{\'e}sar Mu{\~n}oz and Sam Owre and Harald Rue\ss and John Rushby and Vlad Rusu and Hassen Sa{\"\i}di and {N.} Shankar and Eli Singerman and Ashish Tiwari},
	booktitle = {{LFM} 2000: Fifth {NASA} Langley Formal Methods Workshop},
	editor = {{C.} Michael Holloway},
	month = Jun,
	organization = {{NASA} Langley Research Center},
	pages = {187--196},
	title = {An Overview of \textsf{SAL}},
	url = {http://www.csl.sri.com/papers/lfm2000/},
	year = 2000,
}

BGL98

@inproceedings{BGL98,
	author = "Lee Blaine and Li-Mei Gilham and Junbo Liu and Douglas R.                      Smith and Stephen Westfold",
	booktitle = "Thirteenth Automated Software Engineering Conference",
	pages = "270--280",
	publisher = "IEEE Computer Society Press",
	title = "Planware -- Domain-Specific Synthesis of High-Performance                      Schedulers",
	year = 1998,
}

BGMWW92

@string{Apr = "April"}
@article{BGMWW92,
	author = {A. Back and J. Guckenheimer and M. Myers and F. Wicklin and P. Worfolk},
	journal = {Computers and Mathematics},
	month = Apr,
	number = 4,
	pages = {303--309},
	title = {\emph{dstool}: Computer assisted Expoloration of Dynamical Systems},
	volume = 39,
	year = 1992,
}

BGS03

@unpublished{BGS03,
	author = {Becker, Marcel and Limei Gilham and Douglas R. Smith},
	note = {Submitted for publication},
	title = {Planware {II}: Synthesis of Schedulers for Complex Resource Systems},
	year = 2003,
}

BGW90

@inproceedings{BGW90,
	author = {Bundy, A. and F. Giunchiglia and T. Walsh},
	booktitle = {Proceedings of the AAAI-90 Workshop on Automatic Generation of Approximations and Abstractions},
	note = {Also available from Edinburgh as DAI Research Paper No. 506},
	organization = {Amer. Assoc. for Art. Intelligence},
	pages = {221--232},
	title = {Building abstractions},
	year = 1990,
}

BH02

@misc{BH02,
	author = {Levente Butty{\'a}n and Jean-Pierre Hubaux},
	title = {Report on a Working Session on Security in Wireless Ad Hoc Networks},
	year = 2002,
}

BH91

@string{LNCS = "Lecture Notes in Computer Science"}
@incollection{BH91,
	author = {Basin, David A. and Douglas J.~Howe},
	booktitle = {Theoretical Aspects of Computer Software, International Conference TACS '91, {\rm Sendai, Japan}},
	pages = {475--494},
	publisher = {Springer-Verlag},
	series = LNCS,
	title = {Some Normalization Properties of {M}artin-{L}{\"{o}}f's Type Theory, and Applications},
	volume = 526,
	year = 1991,
}

BH98

@unpublished{BH98,
	author = {Bickford, Mark and Jason J. Hickey},
	note = {Department of Computer Science, Cornell University, Unpublished},
	optwwwpdf = {http://mojave.caltech.edu/jyh/papers/cav99_ooioa/paper.pdf},
	optwwwps = {http://mojave.caltech.edu/jyh/papers/cav99_ooioa/paper.ps},
	title = {An Object-Oriented Approach to Verifying Group Communication Systems},
	year = 1998,
}

BH99

@inproceedings{BH99,
	author = {Mark Bickford and Jason J. Hickey},
	booktitle = {Proceedings of $3^{rd}$ Irish Workshop in Formal Methods},
	optwwwpdf = {http://www.bcs.org/upload/pdf/ewic_fm99_paper2.pdf},
	title = {Predicate Transformers for Infinite-State Automata in {\Nuprl} Type Theory},
	year = 1999,
}

BHC95

@inproceedings{BHC95,
	author = "Clemens Ballarin and Karsten Homann and Jacques Calmet",
	booktitle = "Proceeding of International Symposium on Symbolic and Algebraic Computation",
	pages = "150--157",
	publisher = "{ACM} Press",
	title = "Theorems and Algorithms: {A}n Interface between {\Isabelle} and {\Maple}",
	url = citeseer.nj.nec.com/ballarin95theorem.html,
	year = 1995,
}

BHHS89

@string{May = "May"}
@unpublished{BHHS89,
	author = {Bundy, A. and F. van Harmelen and J. Hesketh and A. Smaill},
	month = May,
	note = {Unpublished},
	title = {Experiments with Proof Plans for Induction},
	year = 1989,
}

BHHS90

@inproceedings{BHHS90,
	author = {Bundy, A. and F. van Harmelen and C. Horn and A. Smaill},
	crossref = {CADE90},
	pages = {647--648},
	title = {The {O}yster-{C}lam system},
}

Fully expanded entry:

@string{LNAI = "Lecture Notes in Artificial Intelligence"}
@inproceedings{BHHS90,
	author = {Bundy, A. and F. van Harmelen and C. Horn and A. Smaill},
	booktitle = {Proceedings of the 10$^{th}$ International Conference on Automated Deduction},
	editor = {Mark E. Stickel},
	pages = {647--648},
	publisher = {Springer-Verlag},
	series = LNAI,
	title = {The {O}yster-{C}lam system},
	volume = 449,
	year = 1990,
}

BHHS91

@article{BHHS91,
	author = {Bundy, A. and F. van Harmelen and J. Hesketh and A. Smaill},
	journal = {Journal of Automated Reasoning},
	pages = {303--324},
	title = {Experiments with proof plans for induction},
	volume = 7,
	year = 1991,
}

BHKO02

@string{Jul = "July"}
@string{TOPLAS = "{ACM} Transactions of Programming Language Systems"}
@article{BHKO02,
	author = {Mark van den Brand and Jan Heering and Paul Klint and Pieter A. Olivier},
	journal = TOPLAS,
	month = Jul,
	number = 4,
	pages = {334--368},
	title = {Compiling Language Definitions: The {ASF}+{SDF} Compiler},
	url = {http://portal.acm.org/citation.cfm?doid=567097.567099},
	volume = 24,
	year = 2002,
}

BHL01

@string{May = "May"}
@article{BHL01,
	author = {Bemers-Lee, T. and J. Hendler and O. Lassila},
	journal = {Scientific American},
	month = May,
	number = 5,
	pages = {34--43},
	title = {The Semantic Web},
	volume = 279,
	year = 2001,
}

BHLM94

@unpublished{BHLM94,
	author = {Biagioni, Edoardo and Robert Harper and Peter Lee and Brian G. Milnes},
	note = {To appear in Lisp and Functional Programming 1994 and SIGCOMM 1994.},
	title = {Signatures for a Network Protocol Stack: A Systems Application of Standard ML},
	year = 1994,
}

BHMvE97

@inproceedings{BHMvE97,
	author = {A. Basu and M. Hayden and G. Morrisett and T. von~Eicken},
	crossref = {DSL97},
	pages = {1--15},
	title = {A language-based approach to protocol construction},
}

Fully expanded entry:

@string{Jan = "January"}
@inproceedings{BHMvE97,
	author = {A. Basu and M. Hayden and G. Morrisett and T. von~Eicken},
	booktitle = {DSL'97 -- First {ACM} SIGPAN Workshop on Domain-Specific Languages, in Association with {POPL}'97},
	editor = {S. Kamin},
	location = {Paris, France},
	month = Jan,
	pages = {1--15},
	title = {A language-based approach to protocol construction},
	year = 1997,
}

BHOX98

@string{May = "May"}
@techreport{BHOX98,
	annote = {\url{http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR98-1683}},
	author = {Birman, Kenneth and Mark Hayden and Oznur Ozkasap and  Zhen Xiao and Mihai Budiu and Yaron Minsky},
	institution = {Cornell University},
	month = May,
	number = {TR 98-1683},
	title = {Bimodal Multicast},
	year = 1998,
}

BHSI90

@inproceedings{BHSI90,
	author = {Bundy, A. and F. van Harmelen and A. Smaill and A. Ireland},
	crossref = {CADE90},
	pages = {132--146},
	title = {Extensions to the rippling-out tactic for guiding inductive proofs},
}

Fully expanded entry:

@string{LNAI = "Lecture Notes in Artificial Intelligence"}
@inproceedings{BHSI90,
	author = {Bundy, A. and F. van Harmelen and A. Smaill and A. Ireland},
	booktitle = {Proceedings of the 10$^{th}$ International Conference on Automated Deduction},
	editor = {Mark E. Stickel},
	pages = {132--146},
	publisher = {Springer-Verlag},
	series = LNAI,
	title = {Extensions to the rippling-out tactic for guiding inductive proofs},
	volume = 449,
	year = 1990,
}

BI92

@article{BI92,
	author = {Bridges, D. and H. Ishihara},
	journal = {Bull. London Math. Soc.},
	note = 1992,
	pages = {599--605},
	title = {Locating the Range of an Operator on a Hilbert Space},
	volume = 24,
	year = 1992,
}

BI93

@string{Sep = "September"}
@techreport{BI93,
	address = {Mathematical Sciences Institute, Ithaca, NY},
	author = {Bridges, D. and H. Ishihara},
	institution = {Cornell University},
	month = Sep,
	number = {93--70},
	title = {Spectra of Selfadjoint Operators in Constructive Analysis},
	year = 1993,
}

Bia94

@inproceedings{Bia94,
	author = "Edoardo Biagioni",
	booktitle = "{SIGCOMM}",
	pages = "36--45",
	title = "A Structured {TCP} in Standard {ML}",
	url = citeseer.nj.nec.com/biagioni94structured.html,
	year = 1994,
}

Bib82

@book{Bib82,
	address = {Braunschweig},
	author = {W. Bibel},
	publisher = {Vieweg},
	title = {Automated Theorem Proving},
	year = 1982,
}

Bib87

@book{Bib87,
	address = "Braunschweig, 2nd edition",
	author = "W. Bibel",
	publisher = "Vieweg Verlag",
	title = "Automated Theorem Proving",
	year = 1987,
}

Bib91

@incollection{Bib91,
	address = {Menlo Park, CA},
	author = {Bibel, W.},
	booktitle = {Automating Software Design},
	editor = {M. R. Lowry and R. Mcartney},
	pages = {405--424},
	publisher = {MIT Press},
	title = {Toward predicative programming},
	year = 1991,
}

Bic03

@misc{Bic03,
	author = {Mark Bickford},
	howpublished = {\emph{In Progress}},
	title = {Experiments with theory modification in the {FDL}},
	year = 2003,
}

Bic03b

@misc{Bic03b,
	author = {Mark Bickford},
	howpublished = {{\Nuprl} Math Library Book webpage},
	note = {\url{http://www.nuprl.org/Nuprl4.2/Libraries/}},
	title = {Event Systems},
	year = 2003,
}

Bic04

@misc{Bic04,
	author = {Mark Bickford},
	note = {In preparation},
	title = {Semantics of Event Correlation Languages in a Theory of Events},
	year = 2004,
}

Bic06

@techreport{Bic06,
	address = {Ithaca, NY},
	author = {Mark Bickford},
	institution = {Cornell University},
	note = {To be published, March 2006},
	title = {Unguessable Atoms: A Logical Foundation for Security},
	year = 2006,
}

Bir04

@book{Bir04,
	author = {Kenneth P. Birman},
	publisher = {Springer-Verlag},
	title = {Reliable Distributed Systems},
	year = 2004,
}

Bir93

@string{Dec = "December"}
@article{Bir93,
	author = {Kenneth P. Birman},
	journal = {Communications of the {ACM}},
	month = Dec,
	number = 12,
	pages = {37--53},
	title = {The Process Group Approach to Reliable Distributed Computing},
	volume = 36,
	year = 1993,
}

Bir97

@string{Jan = "January"}
@book{Bir97,
	author = {Kenneth P. Birman},
	month = Jan,
	publisher = {Manning Publishing Company and Prentice Hall},
	title = {Building Secure and Reliable Network Applications},
	year = 1997,
}

Bis67

@book{Bis67,
	address = {NY},
	author = {Bishop, E.},
	publisher = {McGraw Hill},
	title = {Foundations of Constructive Analysis},
	year = 1967,
}

Bis70

@inproceedings{Bis70,
	author = {Bishop, E.},
	booktitle = {Intuitionism and Proof Theory},
	pages = {53--71},
	publisher = {North-Holland, NY},
	title = {Mathematics as a Numerical Language},
	year = 1970,
}

BJ80

@book{BJ80,
	author = {Boolos, George S. and Richard C. Jeffrey},
	publisher = {Cambridge University Press},
	title = {Computability and Logic, Second Edition},
	year = 1980,
}

BJ87

@string{Nov = "November"}
@article{BJ87,
	author = {Birman, Kenneth~P. and Joseph, Thomas~A.},
	journal = {Proc 11th Symposium on Operating Systems Principles (SOSP)},
	month = Nov,
	pages = {123--138},
	title = {Exploiting virtual synchrony in distributed systems},
	year = 1987,
}

BJ87a

@string{Feb = "February"}
@article{BJ87a,
	author = {Birman, Kenneth P. and Joseph, Thomas A.},
	journal = {{ACM} Transactions on Computer Systems},
	month = Feb,
	number = 1,
	pages = {47--76},
	title = {Reliable Communication in the Presence of Failures},
	volume = 5,
	year = 1987,
}

BJ89

@book{BJ89,
	author = {Boolos, G. S. and R. C. Jeffrey},
	publisher = {Cambridge University Press},
	title = {{Computability and Logic, Third Edition}},
	year = 1988,
}

BK03

@string{Sep = "September"}
@misc{BK03,
	author = {Mark Bickford and Alexei Kopylov},
	howpublished = {\emph{In Progress}},
	month = Sep,
	title = {Verification of protocols by combining provers using the {FDL}},
	year = 2003,
}

BK91

@incollection{BK91,
	author = {Basin, David A. and Matt Kaufmann},
	booktitle = {Logical Frameworks},
	editor = {G{\'{e}}rard Huet and Gordon Plotkin},
	pages = {89--119},
	publisher = {Cambridge University Press},
	title = {The {B}oyer-{M}oore prover and {\Nuprl}:  {A}n experimental comparison},
	year = 1991,
}

BKKN03

@inproceedings{BKKN03,
	author = {Yegor Bryukhov and Alexei Kopylov and Vladimir Krupski and Aleksey Nogin},
	crossref = {tphols2003b},
	optwwwref = {http://nogin.org/papers/arith.html},
	pages = {29--39},
	title = {Implementing and Automating Basic Number Theory in {\MetaPRL} Proof Assistant},
	url = {http://nogin.org/papers/arith.html},
}

Fully expanded entry:

@inproceedings{BKKN03,
	author = {Yegor Bryukhov and Alexei Kopylov and Vladimir Krupski and Aleksey Nogin},
	booktitle = {16$^{th}$ International Conference on Theorem Proving in Higher Order Logics ({TPHOLs} 2003). Emerging Trends Proceedings},
	editor = {David Basin and Burkhart Wolff},
	key = {TPHOLs03B},
	optwwwref = {http://nogin.org/papers/arith.html},
	pages = {29--39},
	publisher = {Universit{\"a}t Freiburg},
	title = {Implementing and Automating Basic Number Theory in {\MetaPRL} Proof Assistant},
	url = {http://nogin.org/papers/arith.html},
	year = 2003,
}

BKN96

@article{BKN96,
	author = {Roel Bloo and Fairouz Kamareddine and Rob Nederpelt},
	journal = {Information and Computation},
	number = 2,
	pages = {123--143},
	title = {The {Barendregt} Cube with Definitions and Generalised Reduction},
	volume = 126,
	year = 1996,
}

BKS85

@string{Dec = "December"}
@article{BKS85,
	author = {Bledsoe, W. W. and Kunen, K. and Shostak, R.},
	issn = {0004-3702},
	journal = {Artificial Intelligence},
	month = Dec,
	pages = {255--288},
	title = {Completeness results for inequality provers},
	volume = {27(3)},
	year = 1985,
}

BKVC01

@inproceedings{BKVC01,
	address = "Anaheim, CA",
	author = "Mark Bickford and Christoph Kreitz and Robbert van Renesse and Robert Constable",
	booktitle = "DARPA Information Survivability Conference and Exposition II (DISCEX-II)",
	editor = "J. Lala and D. Mughan and C. McCollum and B. Witten",
	pages = "100--107",
	series = "IEEE Computer Society Press",
	title = "An Experiment in Formal Design Using Meta-properties",
	volume = "II",
	year = 2001,
}

BKVL01

@inproceedings{BKVL01,
	author = "Mark Bickford and Christoph Kreitz and Robbert van Renesse                      and Xiaoming Liu",
	crossref = "tphols2001",
	pages = "105--120",
	title = "Proving Hybrid Protocols Correct",
}

Fully expanded entry:

@string{LNCS = "Lecture Notes in Computer Science"}
@string{Sep = "September"}
@inproceedings{BKVL01,
	address = {Edinburgh, Scotland},
	author = "Mark Bickford and Christoph Kreitz and Robbert van Renesse                      and Xiaoming Liu",
	booktitle = {14$^{th}$ International Conference on Theorem Proving in Higher Order Logics},
	editor = {Richard Boulton and Paul Jackson},
	key = {TPHOLs01},
	month = Sep,
	pages = "105--120",
	publisher = {Springer-Verlag},
	series = LNCS,
	title = "Proving Hybrid Protocols Correct",
	volume = 2152,
	year = 2001,
}

BKvR01

@techreport{BKvR01,
	address = {Ithaca, New York},
	author = {Mark Bickford and Christoph Kreitz and Robbert van Renesse},
	institution = {Cornell University},
	number = {TR2001-1839},
	title = {Formally Verifying Hybrid Protocols with the {\Nuprl} Logical Programming Environment},
	year = 2001,
}

BL76

@string{Mar = "March"}
@techreport{BL76,
	author = {D.~E.~Bell and L.~J.~LaPadula},
	institution = {The MITRE Corporation},
	month = Mar,
	number = {MTR-2997},
	title = {Secure Computer System: Unified Exposition and Multics Interpretation},
	year = 1976,
}

BL84

@book{BL84,
	author = {Bledsoe, W. W. and D. W. Loveland},
	publisher = {American Math Soc.},
	title = {{Automated Theorem Proving: After 25 Years}},
	year = 1984,
}

BL94

@incollection{BL94,
	address = {Cambridge, MA},
	author = {Bruce, Kim B. and G. Longo},
	booktitle = {Theoretical Aspects of Object-Oriented Programming, Types, Semantics and Language Design},
	chapter = {III},
	editor = {C. A. Gunter, J. C. Mitchell},
	pages = {151--196},
	publisher = {MIT Press},
	title = {A Modest Model of Records, Inheritance, and Bounded Quantification},
	year = 1994,
}

Bla79

@inproceedings{Bla79,
	author = {G.R. Blakley},
	booktitle = {AFIPS Conference Proceedings},
	pages = {313--317},
	title = {Safeguarding cryptographic keys},
	volume = 48,
	year = 1979,
}

Ble75

@string{Sep = "September"}
@article{Ble75,
	author = {Bledsoe, W. W.},
	journal = {Fourth Intl. Joint Conference on AI, {\rm Tblisi, USSR}},
	month = Sep,
	title = {A new method for proving certain {P}resburger formulas},
	year = 1975,
}

Blo90

@article{Blo90,
	author = {Bard Bloom},
	journal = {Information and Computation},
	pages = {264--301},
	title = {Can {\LCF} be topped?  flat lattice models of Typed $\lambda$-calculus},
	volume = 87,
	year = 1990,
}

BLP03

@inproceedings{BLP03,
	author = {Giampaolo Bella and Cristiano Longo and L. C. Paulson},
	crossref = {tphols2000},
	pages = {352--366},
	title = {Verifying second-level security protocols},
}

Fully expanded entry:

@string{LNCS = "Lecture Notes in Computer Science"}
@inproceedings{BLP03,
	author = {Giampaolo Bella and Cristiano Longo and L. C. Paulson},
	booktitle = "Theorem Proving in Higher Order Logics:                 13$^{th}$ International Conference, {TPHOLs} 2000",
	editor = "J. Harrison and M. Aagaard",
	key = "TPHOLs00",
	pages = {352--366},
	publisher = "Springer-Verlag",
	series = LNCS,
	title = {Verifying second-level security protocols},
	volume = 1869,
	year = 2000,
}

Blu67

@string{JACM = "Journal of the Association for Computing Machinery"}
@article{Blu67,
	author = {Blum, M.},
	journal = JACM,
	pages = {322--336},
	title = {A machine independent theory of computational complexity},
	volume = 14,
	year = 1967,
}

BLY79

@article{BLY79,
	author = {Baylor, D. A. and Lamb, T. D. and Yau, K.-W.},
	journal = {Journal of Physiology},
	pages = {613--634},
	title = {Responses of retinal rods to single photons},
	volume = 288,
	year = 1979,
}

BM01

@inproceedings{BM01,
	author = {Gilbers Baumslag and Miller, III, Charles F.},
	booktitle = {Groups and computation, {II} (New Brunswick, NJ, 1995)},
	pages = {19--30},
	publisher = {AMS},
	series = {DIMACS series in Discrete Mathematics and Theoretical Computer Science},
	title = {Experimenting and computing with infinite groups},
	volume = 28,
	year = 1997,
}

BM77

@book{BM77,
	author = {Bell, John and Moshe Machover},
	publisher = {North-Holland, New York},
	title = {A Course in Mathematical Logic},
	year = 1977,
}

BM79

@book{BM79,
	author = {Boyer, R. S. and J. S. Moore},
	publisher = {Academic Press, New York},
	title = {{A Computational Logic}},
	year = 1979,
}

BM81

@inproceedings{BM81,
	author = {Boyer, R. S. and J. S. Moore},
	booktitle = {The Correctness Problem in Computer Science},
	pages = {103--84},
	publisher = {Academic Press, New York},
	title = {Metafunctions: Proving Them Correct and Using Them Efficiently as New Proof Procedures},
	year = 1981,
}

BM88

@incollection{BM88,
	author = {Boyer, R. S. and J. S. Moore},
	booktitle = {Machine Intelligence II},
	publisher = {Oxford Universtiy Press},
	title = {Integrating Recursive Procedures into Hueristic Theorem Provers:  A Case Study in Linear Arithmetic},
	year = 1988,
}

BM88a

@book{BM88a,
	author = {Boyer, R. S. and J. S. Moore},
	publisher = {Academic Press},
	title = {A Computational Logic Handbook},
	year = 1988,
}

BM88b

@incollection{BM88b,
	author = {Boyer, Robert S. and J. Strother Moore},
	booktitle = {Machine Intelligence},
	editor = {J. E. Hayes and D. Michie and J. Richards},
	pages = {83--124},
	publisher = {Clarendon Press},
	title = {Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study with Linear Arithmetic},
	volume = 11,
	year = 1988,
}

BM88c

@article{BM88c,
	author = {Baumslag, Gilbert and Miller, III, Charles F.},
	issn = {0024-6093},
	journal = {The Bulletin of the London Mathematical Society},
	number = 3,
	pages = {239--244},
	title = {Some odd finitely presented groups},
	volume = 20,
	year = 1988,
}

BM90

@inproceedings{BM90,
	author = {Burstall, R. M. and J. McKinna},
	booktitle = {Draft Proceedings of 1st Workshop on Logical Frameworks},
	organization = {Sophia Antipolis, France},
	title = {Deliverables: An approach to program development in the Calculus of Constructions},
	year = 1990,
}

BM92

@string{Jan = "January"}
@article{BM92,
	author = {Kim Bruce and John Mitchell},
	journal = {Proceedings of the Nineteenth {ACM} Symposium on Principles of Programming Languages},
	month = Jan,
	pages = {316--327},
	title = {{PER} models of subtyping, recursive types and higher--order polymorphism},
	year = 1992,
}

BMP03

@article{BMP03,
	author = {G. Bella and F. Massacci and L. C. Paulson},
	journal = {IEEE J. of Selected Areas in Communications},
	number = 1,
	pages = {77--87},
	title = {Verifying the {SET} registration protocols},
	volume = 21,
	year = 2003,
}

BMS94

@article{BMS94,
	author = {Baumslag, Gilbert and Miller, III, Charles F. and Short, Hamish},
	issn = {0024-6093},
	journal = {The Bulletin of the London Mathematical Society},
	number = 1,
	pages = {97--101},
	title = {Unsolvable problems about small cancellation and word hyperbolic groups},
	volume = 26,
	year = 1994,
}

BN02

@string{LNCS = "Lecture Notes in Computer Science"}
@inproceedings{BN02,
	author = {Berghofer, Stefan and Tobias Nipkow},
	booktitle = {Types for Proofs and Programs: {TYPES}'2000},
	editor = {Callaghan, P. and Z. Luo and J McKinna and R. Pollack},
	publisher = {Springer-Verlag},
	series = LNCS,
	title = {Executing higher order logic},
	volume = 2277,
	year = 2002,
}

BNS00

@string{APAL = "Annals of Pure and Applied Logic"}
@article{BNS00,
	author = {Bellantoni, Stephen J. and Karl-Heinz Niggl and Helmut Schwichtenberg},
	journal = APAL,
	number = {1--3},
	pages = {17--30},
	title = {Higher type recursion, ramification and polynomial time},
	volume = 104,
	year = 2000,
}

BO83

@inproceedings{BO83,
	author = {Michael Ben-Or},
	booktitle = {Annual ACM Symposium on Principles of Distributed Computing},
	pages = {27--30},
	publisher = {ACM Press, NY},
	title = {Another Advantage of Free Choice: Completely Asynchronous Agreement Protocols},
	year = 1983,
}

Boe85

@string{Oct = "October"}
@inproceedings{Boe85,
	author = {Boehm, Hans J.},
	booktitle = {Annual Symposium on Foundations in Computer Science},
	month = Oct,
	pages = {339--345},
	title = {Partial Polymorphic Type Inference is Undecidable},
	year = 1985,
}

book

@book{book,
	address = {NJ},
	author = {