@comment{Bibliographic database for BibTeX 0.99c}

@string{sicomp="{SIAM} Journal on Computing"}
@string{polymorphism="Polymorphism: The {ML}/{LCF}/{HOPE} Newsletter"}
@string{tcs="Theoretical Computer Science"}
@string{jcss="Journal of Computer and System Sciences"}
@string{cacm="Communications of the {ACM}"}
@string{toplas="{ACM} Transactions on Programming Languages and Systems"}
@string{jacm="Journal of the {ACM}"}
@string{jsl="Journal of Symbolic Logic"}
@string{zml="Zeitschrift {f\"ur} Mathematische Logik und Grundlagen der Mathematik"}
@string{icold="Information and Control"}
@string{ic="Information and Computation"}
@string{aml="Annals of Mathematical Logic"}
@string{apal="Annals of Pure and Applied Logic"}
@string{jar="Journal of Automated Reasoning"}
@string{jsc="Journal of Symbolic Computation"}
@string{cs="Computing Surveys"}
@string{ipl="Information Processing Letters"}
@string{jlp="Journal of Logic Programming"}
@string{scp="Science of Computer Programming"}
@string{ai="Acta Informatica"}
@string{lasc="{LISP} and Symbolic Computation"}

@string{lncs="Lecture Notes in Computer Science"}
@string{lnm="Lectures Notes in Mathematics"}

@string{popl=" {ACM} Symposium on Principles of Programming Languages"}
@string{lics=" Symposium on Logic in Computer Science"}
@string{cade=" Conference on Automated Deduction"}
@string{lofp="Logics of Programs"}
@string{lispandfp=" Symposium on {LISP} and Functional Programming"}
@string{fpca=" Conference on Functional Programming and Computer Architecture"}
@string{stoc=" Symposium on the Theory of Computing"}
@string{focs=" Symposium on the Foundations of Computer Science"}
@string{icalp=" International Colloquium on Automata, Languages, and Programming"}

@string{springer="Springer-Verlag"}
@string{nh="North-Holland"}
@string{ph="Prentice-Hall"}
@string{aw="Addison-Wesley"}
@string{ap="Academic Press"}

@string{first="First"}
@string{second="Second"}
@string{third="Third"}
@string{fourth="Fourth"}
@string{fifth="Fifth"}
@string{sixth="Sixth"}
@string{seventh="Seventh"}
@string{eighth="Eighth"}
@string{ninth="Ninth"}
@string{tenth="Tenth"}
@string{eleventh="Eleventh"}
@string{twelfth="Twelfth"}
@string{thirteenth="Thirteenth"}
@string{fourteenth="Fourteenth"}
@string{fifteenth="Fifteenth"}
@string{sixteenth="Sixteenth"}
@string{seventeenth="Seventeenth"}
@string{eighteenth="Eighteenth"}
@string{nineteenth="Nineteenth"}
@string{twentieth="Twentieth"}

@string{constable="Robert L. Constable"}

@string{lfcs="Laboratory for the Foundations of Computer Science, Edinburgh University"}
@string{cmu="School of Computer Science, Carnegie Mellon University"}

@comment{*A*}

@InCollection{abramsky90,
  crossref =	"turner90",
  author = 	 "Samson Abramsky",
  title = 	 "The Lazy Lambda Calculus",
  chapter = 	 4,
  pages = 	 "65--116"
}

@Article{andrews71,
  author = 	"Peter B. Andrews",
  title = 	"Resolution in Type Theory",
  journal = 	jsl,
  year = 	"1971",
  volume = 	"36",
  pages = 	"414--432"
}



@Article{appel89,
  author = 	 "Andrew W. Appel",
  title = 	 "Run-time Tags Aren't Necessary",
  journal = 	 lasc,
  year = 	 1989,
  volume = 	 2,
  pages = 	 "153--162"
}


@inproceedings{appel91,
title = "{S}tandard {ML} of {N}ew {J}ersey",
author = "Andrew W. Appel and David B. MacQueen",
booktitle = "Third Int'l Symp. on Prog. Lang. Implementation and Logic Programming",
editor="J. Maluszynski and M. Wirsing",
publisher="Springer-Verlag",address="New York",
month = "August",
year = "1991",
pages = "1--13
}

@TechReport{appel92,
  author = 	 "Andrew W. Appel",
  title = 	 "A Critique of Standard {ML}",
  institution =  "Princeton University",
  year = 	 1992,
  number = 	 "CS--TR--364--92",
  address = 	 "Princeton, NJ",
  month = 	 "February"
}

@inproceedings{ appel+89,
author	=	"Andrew W. Appel and Trevor Jim" ,
title	=	"Continuation-passing, Closure-passing Style" ,
booktitle=	sixteenth # popl,
address = "Austin, TX",
month	=	"January" ,
year	=	"1989" ,
pages	=	"293--302"
}

@book{ arbib+75,
	author="Michael A. Arbib and Ernest G. Manes",
	title="Arrows, Structures, and Functors: The Categorical Imperative",
	publisher=ap, year=1975
}

@book{	allen78,
	author="John Allen",
	title="Anatomy of {LISP}",
	publisher="McGraw-Hill",
	year=1978
}

@book{	abelson+85,
	author="Harold Abelson and Gerald Jay Sussman",
	title="Structure and Interpretation of Computer Programs",
	publisher="MIT Press",
	year="1985"
}

@book{	aho+74,
	author="Alfred V. Aho and John E. Hopcroft and Jeffrey D. Ullman",
	title="The Design and Analysis of Computer Algorithms",
	publisher=aw,
	year="1974"
}

@book{	aho+85,
	author="Alfred V. Aho and Ravi Sethi and Jeffrey D. Ullman",
	title="Compilers: Principles, Techniques, and Tools",
	publisher=aw,
	year=1985
}

@incollection{ aczel77a,
        crossref="barwise77",
	author="Peter Aczel",
	title="Introduction to Inductive Definitions",
	pages="739--782"
}

@inproceedings{ aczel78,
        crossref="logiccolloquium77",
	author="Peter Aczel",
	title="The Type Theoretic Interpretation of Constructive Set Theory",
	pages="55--66"
}


@InCollection{ aczel80,
        crossref="kleenesymp",
	Author="Peter Aczel",
	Title="Frege Structures and the Notions of Truth, Proposition, and
Set",
	Pages="31--59"
}


@InProceedings{ aczel83,
	Author="Peter Aczel",
	Title="Frege Structures Revisited",
	BookTitle="Proceedings of the 1983 Marstrand Workshop",
	Editor="B. Nordstr{\"o}m and J. Smith",
	Year="1983"
}




@InProceedings{aczel+90,
  author = 	"Peter Aczel and David P. Carlisle",
  title = 	"The Logical Theory of Constructions: A Formal Framework and
		 its Implementation",
  crossref="lf-workshop"
}

@inproceedings{ aczel77b,
	author="Peter Aczel",
	title="The Strength of {Martin-L\"of}'s Intuitionistic Type Theory with One Universe",
	booktitle="Proceedings of the Symposium on Mathematical Logic",
	publisher="University of Helsinki Department of Philosophy",
	pages="1--32",
	year=1977
}


@inproceedings{ allen87a,
	author="Stuart Allen",
	title="A Non-Type-Theoretic Definition of {Martin-L\"of's} Types",
	booktitle=second # lics,
	address="Ithaca, New York",
	month=jun, year=1987
}

@PhDThesis{ allen87b,
	Author="Stuart Allen",
	Title="A Non-Type-Theoretic Semantics for Type-Theoretic Language",
	School="Cornell University",
	Year="1987"
}


@techreport{ avron87a,
	author="Arnon Avron",
	title="Simple Consequence Relations",
	institution=lfcs,
	month=jun, year=1987,
	number="ECS--LFCS--87--30",
	note="To appear, {\it Information and Computation}."
}

@Article{ avron91,
  author = 	"Arnon Avron",
  title = 	"Simple Consequence Relations",
  journal = 	ic,
  year = 	"1991",
  volume = 	"91",
  number = 	"1",
  pages = 	"105--139"
}

@Proceedings{avron+87b,
  title = 	"Workshop on General Logic",
  year = 	"1987",
  editor = 	"Arnon Avron and Furio Honsell and Robert Harper and Ian Mason
		 and Gordon Plotkin",
  organization = 	lfcs,
  address = 	"Edinburgh, Scotland",
  month = 	feb,
  note = 	"(Published as technical report ECS--LFCS--88--52.)"
}

@InProceedings{ avron87b,
	Author="Arnon Avron",
	Title="Representing Modal Logic in {LF}",
	Organization=lfcs,
	BookTitle="Workshop on General Logic",
	Editor="A. Avron and R. Harper and F. Honsell and I. Mason and G. Plotkin",
	Address="Edinburgh, Scotland",
	Month=feb,
	Year="1987",
	Note="(Published as technical report ECS--LFCS--88--52.)"
}

@techreport{ avron+87,
        author="Arnon Avron and Furio Honsell and Ian A. Mason and
	 Robert Pollack",
	title="Using Typed Lambda Calculus to Implement Formal Systems
		 on a Machine",
	institution=lfcs,
	month=jun,
        year=1987,
	number="ECS--LFCS--87--31",
	note="To appear, {\it Journal of Automated Reasoning}."
}

@InCollection{avron+89,
  author = 	"Arnon Avron and Furio Honsell and Ian A. Mason",
  title = 	"An Overview of the {E}dinburgh Logical Framework",
  booktitle = 	"Current Trends in Hardware Verification and Automated
		 Theorem Proving",
  publisher = 	"Springer-Verlag",
  year = 	"1989",
  editor = 	"G. Birtwistle and P. A. Subramanyam",
  pages = 	"323--240"
}

@comment{*B*}

@inproceedings{ beierle+85,
	author="C. Beierle and A. Voss",
	title="Implementation Specifications",
	booktitle="Recent Trends in Data Type Specification",
	editor="H.-J. Kreowski",
	volume=116,
	series="Informatik Fachberichte",
	pages="39--53",
	year=1985,
	publisher=springer
}


@book{ bishop67,
	author="Errett Bishop",
	title="Foundations of Constructive Analysis",
	publisher="McGraw-Hill",
	year=1967,
	note="No longer in print.  Bishop and {Bridges~\cite{bishop+85}} is a
revised and expanded edition."
}

@book{ bishop+85,
	author="Errett Bishop and Douglas Bridges",
	title="Constructive Analysis",
	publisher=springer,
	year=1985
}

@book{ brouwer75,
	author="L. E. J. Brouwer",
	title="Collected Works, Vol. 1",
	publisher=nh,
	year=1975,
	note="(edited by Ann S. Troelstra)"
}

@book{	barendregt84,
	author="Henk P. Barendregt",
	title="The Lambda Calculus: Its Syntax and Semantics",
	edition="revised",
	publisher=nh,
	year=1984,
	series="Studies in Logic and the Foundations of Mathematics",
	volume=103
}

@book{ barwise+85,
	editor="Jon Barwise and Solomon Feferman",
	title="Model--Theoretic Logics",
	publisher=springer,
	series="Perspectives in Mathematical Logic",
	year=1985
}

@book{	beeson85,
	author="Michael J. Beeson",
	title="Foundations of Constructive Mathematics",
	publisher=springer,
	year=1985,
	series="Ergebnisse der Mathematik und ihrer Grenzgebiete",
	volume=6
}

@book{ benacerraf+83,
	title="Philosophy of Mathematics: Selected Readings",
	editor="Paul Benacerraf and Hilary Putnam",
	publisher="Cambridge University Press",
	year=1983,
	edition=second
}

@book{	boyer+79,
	author="Robert Boyer and {J} S. Moore",
	title="A Computational Logic",
	publisher=ap,
	year=1979
}

@article{ backus78,
	author="John Backus",
	title="Can Programming Be Liberated from the von~{N}eumann Style? {A} Functional Style and Its Algebra of Programs",
	journal=cacm,
	month=aug,
	year=1978
}

@article{ barendregt+83a,
	author="Henk Barendregt and Adrian Rezus",
	title="Semantics for Classical {AUTOMATH} and Related Systems",
	journal=icold,
	year=1983,
	volume=59, pages="127--147"
}

@article{ barendregt+83b,
	author="Henk Barendregt and Mario Coppo and Mariangiola Dezani-Ciancaglini",
	title="A Filter Lambda Model and the Completeness of Type Assignment",
	journal=jsl, volume=48, number=4, year=1983
}

@phdthesis{ bates79,
	author="Joseph L. Bates",
	title="A Logic for Correct Program Development",
	school="Cornell University",
	address="Ithaca, New York",
	year=1979
}

@article{ bates+85,
	author="Joseph L. Bates and Robert L. Constable",
	title="Proofs as Programs",
	journal=toplas,
	year=1985,
	volume=7,
	number=1,
	month=jan
}

@article{ beeson82,
	author="Michael Beeson",
	title="Recursive Models for Constructive Set Theories",
	journal=aml,
	volume=23,
	year=1982,
	pages="127--178"
}

@incollection{ beeson81,
	author="Michael Beeson",
	title="Formalizing Constructive Mathematics: {W}hy and How?",
	booktitle="Constructive Mathematics",
	editor="F. Richman",
	publisher=springer,
	series=lncs,
	year=1981,
	pages="146--190"
}



@Article{ benabou85,
	Author="Jean B{\'e}nabou",
	Title="Fibered Categories and the Foundations of Na{\"\i}ve Category Theory",
	Journal=jsl,
	Volume="50",
	Number="1",
	Pages="10--37",
	Month=mar,
	Year="1985"
}


@incollection{ bishop70,
        crossref="intandpfthy",
	author="Errett Bishop",
	title="Mathematics as a Numerical Language",
	pages="53--71"
}

@incollection{ boyer+81b,
        crossref="boyer+81",
	author="Robert S. Boyer and J S. Moore",
	title="Metafunctions: Proving Them Correct and Using Them Efficiently as New Proof Procedures",
	pages="103--184"
}

@article{ bruce+87,
	author="Kim Bruce and Albert Meyer and John C. Mitchell",
	title="The Semantics of Second-Order Lambda Calculus",
	year=1987,
	journal=ic,
	note="To appear"
}

@inproceedings{ bruce+84,
        crossref="kahn+84",
	author="Kim Bruce and Albert R. Meyer",
	title="A Completeness Theorem for Second-Order Polymorphic Lambda Calculus",
	pages="131--144"
}

@inproceedings{ breazu-tannen+85,
	author="Val Breazu-Tannen and Albert R. Meyer",
	title="Lambda Calculus with Constrained Types",
	booktitle=lofp,
        publisher=springer,
        year=1985,
        pages="23--40"
}

@inproceedings{ debruijn70,
	author="Nicolas G. de Bruijn",
	title="The Mathematical Language {AUTOMATH}, Its Usage and Some of Its Extensions",
	booktitle="Symposium on Automatic Demonstration",
	editor="J. P. Seldin and J. R. Hindley",
	publisher=springer,
	series=lnm, volume=125,
	year=1970,
	pages="29--61"
}

@incollection{ debruijn80,
        crossref="curryvolume",
	author="Nicolas G. de Bruijn",
	title="A Survey of the Project {AUTOMATH}",
	pages="589--606"
}

@phdthesis{ ben-yelles79,
	author="Ch. B. Ben-Yelles",
	title="Type Assignment in the Lambda Calculus: Syntax and Semantics",
	school="University of Wales",
	address="Swansea, Wales",
	year=1979
}

@inproceedings{ burstall+84,
        crossref="kahn+84",
	author="Rod Burstall and Butler Lampson",
	title="A Kernel Language for Abstract Data Types and Modules",
	pages="1--50"
}

@inproceedings{ burstall+80a,
	author="Rod Burstall and David MacQueen and Donald Sannella",
	title="{HOPE}: {A}n Experimental Applicative Language",
	booktitle="Proceedings of the 1980 {LISP} Conference",
	publisher="Stanford University",
	address="Stanford, California",
	year=1980,
	pages="136--143"
}



@TechReport{ burstall+88,
	Author="Rod Burstall and Furio Honsell",
	Title="A Natural Deduction Treatment of Operational Semantics",
	Institution=lfcs,
        Number="ECS--LFCS--88--69",
	Month=nov,
	Year="1988"
}

@InCollection{ burstall+91,
  author = 	"Rod Burstall and Furio Honsell",
  title = 	"Operational Semantics in a Natural Deduction
		 Setting",
  crossref= "huet+91"
}

@techreport{ boehm80,
	author="Hans-J{\"u}rgen B{\"o}hm and Alan Demers and James Donahue",
	title="An Informal Description of {R}ussell",
	institution="Computer Science Department, Cornell University",
	address="Ithaca, New York",
	number="80--430",
	year=1980
}

@inproceedings{ burstall+75,
	author="Rod Burstall and John Darlington",
	title="A Transformation System for Developing Recursive Programs",
	booktitle="Proceedings of the 1975 International Conference on Reliable Software",
	year=1975,
	pages="465--472"
}

@inproceedings{ burstall+77,
	author="Rod Burstall and Joseph A. Goguen",
	title="Putting Theories Together to Make Specifications",
	booktitle="Proceedings of the 5th International Joint Conference on Artificial Intelligence",
	year=1977,
	pages="1045--1058"
}

@inproceedings{ burstall+80b,
	author="Rod Burstall and Joseph A. Goguen",
	title="The Semantics of {CLEAR}, a Specification Language",
	booktitle="Proceedings of Advanced Course on Abstract Software Specifications",
	address="Copenhagen",
	publisher=springer,
	series=lncs,
	volume=86,
	year=1980,
	pages="292--332"
}

@incollection{ burstall+81,
        crossref="boyer+81",
	author="Rod Burstall and Joseph A. Goguen",
	title="An Informal Introduction to Specifications Using {CLEAR}",
	pages="185--213"
}

@incollection{ brouwer23,
        crossref="vanheijenoort67",
	author="L. E. J. Brouwer",
	title="On the Significance of the Principle of the Excluded Middle in Mathematics, Especially in Function Theory",
	pages="334--345"
}

@comment{*C*}



@Unpublished{cooper90,
  author = 	"Eric C. Cooper",
  title = 	"An Overview of the {FOX} Project",
  note = 	"Talk at Bell Laboratories",
  year = 	1990,
  month = 	"July"
}

@InCollection{clinger+85,
  author = 	"William Clinger and Daniel P. Friedman and Mitchell Wand",
  title = 	"A Scheme for Higher-Level Semantic Algebra",
  crossref="nivat+85",
  pages="237--250"
}

@article	( coquand+88,
author	=	"Thierry Coquand and G\'{e}rard Huet" ,
title	=	"The {Calculus of Constructions}" ,
journal	=	"Information and Computation" ,
volume	=	"76" ,
number	=	"2/3" ,
month	=	"February/March" ,
year	=	"1988" ,
pages	=	"95--120"
)

@book{ church56,
	author="Alonzo Church",
	title="Introduction to Mathematical Logic",
	publisher="Princeton University Press",
	year=1956
}

@book{ church51,
	author="Alonzo Church",
	title="The Calculi of Lambda Conversion",
	publisher="Princeton University Press",
	series="Annals of Mathematical Studies",
	volume=6,
	year=1951
}

@book{ clocksin+81,
	author="William Clocksin and C. S. Mellish",
	title="Programming in {PROLOG}",
	publisher=springer,
	year=1981
}

@Unpublished{ constable+87a,
	Author="Robert L. Constable and Douglas Howe",
	Title="{NuPRL} as a Logical Framework",
	Note="(Unpublished manuscript.)"
}

@InCollection{ constable+90,
  author = 	"Robert Constable and Douglas Howe",
  title = 	"{NuPRL} as a General Logic",
  crossref =	"odifreddi90"
}


@book{	constable+82a,
	author="Robert L. Constable and Scott D. Johnson and Carl D. Eichenlaub",
	title="Introduction to the {PL/CV2} Programming Logic",
	publisher=springer,
	year=1982,
	series=lncs,
	volume=135
}

@book{	constable+78,
	author="Robert L. Constable and Michael J. O'Donnell",
	title="A Programming Logic",
	publisher="Winthrop",
	year=1978
}

@book{	constable+86,
	author="Robert L. {Constable, {\it et. al.}}",
	title="Implementing Mathematics with the {NuPRL} Proof Development System",
	publisher=ph,
	year=1986
}

@book{	curry+58,
	author="H. B. Curry and R. Feys",
	title="Combinatory Logic",
	publisher="North-Holland",
	year=1958
}

@book{	curry+72,
	author="H. B. Curry and J. R. Hindley and J. P. Seldin",
	title="Combinatory Logic, Volume 2",
	publisher="North-Holland",
	year=1972
}



@Book{ curien86,
	Author="P-L Curien",
	Title="Categorical Combinators, Sequential Algorithms and Functional Programming",
	Publisher="Pitman/Wiley",
	Series="Research Notes in Theoretical Computer Science",
	Year="1986"
}

@techreport{ chan77,
	author="Tat-Hung Chan",
	title="An Algorithm for Checking {PL/CV} Arithmetical Inferences",
	institution="Computer Science Department, Cornell University",
	address="Ithaca, New York",
	number="77--236",
	year=1977
}
	
@article{ cardelli83,
	author="Luca Cardelli",
	title="The Functional Abstract Machine",
	journal=polymorphism,
	year=1983,
	volume=1
}

@inproceedings{ cardelli84a,
        crossref="kahn+84",
	author="Luca Cardelli",
	title="A Semantics of Multiple Inheritance",
	pages="51--67"
}

@article{ cardelli+86,
	author="Luca Cardelli and Peter Wegner",
	title="On Understanding Types, Data Abstraction, and Polymorphism",
	journal=cs,
	volume=18, number=4, year=1986, month=dec
}

@article{ cardelli85,
	author="Luca Cardelli",
	title="Basic Polymorphic Type Checking",
	journal=polymorphism,
	year=1985, volume=2, number=1, month=jan
}

@inproceedings{ cardelli84b,
	author="Luca Cardelli",
	title="Compiling a Functional Language",
	booktitle="1984" # lispandfp,
	year=1984, month=aug, address="Austin, Texas"
}



@TechReport{ cardelli86,
	Author="Luca Cardelli",
	Title="A Polymorphic {$\lambda$-calculus} with {Type:Type}",
	Institution="DEC SRC",
	Year="1986"
}

@Unpublished{ cardelli87,
	Author="Luca Cardelli",
	Title="Phase Distinctions in Type Theory",
	Note="unpublished manuscript"
}



@TechReport{cardelli89,
  author = 	 "Luca Cardelli",
  title = 	 "Typeful Programming",
  institution =  "DEC SRC",
  year = 	 1989,
  number = 	 45
}

@Article{ cartmell86,
	Author="John Cartmell",
	Title="Generalised Algebraic Theories and Contextual Categories",
	Journal=apal,
	Volume="32",
	Pages="209--243",
	Year="1986"
}

@inproceedings{ cartwright82,
	author="Robert Cartwright",
	title="Toward a Logical Theory of Program Data",
	booktitle=lofp,
	year=1982,
	publisher=springer,
	series=lncs, volume=131,
	pages="37--51"
}

@article{ church40,
	author="Alonzo Church",
	title="A Formulation of the Simple Theory of Types",
	journal=jsl,
	year=1940,
	volume=5,
	pages="56--68"
}

@techreport{ clement+85,
	author="Dominique {Cl\'ement} and Jo{\"e}lle Despeyroux and Thierry Despeyroux and Laurent Hascoet and Gilles Kahn",
	title="Natural Semantics on the Computer",
	institution="INRIA",
	address="Sophia--Antipolis, France",
	number="RR 416", month=jun, year=1985
}



@InProceedings{ clement+86,
	Author="Dominique {Cl\'ement} and Jo{\"e}lle Despeyroux and Thierry Despeyroux and Gilles Kahn",
	Title="A Simple Applicative Language: {Mini-ML}",
	BookTitle="1986" # lispandfp,
	Year="1986"
}

@inproceedings{ constable71,
	author=constable,
	title="Constructive Mathematics and Automatic Program Writers",
	booktitle="Proceedings of the {IFIP} Congress",
	publisher="{IFIP}",
	address="Ljubljana",
	year=1971,
	pages="229--233"
}

@inproceedings{ constable77,
	author=constable,
	title="On the Theory of Programming Logics",
	booktitle=ninth # stoc,
	address="Boulder, Colorado",
	year=1977,
	pages="269--285"
}

@inproceedings{ constable80a,
	author=constable,
	title="Programs and Types",
	booktitle="Twenty-first" # focs,
	year=1980,
	pages="118--128"
}

@techreport{ constable80b,
	author=constable,
	title="The Fundamental Theorem of Arithmetic in {PL/CV2}",
	institution="Computer Science Department, Cornell University",
	address="Ithaca, New York",
	number="80--424",
	year=1980
}

@techreport{ constable82,
	author=constable,
	title="Intensional Analysis of Functions and Types",
	institution="Computer Science Department, University of Edinburgh",
	number="CSR--118--82",
	month=jun,
	year=1982
}

@article{ constable85a,
	author=constable,
	title="Constructive Mathematics as a Programming Logic {I}: {S}ome Principles of Theory",
	journal="Annals of Discrete Mathematics",
	volume=24,
	year=1985,
	pages="269--285"
}

@inproceedings{ constable83a,
	author=constable,
	title="Mathematics as Programming",
	booktitle=lofp,
	publisher=springer,
	series=lncs,
	volume=164,
	year=1983
}

@inproceedings{ constable83b,
	author=constable,
	title="Partial Functions in Constructive Formal Theories",
	booktitle="Proceedings of the 6th G.I. Conference",
	publisher=springer,
	series=lncs,
	volume=45,
	year=1983
}

@article{ constable85b,
	author=constable,
	title="Programs as Proofs",
	journal=ipl,
	volume=16,
	number=3,
	year=1985,
	pages="21--38"
}

@inproceedings{ cousineau+85,
	author="Guy Cousineau and Pierre-Louis Curien and Michel Mauny",
        title="The Categorical Abstract Machine",
	booktitle="1985" # fpca,
	editor="J. P. Jouannaud",
	publisher=springer,
	series=lncs,
	volume="201",
	year=1985
}

@inproceedings{ constable+79,
	author="Robert L. Constable and Scott D. Johnson",
	title="A {PL/CV} Precis",
	booktitle="?th" # popl,
	year=1979,
	pages="7--20"
}

@inproceedings{ constable+85a,
	author="Robert L. Constable and N. P. Mendler",
	title="Recursive Definitions in Type Theory",
	booktitle=lofp,
	publisher=springer,
	series=lncs,
	year=1985,
	pages="61--78"
}

@article{ constable+85b,
	author="Robert L. Constable and Todd Knoblock and Joseph L. Bates",
	title="Writing Programs That Construct Proofs",
	journal=jar,
	volume=1,
	number=3,
	year=1985,
	pages="285--326"
}



@InProceedings{ constable+87b,
	Author="Robert L. Constable and Scott Fraser Smith",
	Title="Partial Objects in Constructive Type Theory",
	BookTitle=second # lics,
	Pages="183--193",
	Month=jun,
	Year="1987"
}


@InProceedings{ constable+88,
	Author="Robert L. Constable and Scott Fraser Smith",
	Title="Computational Foundations of Basic Recursive Function Theory",
	BookTitle=third # lics,
	Pages="360--371",
	Month=jul,
	Year="1988"
}

@inproceedings{ constable+82b,
	author="Robert L. Constable and Daniel R. Zlatin",
	title="Report on the Type Theory {(V3)} of the Programming Logic {PL/CV3}",
	booktitle=lofp,
	publisher=springer,
	series=lncs,
	volume=131,
	year=1982
}

@article{ constable+84,
	author="Robert L. Constable and Daniel R. Zlatin",
	title="The Type Theory of {PL/CV3}",
	journal=toplas,
	volume=7,
	number=1,
	month=jan,
	year=1984,
	pages="72--93"
}



@Article{ coppo+78,
	Author="Mario Coppo and Mariangiola Dezani",
	Title="A New Type Assignment for Lambda Terms",
	Journal=zml,
	Volume="19",
	Pages="139--156",
	Year="1978"
}


@inproceedings{ coppo+80,
        crossref="curryvolume",
	author="Mario Coppo and Mariangiola Dezani-Ciancaglini and B. Venneri",
	title="Principal Type Schemes and Lambda Calculus Semantics",
	pages="535--560"
}

@inproceedings{ coppo+83,
	author="Mario Coppo and E. Giovanetti",
	title="Completeness Results for a Polymorphic Type System",
	booktitle="CAAP '83",
	editor="G. Ausiello",
	publisher=springer,
	series=lncs, volume=159,
	year=1983,
	pages="179--190"
}

@inproceedings{ coppo+86,
	author="Mario Coppo and M. Zacchi",
	title="Type Inference and Logical Relations",
	booktitle=lics,
	address="Boston",
	month=jun, year=1986,
	pages="218--226"
}

@inproceedings{ coquand+85,
	author="Thierry Coquand and {G\'erard} Huet",
	title="Constructions: A Higher-Order Proof System for Mechanizing Mathematics",
	booktitle="{EUROCAL '85}: European Conference on Computer Algebra",
	publisher=springer, series=lncs,
	volume=203, year=1985, pages="151--184",
	editor="B. Buchberger"
}

@phdthesis{ coquand85,
	author="Thierry Coquand",
	title="Une Th\'eorie des Constructions",
	school="Universit\'e Paris VII",
	year=1985, month=jan
}

@inproceedings{ coquand86,
	author="Thierry Coquand",
	title="An Analysis of {Girard's} Paradox",
	booktitle=lics,
	address="Boston",
	month=jun, year=1986,
	pages="227--236"
}

@techreport{ coquand+89,
	author="Thierry Coquand and Gilles Dowek and G{\'e}rard Huet and
Christine {Paulin-Mohring}",
	title="The {C}alculus of {C}onstructions: {D}ocumentation and User's Guide",
	institution="Projet Formel, {INRIA-ENS}",
	month=jul,
	year="1989"
}

@InCollection{ coquand91,
  author = 	"Thierry Coquand",
  title = 	"An Algorithm for Testing Conversion in Type Theory",
  crossref="huet+91"
}


@comment{*D*}



@InProceedings{duba+91,
  author = 	 "Bruce Duba and Robert Harper and David MacQueen",
  title = 	 "Typing First-Class Continuations in {ML}",
  booktitle = eighteenth # popl,
  year = 	 1991,
  month = 	 "January"
}

@Article{dybvig+89,
  author = 	"R. Kent Dybvig and Bob Hieb",
  title = 	"Engines from Continuations",
  journal = 	"Journal of Computer Languages",
  year = 	1989,
  volume = 	14,
  number = 	2,
  pages = 	"109--124"
}



@InProceedings{despeyroux86,
  author = 	"Jo{\"e}lle Despeyroux",
  title = 	"Proof of Translation in Natural Semantics",
  booktitle = 	first # lics,
  year = 	"1986",
  pages = 	"193--205"
}

@InProceedings{ despeyroux84,
        crossref="kahn+84",
	Author="Thierry Despeyroux",
	Title="Executable Specifications of Static Semantics"
}


@book{	dijkstra76,
	author="Edsger W. Dijkstra",
	title="A Discipline of Programming",
	publisher=ph,
	year=1976
}

@book{ donahue76,
	author="James Donahue",
	title="Complementary Definitions of Programming Language Semantics",
	publisher=springer,
	series=lncs,
	volume=42,
	year=1976
}

@book{	dummett77,
	author="Michael Dummett",
	title="Elements of Intuitionism",
	publisher="Oxford University Press",
	year=1977
}

@book{ dummett73,
	author="Michael Dummett",
	title="Frege: Philosophy of Language",
	publisher="Duckworth",
	year=1973
}

@phdthesis{ vandaalen80,
	author="Diedrik T. van Daalen",
	title="The Language Theory of {AUTOMATH}",
	school="Technical University of Eindhoven",
	address="Eindhoven, Netherlands",
	year=1980
}

@phdthesis{ damas85,
	author="Luis Manuel Martins Damas",
	title="Type Assignment in Programming Languages",
	school="Edinburgh University",
	year=1985
}

@inproceedings{ damas+82,
	author="Luis Damas and Robin Milner",
	title="Principal Type Schemes for Functional Programs",
	booktitle=ninth # popl,
	year=1982,
	pages="207--212"
}

@inproceedings{ demers+80a,
	author="Alan J. Demers and James E. Donahue",
	title="Data Types, Parameters, and Type Checking",
	booktitle=seventh # popl,
	year=1980,
	pages="12--23"
}

@inproceedings{ demers+80b,
	author="Alan J. Demers and James E. Donahue",
	title="Type Completeness as a Language Principle",
	booktitle=seventh # popl,
	year=1980,
	pages="234--244"
}

@inproceedings{ demers+83,
	author="Alan J. Demers and James E. Donahue",
	title="Making Variables Abstract: An Equational Theory for {R}ussell",
	booktitle=tenth # popl,
	year=1983,
	pages="59--72"
}

@techreport{ donahue+79,
	author="James E. Donahue and Alan J. Demers",
	title="Revised Report on {R}ussell",
	institution="Computer Science Department, Cornell University",
	address="Ithaca, New York",
	year=1979,
	number="79--389",
	month=sep
}

@article{ donahue+85,
	author="James E. Donahue and Alan J. Demers",
	title="Data Types are Values",
	journal=toplas,
	volume=7,
	number=3,
	year=1985,
	pages="426--445"
}

@article{ donahue79,
	author="James E. Donahue",
	title="On the Semantics of Data Type",
	journal=sicomp,
	volume=8,
	year=1979,
	pages="546--560"
}

@inproceedings{ dummett75,
        crossref="logiccolloquium73",
	author="Michael Dummett",
	title="The Philosophical Basis of Intuitionistic Logic"
}

@comment{*E*}



@InProceedings{evans68,
  author = 	"Arthur Evans",
  title = 	"{PAL} -- A Language Designed for Teaching Programming
		 Linguistics",
  booktitle = 	"Proc. {ACM} 23rd National Conference",
  year = 	1968,
  pages = 	"395--403",
  organization = 	"{ACM}",
  publisher = 	"Brandin Systems Press",
  address = 	"Princeton"
}

@inproceedings{ elliott89,
	author="Conal Elliott",
	title="Higher-order Unification with Dependent Function Types",
	year=1989, month=apr,
	address="Chapel Hill, NC",
	booktitle="Proceedings of the Third International Conference
		 on Rewriting Techniques and Applications",
	publisher = springer,
	series=lncs,
	volume=355,
	editor="N. Dershowitz",
	pages="121--136"
}

@PhdThesis{elliott90,
  author = 	"Conal Elliott",
  title = 	"Extensions and Applications of Higher-Order Unification",
  school = 	cmu,
  year = 	"1990",
  month = 	"May"
}



@book{ ehrig+85,
	author="Hartmut Ehrig and Bernd Mahr",
	title="Fundamentals of Algebraic Specification 1: Equations and Initial
		Semantics",
	publisher=springer,
	year=1985
}


@InProceedings{ erhard88,
	Author="Thomas Erhard",
	Title="A Categorical Semantics of {C}onstructions",
	BookTitle=third # lics,
	Address="Edinburgh",
	Pages="264--273",
	Month=jul,
	Year="1988"
}


@comment{*F*}

@InProceedings{feferman89,
  author = 	"Solomon Feferman",
  title = 	"Finitary Inductively Presented Logics",
  pages = 	"191--220",
  crossref = "logiccolloquium88"
}

@unpublished	( felty+88,
author	=	"Amy Felty and Dale Miller" ,
title	=	"A Metalanguage for Type Checking and Inference" ,
month	=	"November" ,
year	=	"1988" ,
note	=	"Manuscript" 
)

@phdthesis	( felty89,
author	=	"Amy Felty" ,
title	=	"Specifying and Implementing Theorem Provers in a
Higher-Order Logic Programming Language" ,
school	=	"Department of Computer and Information Science,
University of Pennsylvania" ,
month	=	"July" ,
year	=	"1989"
)



@TechReport{felleisen85,
  author = 	{Matthias Felleisen},
  title = 	{Transliterating {P}rolog into {S}cheme},
  institution =	{Indiana University Computer Science Department},
  year = 	{1985},
  number = 	{182}
}

@PhdThesis{felleisen87,
  author = 	"Matthias Felleisen",
  title = 	"The Calculi of {$\lambda_v$-CS} Conversion: A Syntactic
		 Theory of Control and State in Imperative Higher-Order
		 Programming Languages",
  school = 	"Indiana University",
  year = 	"1987",
  address = 	"Bloomington, IN",
  OPTnote = 	"(Available as technical report no. 226.)"
}

@InCollection{felleisen+86a,
  author = 	"Matthias Felleisen and Daniel Friedman",
  title = 	"Control Operators, the {SECD} Machine, and the
		 {$\lambda$}-Calculus",
  booktitle = 	"Formal Description of Programming Concepts {III}",
  publisher = 	"North-Holland",
  year = 	"1986"
}

@InProceedings{felleisen+86b,
  author = 	"Matthias Felleisen and Daniel Friedman and Eugene Kohlbecker
		 and Bruce Duba",
  title = 	"Reasoning with Continuations",
  booktitle = 	first # lics,
  year = 	"1986",
  organization = 	"{IEEE}",
  month = 	"June"
}

@Article{felleisen+87,
  author = 	"Matthias Felleisen and Daniel Friedman and Eugene Kohlbecker
		 and Bruce Duba",
  title = 	"A Syntactic Theory of Sequential Control",
  journal = 	tcs,
  year = 	"1987",
  volume = 	"52",
  number = 	"3",
  pages = 	"205--237"
}



@InProceedings{felleisen+88,
  author = 	{Matthias Felleisen},
  title = 	{The Theory and Practice of First-Class Prompts},
  booktitle = 	fifteenth # popl,
  year = 	{1988},
  pages = 	{180--190},
  organization = 	{ACM},
  address = 	{San Diego, CA}
}

@InProceedings{filinski89b,
  author = 	"Andrzej Filinski",
  title = 	"Declarative Continuations: An Investigation of Duality in
		 Programming Language Semantics",
  booktitle = 	"Summer Conference on Category Theory and Computer Science",
  year = 	"1989",
  publisher = 	"Springer-Verlag",
  series=lncs,
  volume="389",
  address = 	"Manchester, {UK}"
}

@MastersThesis{filinski89a,
  author = 	"Andrzej Filinski",
  title = 	"Declarative Continuations and Categorical Duality",
  school = 	"University of Copenhagen",
  year = 	"1989",
  address = 	"Copenhagen, Denmark",
  month = 	"August",
  note = 	"({DIKU} Report 89/11)"
}

@Unpublished{ farres87,
	Author="Jordi Farres",
	Title="On the Representation of {Z} in {LF}",
	Note="(Unpublished manuscript.)"
}

@InProceedings{ fiadeiro+87,
	Author="Jos{\'e} Fiadeiro and Amilcar Sernadas",
	Title="Structuring Theories on Consequence",
	BookTitle="Proc. of the Fifth Workshop on Specification of Abstract Data Types",
	Editor="Donald Sannella and Andrzej Tarlecki",
	Address="Gullane",
	Month=sep,
	Year="1987"
}


@book{	fitting83,
	author="Melvin Fitting",
	title="Proof Methods for Modal and Intuitionistic Logics",
	publisher="D. Reidel",
	year=1983
}

@techreport{ fairbairn82,
	author="Jon Fairbairn",
	title="Ponder and its Type System",
	institution="Computing Laboratory, University of Cambridge",
	number="31",
	year=1982,
	note="Reprinted in volume 1 number 2 of {\it Polymorphism: The {ML}/{LCF}/{HOPE} Newsletter}, (1983)"
}

@article{ fortune+83,
	author="Steven Fortune and Daniel Leivant and Michael O'Donnell",
	title="The Expressiveness of Simple and Second Order Type Structures",
	journal=jacm,
	volume=30,
	year=1983,
	pages="151--185"
}

@techreport{ formel87a,
	author="Projet Formel",
	title="The {CAML} Primer",
	institution="INRIA--ENS",
	month=may,
	year=1987
}

@techreport{ formel87b,
	author="Projet Formel",
	title="{CAML}: The Reference Manual",
	institution="INRIA--ENS",
	month=jun,
	year=1987
}

@incollection{ frege67,
        crossref="vanheijenoort67",
	author="Gottlob Frege",
	title="{\it Begriffschrifft}, a formula language, modeled upon that for arithmetic, for pure thought",
	pages="1--82"
}

@inproceedings{ freyd+87,
	author="Peter Freyd and Andre Scedrov",
	title="Some Semantic Aspects of Polymorphic Lambda Calculus",
	booktitle=second # lics,
	address="Ithaca, New York",
	month=jun, year=1987,
	pages="315--319"
}



@InCollection{friedman+85,
  author = 	{Daniel P. Friedman and Christopher T. Haynes and Eugene
		Kohlbecker},
  title = 	{Programming with Continuations},
  booktitle = 	{Program Transformations and Programming Environments},
  publisher = 	springer,
  year = 	{1985},
  editor = 	{P. Pepper},
  pages = 	{263--274}
}

@inproceedings{ friedman75,
        crossref="logiccolloquium75",
	author="Harvey Friedman",
	title="Equality Between Functionals",
        pages="22--37"
}

@comment{*G*}

@Misc{griffin92,
  author = 	 "Timothy Griffin",
  howpublished = "Private communication.",
  year = 	 1992,
  month = 	 "January"
}

@article{ goguen+84b,
	author="Joseph A. Goguen and Rod Burstall",
	title="Some Fundamental Algebraic Tools for the Semantics of
Computation.  {P}art {I}: {C}omma Categories, Colimits, Structures, and
Theories.",
	journal=tcs,
	volume=31,
	year=1894,
	pages="175--209"
}

@incollection{ goguen71,
	author="Joseph A. Goguen",
	title="Mathematical Representation of Hierarchically Organized
Systems",
	booktitle="Global Systems Dynamics",
	editor="E. Attinger",
	pages="112--128",
	publisher="S. Karger",
	year=1971
}


@article{ goguen+81,
	author="Joseph A. Goguen and Jos{\'e} Meseguer",
	title="Completeness of Many-Sorted Equational Logic",
	journal="SIGPLAN Notices",
	volume=16,
	pages="24--32",
	year=1981
}

@inproceedings{ goguen+86,
	author="Joseph A. Goguen and Rod Burstall",
	title="A Study in the Foundations of Programming Methodology:
Specifications, Institutions, Charters and Parchments",
	booktitle="Proc. Workshop on Category Theory and Computer Programming",
	address="Guildford",
	Publisher=springer,
	Volume=240,
	Series=lncs,
	pages="313--333",
	year=1986
}

@InProceedings{ giannini+88,
	Author="Paola Giannini and Simona Ronchi della Rocca",
	Title="Characterization of Typings in Polymorphic Type Discipline",
	BookTitle=third # lics,
	Pages="61--71",
	Month=jul,
	Year="1988"
}


@book{ goldblatt79,
	author="Robert Goldblatt",
	title="Topoi: The Categorial Analysis of Logic",
	publisher=nh,
	year=1979
}

@book{ gentzen69a,
	editor="M. E. Szabo",
	title="The Collected Works of Gerhard Gentzen",
	publisher=nh,
	year=1969
}

@book{ gabbay81,
	author="Dov Gabbay",
	title="Semantical Investigations in Heyting's Intuitionistic Logic",
	publisher="D. Reidel",
	year=1981
}

@phdthesis{ girard72,
	author="Jean--Yves Girard",
	title="Interpr{\`e}tation Fonctionelle et {\'E}limination des Coupures dans {l'A}rithm{\`e}tique {d'Ordre} Sup{\'e}rieure",
	school="Universit{\'e} Paris {VII}",
	year=1972
}

@book{	gordon+79,
	author="Michael Gordon and Robin Milner and Christopher Wadsworth",
	title="{E}dinburgh {LCF}: A Mechanized Logic of Computation",
	publisher=springer,
	year=1979,
	series=lncs,
	volume=78
}

@book{ goodstein57,
	author="R. L. Goodstein",
	title="Recursive Number Theory",
	publisher=nh,
	year=1957
}

@book{	gries81,
	author="David Gries",
	title="The Science of Programming",
	publisher=springer,
	year=1981
}

@incollection{ gentzen69b,
	author="Gerhard Gentzen",
	title="Investigations into Logical Deduction",
	booktitle="The Collected Works of Gerhard Gentzen",
	editor="M. E. Szabo",
	publisher=nh,
	year=1969
}

@inproceedings{ girard71,
        crossref="secondscand",
	author="Jean--Yves Girard",
	title="Une Extension de l'Interpretation de {G\"o}del {\`a} l'Analyse, et son Application {\`a} l'{\'E}limination des Coupures dans l'Analyse et la Th{\'e}orie des types",
	pages="63--92"
}

@inproceedings{ goguen+84a,
	author="Joseph Goguen and Rod Burstall",
	title="Introducing {I}nstitutions",
	booktitle=lofp,
	editor="E. Clarke and D. Kozen",
	publisher=springer,
	series=lncs,
	year=1984,
	volume=164,
	pages="221--256"
}

@incollection{ goguen+78,
	author="Joseph A. Goguen and James W. Thatcher and Eric G. Wagner",
	title="Initial Algebra Approach to the Specification, Correctness, and Implementation of Abstract Data Types",
	booktitle="Current Trends in Programming Methodology, Volume IV",
	editor="Raymond Yeh",
	publisher=ph,
	year=1978
}

@techreport{ griffin87,
        author="Timothy Griffin",
	title="An Environment for Formal Systems",
	month=jun, year=1987,
	number="87--846",
	institution="Cornell University",
	address="Ithaca, New York"
}



@InProceedings{ griffin88,
	Author="Timothy Griffin",
	Title="Notational Definition --- A Formal Account",
	BookTitle=third # lics,
	Address="Edinburgh",
	Pages="372--383",
	Month=jul,
	Year="1988"
}


@InProceedings{ griffin90,
  author = 	"Timothy Griffin",
  title = 	"A Formulas-as-Types Notion of Control",
  booktitle = 	seventeenth # popl,
  year = 	"1990",
  organization ="{ACM}",
  publisher = 	"{ACM}",
  address = 	"San Francisco, CA",
  month = 	"January"
}

@comment{*H*}

@Misc{harper+91,
  author = 	 "Robert Harper and Mark Lillibridge",
  howpublished = "Announcement on the {\tt types} electronic forum.",
  year = "1991",
  month = "July"
}

@Unpublished{harper+92a,
  author = 	 "Robert Harper and Bruce Duba and David MacQueen",
  title = 	 "Typing First-Class Continuations in {ML}",
  note = 	 "Revised and expanded version of~\cite{duba+91}, in preparation."
}

@Unpublished{harper+92b,
  author = 	 "Robert Harper and Mark Lillibridge",
  title = 	 "Polymorphic Type Assignment and CPS Conversion",
  note = 	 "(Submitted for publication to the 1992 SIGPLAN Continuations
		  Workshop)",
  year = 	 1992,
  month = 	 "February"
}

@unpublished	( huet86,
author	=	"G\'{e}rard Huet" ,
title	=	"Formal Structures for Computation and Deduction" ,
month	=	"May" ,
year	=	"1986" ,
note	=	"Lecture notes for a graduate course at Carnegie
Mellon University" 
)

@inproceedings	( hannan+88,
author	=	"John Hannan and Dale Miller" ,
title	=	"Uses of Higher-Order Unification for Implementing
Program Transformers" ,
booktitle=	"Logic Programming: Proceedings of the Fifth
International Conference and Symposium, Volume 2" ,
publisher=	"MIT Press" ,
month	=	"August" ,
year	=	"1988" ,
editor	=	"Robert A. Kowalski and Kenneth A. Bowen" ,
address	=	"Cambridge, Massachusetts" ,
pages	=	"942--959" 
)

@inproceedings	( hannan88+b,
author	=	"John Hannan and Dale Miller" ,
title	=	"Enriching a Meta-Language with Higher-Order
Features" ,
booktitle=	"Proceedings of the Workshop on Meta-Programming in
Logic Programming" ,
publisher=	"University of Bristol" ,
address	=	"Bristol, England" ,
month	=	"June" ,
year	=	"1988" ,
editor	=	"John Lloyd" 
)

@techreport	( hannan89,
author	=	"John J. Hannan" ,
title	=	"Proof-theoretic Methods for Analysis of Functional
Programs" ,
institution=	"University of Pennsylvania" ,
address	=	"Philadelphia" ,
number	=	"MS-CIS-89-07" ,
month	=	"January" ,
year	=	"1989" ,
note	=	"Dissertation Proposal" 
)

@InProceedings{hagino87,
  author = 	"Tatsuya Hagino",
  title = 	"A Typed Lambda Calculus with Categorical Type Constructors",
  booktitle = 	"Summer Conference on Category Theory and Computer Science",
  year = 	1987,
  editor = 	"David Pitt and Axel Poigne and David Rydeheard"
}



@Article{haynes+86,
  author = 	"Christopher T. Haynes and Daniel P. Friedman and Mitchell
		 Wand",
  title = 	"Obtaining Coroutines from Continuations",
  journal = 	"Journal of Computer Languages",
  year = 	1986,
  volume = 	11,
  pages = 	"143--153"
}



@Article{haynes+87a,
  author = 	{Christopher T. Haynes and Daniel P. Friedman},
  title = 	{Embedding Continuations in Procedural Objects},
  journal = 	toplas,
  year = 	{1987},
  volume = 	{9},
  pages = 	{582--598}
}



@Article{haynes+87b,
  author = 	{Christopher T. Haynes and Daniel P. Friedman},
  title = 	{Abstracting Timed Preemption with Engines},
  journal = 	{Journal of Computer Languages},
  year = 	{1987},
  volume = 	{12},
  pages = 	{109--121}
}



@Article{haynes87,
  author = 	{Christopher T. Haynes},
  title = 	{Logic Continuations},
  journal = 	{Journal of Logic Programming},
  year = 	{1987},
  volume = 	{4},
  pages = 	{157--176}
}

@book{ hayashi+88,
	author="Susumu Hayashi and Hiroshi Nakano",
	title="{PX}: {A} Computational Logic",
	publisher="The MIT Press",
	series="Foundations of Computing Series",
	year=1988
}

@Book{ hindley+86,
	Author="J. Roger Hindley and Jonathan P. Seldin",
	Title="Introduction to Combinators and $\lambda$-Calculus",
	Publisher="Cambridge University Press",
	Series="London Mathematical Society Student Texts",
	Volume="1",
	Year="1986"
}

@book{	hindley+72,
	author="J. Roger Hindley and Bruce Lercher and Jonathan P. Seldin",
	title="Introduction to Combinatory Logic",
	publisher="Cambridge University Press",
	year=1972,
	series="London Mathematical Society Lecture Note Series",
	volume=7
}

@book{ herrlich+73,
	author="Horst Herrlich and George E. Strecker",
	title="Category Theory",
	publisher="Allyn and Bacon",
	year=1973
}

@book{	heyting56,
	author="Arend Heyting",
	title="Intuitionism: An Introduction",
	publisher=nh,
	year=1956
}

@inproceedings{ hanna+86,
	author="F. K. Hanna and N. Daeche",
	title="Purely Functional Implementation of a Logic",
	booktitle=eighth # cade,
	editor="J{\"o}rg H. Siekmann",
	year=1986,
	publisher=springer, series=lncs, volume=230
}

@article{ henkin50,
	author="Leon Henkin",
	title="Completeness in the Theory of Types",
	journal=jsl,
	volume=15,
	year=1950,
	pages="81--91"
}

@article{ hindley69,
	author="J. Roger Hindley",
	title="The Principal Type Scheme of an Object in Combinatory Logic",
	journal="Transactions of the American Mathematical Society",
	volume=146,
	year=1969,
	pages="29--40"
}

@article{ hindley83,
	author="J. Roger Hindley",
	title="The Completeness Theorem for Typing {$\lambda$} Terms",
	journal=tcs,
	volume=22,
	year=1983,
	pages="127--134"
}



@Article{ hindley+80,
	Author="J. Roger Hindley and Giuseppe Longo",
	Title="Lambda Calculus Models and Extensionality",
	Journal=zml,
	Volume="26",
	Pages="289--310",
	Year="1980"
}


@phdthesis{ harper85,
	author="Robert Harper",
	title="Aspects of the Implementation of Type Theory",
	school="Cornell University",
	address="Ithaca, New York",
	year=1985
}

@inproceedings{ harper86a,
	author="Robert Harper",
	title="Modules and Persistence in {S}tandard {ML}",
	booktitle="Proceedings of the Appin Workshop on Abstract Types and Persistence",
	year=1986,
	editor="Malcolm Atkinson and Ron Morrison",
	publisher=springer
}

@techreport{ harper86b,
	author="Robert Harper",
	title="Introduction to {S}tandard {ML}",
	institution=lfcs,
	number="ECS--LFCS--86--14",
	month=sep, year=1986
}



@Unpublished{ harper87,
	Author="Robert Harper",
	Title="The {D}amas-{M}ilner Type Assignment System in {LF}",
	Note="(Unpublished manuscript.)"
}

@Unpublished{ harper86c,
	Author="Robert Harper",
	Title="{Martin-L\"of's} Type Theory in {LF}",
	Note="(Unpublished manuscript.)"
}

@Unpublished{ harper86d,
	Author="Robert Harper",
	Title="The Relationship between {Martin-L\"of's} Categories and {LF}",
	Note="(Unpublished manuscript.)"
}

@inproceedings{ harper+87a,
	author="Robert Harper and Furio Honsell and Gordon Plotkin",
	title="A Framework for Defining Logics",
	booktitle=second # lics,
	address="Ithaca, New York",
	year=1987, month=jun,
	pages="194--204"
}

@inproceedings{ harper+87b,
	author="Robert Harper and Robin Milner and Mads Tofte",
	title="A Type Discipline for Program Modules",
	booktitle="{TAPSOFT '87}",
	publisher=springer, series=lncs,
	volume=250, month=mar, year=1987
}

@techreport{ harper+87c,
	author="Robert Harper and Robin Milner and Mads Tofte",
	title="The Semantics of {Standard ML}",
	institution=lfcs,
	number="ECS--LFCS--87--36",
	month=aug, year=1987
}



@TechReport{ harper+88,
	Author="Robert Harper and Robin Milner and Mads Tofte",
	Title="The Definition of {Standard ML} (Version 2)",
	Institution=lfcs,
	Number="ECS--LFCS--88--62",
	Month=aug,
	Year="1988"
}

@TechReport{ harper88a,
	Author="Robert Harper",
	Title="Constructing Type Systems over an Operational Semantics",
	Institution=lfcs,
	Number="ECS--LFCS--88--59",
	Month=jul,
	Year="1988"
}

@TechReport{ harper88b,
	Author="Robert Harper",
	Title="An Equational Formulation of {LF}",
	Institution=lfcs,
	Number="ECS--LFCS--88--67",
	Month=oct,
	Year="1988"
}

@InProceedings{ mitchell+88,
	Author="John Mitchell and Robert Harper",
	Title="The Essence of {ML}",
	BookTitle=fifteenth # popl,
	Address="San Diego, California",
	Month=jan,
	Year="1988"
}



@InProceedings{ harper+89a,
	Author="Robert Harper and Randy Pollack",
	Title="Type Checking, Universe Polymorphism, and Typical Ambiguity in
	the {C}alculus of {C}onstructions",
	BookTitle="TAPSOFT '89",
	Address="Barcelona, Spain",
	month=mar,
	year=1989
}


@InProceedings{ harper+89b,
	Author="Robert Harper and Donald Sannella and Andrzej Tarlecki",
	Title="Structure and Representation in {LF}",
	BookTitle=fourth # lics,
	Address="Asilomar, California",
	Month=jun,
	Year=1989
}

@Unpublished{ harper+89c,
	Author="Robert Harper and John C. Mitchell and Eugenio Moggi",
	Title="Higher-Order Modules and the Phase Distinction",
	Year=1989,
	Note="(To appear POPL '90)"
}

@TechReport{ harper+89d,
	Author="Robert Harper and Donald T. Sannella and Andrzej Tarlecki",
	Title="Logic Representation",
	Institution=cmu,
	Number="CMU--CS--89--175",
	Month=jul,
	Year=1989,
	Note="To appear: Third Biennial Summer Conference on Category Theory
and Computer Science"
}

@TechReport{ harper+89e,
	Author="Robert Harper and Furio Honsell and Gordon Plotkin",
	Title="A Framework for Defining Logics",
	Institution=cmu,
	Number="CMU--CS--89--173",
	Month=jan,
	Year=1989,
	Note="Revised and expanded version of~\cite{harper+87a}, submitted for
publication."
}

@TechReport{ harper+89f,
	Author="Robert Harper and Robin Milner and Mads Tofte",
	Title="The Definition of {Standard ML} (Version 3)",
	Institution=lfcs,
	Number="ECS--LFCS--89--81",
	Month=may,
	Year="1989"
}

@TechReport{ harper+89g,
	Author="Robert Harper and Robert Pollack",
	Title="Type Checking with Universes",
	Institution=cmu,
	Number="CMU--CS--89--176",
	Month=aug,
	Year=1989,
	Note="Submitted for publication."
}

@TechReport{ harper+89h,
	Author="Robert Harper and Donald Sannella and Andrzej Tarlecki",
	Title="Structure and Representation in LF",
	Institution=cmu,
	Number="CMU--CS--89--174",
	Month=jul,
	Year=1989,
	Note="Expanded version of~\cite{harper+89b}"
}

@TechReport{harper90,
  author = 	"Robert Harper",
  title = 	"Systems of Polymorphic Type Assignment in {LF}",
  institution = 	cmu,
  year = 	"1990",
  number = 	"CMU--CS--90--144",
  month = 	"June"
}



@Book{milner+90,
  author = 	"Robin Milner and Mads Tofte and Robert Harper",
  title = 	"The Definition of Standard ML",
  publisher = 	"MIT Press",
  year = 	"1990"
}

@Unpublished{ honsell86,
	Author="Furio Honsell",
	Title="{LF} in {LF}",
	Note="(Unpublished manuscript.)"
}

@article{ hoare69,
	author="C. A. R. Hoare",
	title="An Axiomatic Basis for Computer Programming",
	journal=cacm,
	volume=12,
	year=1969,
	pages="576--581"
}

@article{ hoare75,
	author="C. A. R. Hoare",
	title="Recursive Data Structures",
	journal="International Journal of Computer and Information Sciences",
	volume=4, number=2,
	year=1975,
	month=jun,
	pages="105--132"
}

@article{ hoare82,
	author="C. A. R. Hoare",
	title="Proof of Correctness of Data Representation",
	journal=ai,
	volume=1,
	year=1972,
	pages="271--281"
}

@incollection{ hoare80,
	author="C. A. R. Hoare",
	title="Notes on Data Structuring",
	booktitle="Structured Programming",
	publisher=ap,
	year=1980,
	pages="83--174"
}

@techreport{
	hook+86,
	author="James G. Hook and Douglas Howe",
	title="Impredicative Strong Existential Equivalent to {Type:Type}",
	institution="Cornell University",
	address="Ithaca, New York",
	number="TR 86--760",
	year=1986
}



@InProceedings{ howe87,
	Author="Douglas Howe",
	Title="The Computational Behavior of {Girard's} Paradox",
	BookTitle=second # lics,
	Address="Ithaca, New York",
	Pages="205--214",
	Month=jun,
	Year="1987"
}

@incollection{ howard80,
        crossref="curryvolume",
	author="William A. Howard",
	title="The Formulas-as-Types Notion of Construction",
	pages="479--490"
}

@article{ huet75,
	author="{G\'erard} P. Huet",
	title="Unification for Typed Lambda Calculus",
	journal=tcs,
	year=1975,
	month=jun,
	volume=1,
	number=1,
	pages="27--58"
}

@article{ huet80,
	author="{G\'erard} Huet",
	title="Confluent Reductions: {A}bstract Properties and Applications to Term Rewriting Systems",
	journal=jacm,
	volume=27, number=4,
	year=1980,
	month=oct,
	pages="797--821"
}

@InProceedings{ huet88,
	Author="{G\'erard} Huet",
	Title="The Constructive Engine",
	BookTitle="ESOP {'88}",
	Year="1988",
	Note="(To appear.)"
}

@Unpublished{ huet87,
	Author="{G\'erard} Huet",
	Title="Extending the {C}alculus of {C}onstructions with {Type:Type}",
	Month=apr,
	Year=1987,
	Note="unpublished manuscript"
}

@InProceedings{ hyland+89,
	Author="J. Martin E. Hyland and Andrew M. Pitts",
	Title="The {T}heory of {C}onstructions: Categorical Semantics and Topos-Theoretic Models",
	crossref="gray+89"
}

@comment{*I*}

@comment{*J*}

@phdthesis{ jutting77,
	author="L. S. Jutting",
	title="Checking {Landau's} {{\it Grundlagen}} in the {AUTOMATH} System",
	school="Eindhoven University",
	address="Netherlands",
	year=1977
}

@phdthesis{ johnson80,
	author="Scott D. Johnson",
	title="A Computer System for Checking Proofs",
	school="Cornell University",
	address="Ithaca, New York",
	year=1980,
	note="Also available from UMI Press, New York"
}

@comment{*K*}

@book{	kleene52,
	author="Stephen C. Kleene",
	title="Introduction to Metamathematics",
	publisher="van Nostrand",
	year=1952
}

@book{	knuth73a,
	author="Donald E. Knuth",
	title="The Art of Computer Programming, Volume 1: Fundamental Algorithms",
	edition=second,
	publisher=aw,
	year=1973
}

@book{	knuth69,
	author="Donald E. Knuth",
	title="The Art of Computer Programming, Volume 2: Seminumerical Algorithms",
	publisher=aw,
	year=1969
}

@book{	knuth73b,
	author="Donald E. Knuth",
	title="The Art of Computer Programming, Volume 3: Sorting and Searching",
	publisher=aw,
	year=1973
}

@inproceedings{ knoblock+86,
	author="Todd B. Knoblock and Robert L. Constable",
	title="Formalized Metareasoning in Type Theory",
	booktitle=lics,
	address="Boston",
	year=1986,
	pages="237--248"
}


@article{ koymans82,
	author="C. P. J. Koymans",
	title="Models of the Lambda Calculus",
	journal=icold,
	volume=52, number=3, year=1982, pages="306--323"
}

@phdthesis{ kozen77,
	author="Dexter C. Kozen",
	title="Complexity of Finitely Presented Algebras",
	school="Cornell University",
	address="Ithaca, New York",
	year=1977
}

@phdthesis{ krafft81,
	author="Dean B. Krafft",
	title="{AVID}: A System for the Interactive Development of Verifiably Correct Programs",
	school="Cornell University",
	address="Ithaca, New York",
	year=1981
}

@comment{*L*}

@book{	lakatos76,
	author="Imre Lakatos",
	title="Proofs and Refutations",
	publisher="Cambridge University Press",
	year=1976
}

@book{ lambek+86,
	author="Joachim Lambek and Phillip J. Scott",
	title="Introduction to Higher Order Categorical Logic",
	publisher="Cambridge University Press",
	series="Cambridge Studies in Advanced Mathematics",
	volume=7,
	year=1986
}

@book{	loveland78,
	author="Donald W. Loveland",
	title="Automated Theorem Proving: A Logical Basis",
	publisher=nh,
	year=1978
}



@InProceedings{girard+87,
	Author="Jean-Yves Girard and Yves Lafont",
	Title="Linear Logic and Lazy Computation",
	BookTitle="{TAPSOFT '87}: Colloquium on Functional and Logic Programming and Specifications",
	Series=lncs,
	Volume=250,
	Editor="Hartmut Ehrig and Robert Kowalski and Giorgio Levi and Ugo Montanari",
	Address="Pisa, Italy",
	Pages="52--66",
	Month=mar,
	Year="1987"
}


@incollection{ lambek80,
        crossref="curryvolume",
	author="Joachim Lambek",
	title="From Lambda Calculus to Cartesian Closed Categories",
	pages="375--402"
}

@article{ landin65,
	author="Peter J. Landin",
	title="A Correspondence between {ALGOL--60} and {C}hurch's Lambda Notation",
	journal=cacm, volume=8, year=1965, pages="89--101"
}

@incollection{ lauchli70,
        crossref="intandpfthy",
	author="H. L{\"a}uchli",
	title="An Abstract Notion of Realizability for which Intuitionistic Logic is Complete",
	pages="227--234"
}

@inproceedings{ leivant83,
	author="Daniel Leivant",
	title="Polymorphic Type Inference",
	booktitle=tenth # popl,
	year=1983,
	pages="88--98"
}



@TechReport{ luo+89,
	author="Zhaolui Luo and Robert Pollack and Paul Taylor",
	title="How to Use Lego: A Preliminary User's Manual",
	institution=lfcs,
        number="LFCS-TN-27",
	month=oct,
	year=1989
}

@TechReport{ luo88a,
	Author="Zhaolui Luo",
	Title="A Higher-Order Calculus and Theory Abstraction",
	Institution=lfcs,
	Number="ECS--LFCS--88--57",
	Month=jul,
	Year="1988"
}

@TechReport{ luo88b,
	Author="Zhaolui Luo",
	Title="{${\rm CC}^\infty_\subset$} and its Metatheory",
	Institution=lfcs,
	Number="ECS--LFCS--88-58",
	Month=jul,
	Year="1988"
}

@InProceedings{ luo89,
	Author="Zhaolui Luo",
	Title="ECC, an Extended Calculus of Constructions",
	Booktitle=fourth # lics,
	Month=jun,
	Year=1989,
	Address="Asilomar, California"
}

@comment{*M*}



@InProceedings{meyer+85,
  author = 	"Albert R. Meyer and Mitchell Wand",
  title = 	"Continuation Semantics in Typed Lambda Calculi (Summary)",
  booktitle = 	"Logics of Programs",
  year = 	1985,
  editor = 	"Rohit Parikh",
  pages = 	"219--224",
  publisher = 	springer,
  series=lncs,
  volume=224
}

@article{ macqueen+85,
	Author="David B. MacQueen and Donald T. Sannella",
	Title="Completeness of Proof Systems for Equational Specifications",
	Journal="{IEEE} Transactions on Software Engineering",
	Volume="SE-11",
	Year=1985,
	Pages="454--461"
}


@TechReport{ mason87,
	Author="Ian Mason",
	Title="{Hoare's} Logic in the {LF}",
	Institution="lfcs",
	Number="ECS--LFCS--87--32",
	Month=jun,
	Year="1987"
}


@book{ manna+85,
	author="Zohar Manna and Richard Waldinger",
	title="The Logical Basis for Computer Programming",
	publisher=aw,
	year=1985
}

@book{ maclane71,
	author="Saunders MacLane",
	title="Categories for the Working Mathematician",
	publisher=springer,
	series="Graduate Texts in Mathematics", volume=5,
	year=1971
}

@book{ manna74,
	author="Zohar Manna",
	title="Mathematical Theory of Computation",
	publisher="McGraw-Hill",
	year=1974
}

@book{ machtey+78,
	author="Michael Machtey and Paul Young",
	title="An Introduction to the General Theory of Algorithms",
	publisher=nh,
	year=1978
}

@inproceedings{ macqueen86a,
	author="David MacQueen",
	title="Using Dependent Types to Express Modular Structure",
	booktitle=thirteenth # popl,
	year=1986
}

@inproceedings{ macqueen86b,
	author="David MacQueen",
	title="Modules for {S}tandard {ML}",
	booktitle="1984" # lispandfp,
	year=1984,
	pages="198--207",
	note="Revised version appears in~{\cite{harper+86}}."
}

@techreport{ harper+86,
	author="Robert Harper and David MacQueen and Robin Milner",
	title="{S}tandard {ML}",
	institution=lfcs,
	year=1986,
	number="{ECS--LFCS--86--2}",
	month=mar
}

@article{ manna+80,
	author="Zohar Manna and Richard Waldinger",
	title="A Deductive Approach to Program Synthesis",
	journal=toplas,
	volume=2,
	number=1,
	year=1980,
	month=jan,
	pages="90--121"
}

@article{ macqueen+86,
	author="David MacQueen and Gordon Plotkin and Ravi Sethi",
	title="An Ideal Model for Recursive Polymorphic Types",
	journal=ic,
	year=1986, volume=18, number="1/2", month="October/November",
	pages="95--130"
}

@Unpublished{ martin-lof71a,
	Author="Per {Martin-L\"of}",
	Title="A Theory of Types",
	Note="Unpublished manuscript"
}

@inproceedings{ martin-lof71b,
        crossref="secondscand",
	author="Per {Martin-L\"of}",
	title="{\it Hauptsatz} for the Intuitionistic Theory of Iterated Inductive Definitions",
	pages="179--216"
}

@inproceedings{ martin-lof75,
        crossref="thirdscand",
	author="Per {Martin-L\"of}",
	title="About Models for Intuitionistic Type Theories and the Notion of Definitional Equality",
	pages="81--109"
}

@inproceedings{ martin-lof73,
        crossref="logiccolloquium73",
	author="Per {Martin-L\"of}",
	title="An Intuitionistic Theory of Types: Predicative Part",
	pages="73--118"
}

@book{	martin-lof84,
	author="Per {Martin-L\"of}",
	title="Intuitionistic Type Theory",
	publisher="Bibliopolis",
	address="Naples",
	year=1984,
	series="Studies in Proof Theory",
	volume=1
}

@book{	martin-lof70,
	author="Per {Martin-L\"of}",
	title="Notes on Constructive Mathematics",
	publisher="Almquist {\&} Wiksell",
	year=1970
}

@inproceedings{ martin-lof82,
	author="Per {Martin-L\"of}",
	title="Constructive Mathematics and Computer Programming",
	booktitle="Sixth International Congress for Logic, Methodology, and Philosophy of Science",
	publisher=nh,
	year=1982,
	pages="153--175"
}



@Unpublished{ martin-lof85a,
	Author="Per {Martin-L\"of}",
	Title="Truth of a Proposition, Evidence of a Judgement, Validity of a
	Proof",
	year=1985,
	month="June",
	Note="Lecture given at the workshop {``Theories of
	Meaning''}, Florence, Italy."
}


@techreport{ martin-lof85b,
	author="Per {Martin-L\"of}",
	title="On the Meanings of the Logical Constants and the Justifications of the Logical Laws",
	institution="Scuola di Specializzazione in Logica Matematica, Dipartimento di Matematica, Universit\`a di Siena",
	series="Atti degli Incontri di Logica Matematica", number=2,
	year=1985
}


@phdthesis{ mccarty84,
	author="David Charles McCarty",
	title="Realizability and Recursive Mathematics",
	school="Oxford University",
	year=1984
}

@incollection{ mccarthy63,
	author="John McCarthy",
	title="A Basis for a Mathematical Theory of Computation",
	booktitle="Computer Programming and Formal Systems",
	editor="P. Braffort and D. Herschberg",
	publisher=nh,
	year=1963,
	pages="33--70"
}



@PhDThesis{ mendler87,
	Author="Paul Mendler",
	Title="Recursive Definition in Type Theory",
	School="Cornell University",
	Year="1987"
}

@InProceedings{ mendler+88,
	Author="Paul F. Mendler and Peter Aczel",
	Title="The Notion of a Framework and a Framework for {LTC}",
	BookTitle=third # lics,
	Address="Edinburgh",
	Pages="392--401",
	Month=jul,
	Year="1988"
}



@InProceedings{mendler90a,
  author = 	"Nax Mendler",
  title = 	"A Series of Type Theories and Their Interpretation in the
		 Logical Theory of Constructions",
  crossref="lf-workshop"
}



@InProceedings{mendler90b,
  author = 	"Nax Mendler", 
  title = 	"Quotient Types via Coequalizers in Martin-L{\"o}f's Type
		 Theory",
  crossref="lf-workshop"
}

@article{ meyer82,
	author="Albert Meyer",
	title="What is a Model of the Lambda Calculus?",
	journal=icold,
	year=1982,
	volume=52,
	number=1,
	pages="87--122"
}

@inproceedings{ meyer+86,
	author="Albert Meyer and Mark Reinhold",
	title="{`Type'} is not a Type: Preliminary Report",
	booktitle=thirteenth # popl,
	year=1986
}

@techreport{ matthews82a,
	author="David C. J. Matthews",
	title="{POLY} Report",
	institution="Computer Laboratory, University of Cambridge",
	number=28,
	year=1982
}

@techreport{ matthews82b,
	author="David C. J. Matthews",
	title="Introduction to {POLY}",
	institution="Computer Laboratory, University of Cambridge",
	number=29,
	year=1982
}

@inproceedings{ mccracken84a,
        crossref="kahn+84",
	author="Nancy McCracken",
	title="The Type Checking of Programs with Implicit Type Structure",
	pages="301--316"
}

@article{ mccracken84b,
	author="Nancy McCracken",
	title="A Finitary Retract Model for the Polymorphic Lambda Calculus",
	journal=icold,
	year=1984, note="To appear."
}

@phdthesis{ mccracken79,
	author="Nancy McCracken",
	title="An Investigation of a Programming Language with a Polymorphic Type Structure",
	school="Syracuse University",
	address="Syracuse, New York",
	year=1979
}

@inproceedings{ meertens83,
	author="Lambert Meertens",
	title="Incremental Polymorphic Type Checking in {B}",
	booktitle=tenth # popl,
	year=1983,
	pages="265--275"
}



@TechReport{milner+88,
  author = 	"Robin Milner and Mads Tofte",
  title = 	"Co-induction in Relational Semantics",
  institution = 	lfcs,
  year = 	1988,
  number = 	"ECS-LFCS-88-65",
  address = 	"Edinburgh",
  month = 	"October"
}

@article{ milner77,
	author="Robin Milner",
	title="Fully Abstract Models of the Typed Lambda Calculus",
	journal=tcs,
	volume=4, year=1977, pages="348--375"
}

@article{ milner78,
	author="Robin Milner",
	title="A Theory of Type Polymorphism in Programming Languages",
	journal=jcss,
	volume=17, year=1978, pages="348--375"
}

@article{ milner83,
	author="Robin Milner",
	title="How {ML} Evolved",
	journal=polymorphism,
	volume=1, year=1983
}

@Article{mitchell88,
  author = 	 "John C. Mitchell",
  title = 	 "Polymorphic Type Inference and Containment",
  journal = 	 iandc,
  year = 	 1988,
  volume = 	 76,
  number = 	 "2/3",
  pages = 	 "211--249",
  note = 	 "(Reprinted in~\cite{huet90}, pp. 153--194.)"
}

@inproceedings{ mitchell84,
        crossref="kahn+84",
	author="John C. Mitchell",
	title="Type Inference and Type Containment",
        pages="257--278"
}

@inproceedings{ mitchell+85a,
	author="John C. Mitchell and Gordon Plotkin",
	title="Abstract Types Have Existential Type",
	booktitle=twelfth # popl,
	year=1985
}

@inproceedings{ mitchell+85b,
	author="John C. Mitchell and Albert Meyer",
	title="Second-Order Logical Relations",
	booktitle=lofp,
	publisher=springer, series=lncs,
	year=1985, pages="225--236"
}

@inproceedings{ mitchell86a,
	author="John C. Mitchell",
	title="Representation Independence and Data Abstraction",
	booktitle=thirteenth # popl,
	year=1986
}

@inproceedings{ mitchell86b,
	author="John C. Mitchell",
	title="A Type-Inference Approach to Reduction Properties and Semantics of Polymorphic Expressions",
	booktitle="1986" # lispandfp,
	month=aug, year=1986,
	pages="308--319"
}

@inproceedings{ mitchell+87,
	author="John C. Mitchell and Albert R. Meyer and Eugenio Moggi and Richard Statman",
	title="Empty Types in Polymorphic Lambda Calculus",
	booktitle=fourteenth # popl,
	month=jan, year=1987,
	pages="253--262"
}



@TechReport{mitchell89,
  author = 	"John C. Mitchell",
  title = 	"Type Systems for Programming Languages",
  institution = 	"Stanford University",
  year = 	1989,
  number = 	"STAN-CS-89-1277"
}

@InCollection{mitchell91,
  author = 	"John C. Mitchell",
  title = 	"Type Systems for Programming Languages",
  crossref = "vanleeuwen91",
  chapter = 	"8",
  pages = 	"365--458"
}



@inproceedings{ moggi89,
	author="Eugenio Moggi",
	title="Computational Lambda Calculus and Monads",
	booktitle=fourth # lics,
	address="Asilomar, California",
	month=jun,
	year="1989"
}



@InProceedings{ moggi89b,
  author = 	"Eugenio Moggi",
  title = 	"A Category-Theoretic Account of Program Modules",
  booktitle = 	"Proceedings of the Third Biennial Workshop on Category Theory
		 and Computer Science",
  year = 	1989,
  publisher = 	springer,
  month = 	sep
}

@inproceedings{ mulmuley84,
	author="Ketan Mulmuley",
	title="A Semantic Characterization of Full Abstraction for Typed Lambda Calculus",
	booktitle="Twenty-fifth" # focs,
	year=1984, pages="279--288"
}

@comment{*N*}

@Book{ nordstrom+90,
  author = 	"Bengt Norstr{\"o}m and Kent Petersson and Jan M. Smith",
  title = 	"Programming in Martin-L{\"o}f's Type Theory: An Introduction",
  publisher = 	"Oxford University Press",
  year = 	"1990",
  volume = 	"7",
  series = 	"International Series of Monographs on Computer Science"
}

@book{ nordstrom+88,
	author="Bengt Nordstr{\"o}m and Kent Petersson and Jan Smith",
	title="Programming in {Martin-L\"of's} Type Theory",
	publisher="University of G{\"o}teborg",
	address="G{\"o}teborg, Sweden",
	month="Midsummer",
	year=1988,
	note="Preprint"
}

@phdthesis{ nelson80,
	author="Greg Nelson",
	title="Techniques for Program Verification",
	school="Stanford University",
	address="Stanford, California",
	year=1980
}

@article{ nelson+80,
	author="Greg Nelson and Derek Oppen",
	title="Fast Decision Procedures Based on Congruence Closure",
	journal=jacm, volume=27, number=2, year=1980, month=apr, pages="356--364"
}

@article{ nelson+79,
	author="Greg Nelson and Derek Oppen",
	title="Simplification by Cooperating Decision Procedures",
	journal=toplas,
	volume=1,
	number=2,
	month=oct,
	year=1979,
	pages="245--257"
}

@article{ nordstrom+84,
	author="Bengt Nordstr{\"o}m and Jan Smith",
	title="Propositions, Types, and Specifications in {Martin-L\"of's} Type Theory",
	journal="BIT",
	volume=24,
	number=3,
	year=1984,
	pages="288--301"
}

@inproceedings{ nordstrom81,
	author="Bengt Nordstr{\"o}m",
	title="Programming in Constructive Set Theory: Some Examples",
	booktitle="1981" # fpca,
	address="Portsmouth, New Hampshire",
	year=1981,
	pages="141--153"
}

@article{ nordstrom+83,
	author="Bengt Nordstrom and Kent Petersson",
	title="Types and Specifications",
	journal=ipl,
	year=1983, pages="915--920"
}

@comment{*O*}

@book{ odonnell77,
	author="Michael J. O'Donnell",
	title="Computing in Systems Described by Equations",
	publisher=springer, series=lncs, volume=58,
	year=1977
}

@book{ odonnell85,
	author="Michael J. O'Donnell",
	title="Equational Logic as a Programming Language",
	publisher="MIT Press",
	year=1985
}

@inproceedings{ oppen78,
	author="Derek Oppen",
	title="Reasoning about Recursively-Defined Data Structures",
	booktitle=fifth # popl,
	year=1978, pages="151--157"
}

@comment{*P*}



@PhdThesis{pierce91,
  author = 	 "Benjamin C. Pierce",
  title = 	 "Programming with Intersection Types and Bounded Polymorphism",
  school = 	 cmu,
  year = 	 1991,
  address = 	 "Pittsburgh, PA",
  month = 	 "December"
}

@InProceedings{mohring86,
  author = 	"Christine Mohring",
  title = 	"Algorithm Development in the Calculus of Constructions",
  booktitle = 	first # lics,
  year = 	"1986",
  pages = 	"84--91",
  address = 	"Cambridge, MA",
  month = 	"June"
}



@InProceedings{paulin-mohring89a,
  author = 	"Christine Paulin-Mohring",
  title = 	"Extracting {$F_\omega$'s} Programs from Proofs in the
		 Calculus of Constructions",
  booktitle =   sixteenth # popl,
  year = 	"1989"
}

@PhdThesis{paulin-mohring89b,
  author = 	"Christine Paulin-Mohring",
  title = 	"Extraction de Programmes dans le Calcul des Constructions",
  school = 	"Universit{\'e} Paris 7",
  year = 	"1989"
}

@techreport{ pollack88,
	author="Robert Pollack",
	title="The Theory of {LEGO}",
	institution=lfcs,
	year=1988,
	note="To appear."
}



@TechReport{pfenning92,
  author = 	 "Frank Pfenning",
  title = 	 "On the Undecidability of Partial Polymorphic Type Reconstruction",
  institution =  cmu,
  year = 	 1992,
  number = 	 "CMU--CS--92--105",
  address = 	 "Pittsburgh, PA 15213",
  month = 	 "January"
}

@inproceedings{ pfenning89,
	author="Frank Pfenning",
	title="Elf: A Language for Logic Definition and Verified
Metaprogramming",
	booktitle=fourth # lics,
	year=1989, month=jun
}

@InCollection{pfenning91,
  author = 	"Frank Pfenning",
  title = 	"Logic Programming in the {LF} Logical Framework",
  crossref = "huet+91"
}

@PhDThesis{ pym90,
	Author="David Pym",
	Title="Proofs, Search and Computation in General Logic",
	School="Edinburgh University",
	Year="1990",
	Note="Available as Edinburgh University Computer Science
		 Department Technical Report ECS--LFCS--90--125"
}

@InCollection{ pym+91,
  author = 	"David Pym and Lincoln Wallen",
  title = 	"Proof Search in the {$\lambda\Pi$-calculus}",
  crossref = "huet+91"
}



@book{	prawitz65,
	author="Dag Prawitz",
	title="Natural Deduction: A Proof-Theoretical Study",
	publisher="Almquist {\&} Wiksell",
	year=1965
}

@article{ paterson+78,
	author="Michael S. Paterson and Mark N. Wegman",
	title="Linear Unification",
	journal=jcss,
	volume=16,
	year=1978,
	pages="158--197"
}

@techreport{ paulson83a,
	author="Lawrence Paulson",
	title="Tactics and Tacticals in {LCF}",
	institution="Computer Laboratory, University of Cambridge",
	year=1983, month=jul,
	number=39
}

@article{ paulson86,
	author="Lawrence Paulson",
	title="Natural Deduction Proof as Higher-Order Resolution",
	journal=jlp,
	volume=3, year=1986, pages="237--258"
}

@techreport{ paulson87,
	author="Lawrence Paulson",
	title="The Foundations of a Generic Theorem Prover",
	institution="Computer Laboratory, University of Cambridge",
	year=1987, number=130
}

@article{ paulson85a,
	author="Lawrence Paulson",
	title="Lessons Learned from {LCF}: A Survey of Natural Deduction Proofs",
	journal="The Computer Journal",
	volume=28, year=1985
}

@techreport{ paulson85b,
	author="Lawrence Paulson",
	title="Interactive Theorem Proving with {C}ambridge {LCF}",
	institution="Computer Laboratory, University of Cambridge",
	year=1985, month=nov, number=80
}

@article{ paulson83b,
	author="Lawrence Paulson",
	title="A Higher-Order Implementation of Rewriting",
	journal=scp,
	volume=3,
	year=1983,
	pages="119--149"
}

@inproceedings{ paulson84a,
        crossref="kahn+84",
	author="Lawrence Paulson",
	title="Structural Induction in {LCF}",
}

@techreport{ paulson84b,
	author="Lawrence Paulson",
	title="Verifying the Unification Algorithm in {LCF}",
	institution="Computer Laboratory, University of Cambridge",
	year=1984, month=mar,
	number=50
}

@techreport{ paulson84c,
	author="Lawrence Paulson",
	title="Constructing Recursion Operators in Intuitionistic Type Theory",
	institution="Computer Laboratory, University of Cambridge",
	year=1984, month=oct,
	number=57
}

@techreport{ petersson82,
	author="Kent Petersson",
	title="A Programming System for Type Theory",
	institution="Programming Methodology Group, University of {G\"oteborg}/Chalmers Institute of Technology",
	year=1982, month=mar,
	number=21
}



@Unpublished{ pitts+88,
	Author="Andrew M. Pitts and Paul Taylor",
	Title="A Note on {Russell's} Paradox in Locally Cartesian Closed
	Categories",
	Note="To appear"
}


@techreport{ petersson+85,
	author="Kent Petersson and Jan Smith",
	title="Program Derivation in Type Theory: The {P}olish Flag Problem",
	institution="Programming Methodology Group, University of {G\"oteborg}/Chalmers Institute of Technology",
	year=1985, month=jan
}

@article{ plotkin75,
	author="Gordon Plotkin",
	title="Call-by-Name, Call-by-Value, and the Lambda Calculus",
	journal=tcs, volume=1, year=1975, pages="125--159"
}

@TechReport{ plotkin72,
	Author="Gordon Plotkin",
	Title="A Set-Theoretical Definition of Application",
	Institution="School of Artificial Intelligence, Edinburgh University",
	Number="MIP--R--95",
	Year="1972"
}


@Article{ plotkin74,
	Author="Gordon Plotkin",
	Title="The $\lambda$-Calculus is $\omega$-Incomplete",
	Journal=jsl,
	Volume="39",
	Pages="313--317",
	Year="1974"
}


@article{ plotkin76,
	author="Gordon Plotkin",
	title="A Power Domain Construction",
	journal=sicomp, volume=5, year=1976, pages="452--487"
}

@article{ plotkin77,
	author="Gordon Plotkin",
	title="{LCF} Considered as a Programming Language",
	journal=tcs, volume=5, year=1977, pages="223--257"
}

@article{ plotkin78,
	author="Gordon Plotkin",
	title="{${\rm T}^{\omega}$} as a Universal Domain",
	journal=jcss, volume=17, year=1978, pages="209--236"
}

@techreport{ plotkin81,
	author="Gordon Plotkin",
	title="A Structural Approach to Operational Semantics",
	institution="Computer Science Department, Aarhus University",
	number="DAIMI--FN--19",
	year=1981
}

@inproceedings{ plotkin80,
        crossref="curryvolume",
	author="Gordon Plotkin",
	title="Lambda-Definability in the Full Type Hierarchy",
	pages="363--373"
}

@unpublished{ plotkin83,
	author="Gordon Plotkin",
	title="Notes for a Post-Graduate Course in Semantics",
	year=1983,
	note="Available from the Computer Science Department, University of Edinburgh"
}

@inproceedings{ prawitz73,
	author="Dag Prawitz",
	title="Towards a Foundation of a General Proof Theory",
	booktitle="Logic, Methodology, and Philosophy of Science, {VI}",
	editor="P. Suppes and L. Henkin and A. Joja and Gr. C. Moisil",
	publisher=nh,
	year=1973
}

@inproceedings{ prawitz70,
        crossref="secondscand",
	author="Dag Prawitz",
	title="Ideas and Results in Proof Theory",
	pages="235--308"
}

@comment{*Q*}

@comment{*R*}



@TechReport{ramsey90,
  author = 	"Norman Ramsey",
  title = 	"Concurrent Programming in {ML}",
  institution = 	"Computer Science Department, Princeton University",
  year = 	1990,
  number = 	"CS-TR-262-90"
}



@TechReport{reppy89,
  author = 	"John Reppy",
  title = 	"First-Class Synchronous Operations in Standard {ML}",
  institution = 	"Computer Science Department, Cornell University",
  year = 	1989,
  number = 	"TR~89-1068",
  address = 	"Ithaca, NY",
  month = 	"December"
}



@Unpublished{reppy90,
  author = 	"John Reppy",
  title = 	"Asynchronous Signals in Standard {ML}",
  note = 	"(Unpublished manuscript.)",
  year = 	1990,
  month = 	"August"
}

@book{ reps84,
	author="Thomas Reps",
	title="Generating Language-Based Environments",
	publisher="{MIT} Press",
	year=1984
}





@TechReport{reynolds88,
  author = 	 "John C. Reynolds",
  title = 	 "Preliminary Design of the Programming Language Forsythe",
  institution =  cmu,
  year = 	 1988,
  number = 	 "CMU--CS--88--159",
  address = 	 "Pittsburgh, PA",
  month = 	 "June"
}

@Article{reynolds70,
  author = 	"John C. Reynolds",
  title = 	"{GEDANKEN} --- A Simple Typeless Languages Based on the
		 Principle of Completeness and the Reference Concept",
  journal = 	cacm,
  year = 	1970,
  volume = 	13,
  number = 	5,
  pages = 	"308--319",
  month = 	"May"
}

@book{ reynolds81a,
	author="John C. Reynolds",
	title="The Craft of Programming",
	publisher=ph,
	year=1981
}

@book{ russell56,
	author="Bertrand Russell",
	title="Logic and Knowledge",
	publisher="Allen and Unwin",
	year=1956
}

@inproceedings{ reps+84,
	author="Thomas Reps and Bowen Alpern",
	title="Interactive Proof Checking",
	booktitle=eleventh # popl,
	year=1984
}

@techreport{ reps+87,
        author="Thomas W. Reps and Tim Teitelbaum",
	title="The Synthesizer Generator Reference Manual",
	institution="Cornell University",
	address="Ithaca, New York",
	year=1987,
	edition=second
}

@inproceedings{ reynolds74a,
	author="John C. Reynolds",
	title="Towards a Theory of Type Structure",
	booktitle="{\it Colloq. sur la Programmation}",
	year=1974,
	publisher=springer,
	series=lncs,
	volume=19,
	pages="408--423"
}


@inproceedings{ reynolds80,
	author="John C. Reynolds",
	title="Using Category Theory to Design Implicit Conversions and Generic Operators",
	booktitle="Proceedings of the Aarhus Workshop on Semantics-Directed Compiler Generation",
	editor="Neil Jones",
	publisher=springer, series=lncs, volume=94, year=1980,
	pages="211--258"
}

@incollection{ reynolds81b,
	author="John C. Reynolds",
	title="The Essence of {A}lgol",
	booktitle="Algorithmic Languages",
	editor="J. DeBakker",
	publisher=nh,
	year=1981, pages="513--523"
}



@InProceedings{ reynolds72,
  author = 	"John C. Reynolds",
  title = 	"Definitional Interpreters for Higher-Order Programming
		 Languages", 
  booktitle = 	"Conference Record of the 25th National {ACM} Conference",
  year = 	"1972",
  pages = 	"717--740",
  organization = 	"{ACM}",
  address = 	"Boston",
  month = 	"August"
}

@InProceedings{reynolds74b,
  author = 	"John C. Reynolds",
  title = 	"On the Relation Between Direct and Continuation Semantics",
  booktitle = 	"Proc. {ICALP} '74",
  year = 	"1974",
  pages = 	"141--156",
  publisher = 	springer,
  series =      lncs,
  volume=       14
}

@inproceedings{ reynolds84,
        crossref="kahn+84",
	author="John C. Reynolds",
	title="Polymorphism is not Set-Theoretic",
        pages="145--156"
}

@inproceedings{ reynolds85,
	author="John C. Reynolds",
	title="Three Approaches to Type Structure",
	booktitle="TAPSOFT",
	year=1985,
	publisher=springer
}


@TechReport{ reynolds+88,
	Author="John C. Reynolds and Gordon D. Plotkin",
	Title="On Functors Expressible in the Polymorphic Typed Lambda Calculus",
	Institution=lfcs,
	Number="ECS--LFCS--88-53",
	Month=may,
	Year="1988",
	Note="To appear in {\it Information and Computation}"
}

@unpublished{ rezus85,
	author="Adrian Rezus",
	title="A Semantics for {Martin-L\"of's} Constructive Type Theory",
	year=1985, note="Unpublished notes"
}

@article{ robinson65,
	author="John A. Robinson",
	title="A Machine-Oriented Logic Based on the Resolution Principle",
	journal=jacm,
	year=1965,
	volume=12,
	pages="23--41"
}



@InProceedings{ ronchi-della-rocca87,
	Author="Simona Ronchi della Rocca",
	Title="A Unification Semi-Algorithm for Intersection Type Schemes",
	BookTitle="TAPSOFT '87",
	Editor="Hartmut Ehrig and Robert Kowalski and Giorgio Levi and Ugo Montanari",
	Pages="37--51",
	Month=mar,
	Year="1987"
}




@article{ russell08,
	author="Bertrand Russell",
	title="Mathematical Logic as Based on a Theory of Types",
	journal="American Journal of Mathematics",
	volume=30,
	year=1908,
	pages="222--262"
}

@comment{*S*}

@InProceedings{salvesen+88,
  author = 	"Anne Salvesen and Jan M. Smith",
  title = 	"The Strength of the Subset Type in Martin-L{\"o}f's Type
		 Theory",
  booktitle = 	third # lics,
  year = 	"1988",
  pages = 	"384--391",
  address = 	"Edinburgh, Scotland"
}

@Unpublished{ salvesen90,
  author = 	"Anne Salvesen",
  title = 	"A Proof of the {C}hurch-{R}osser Property for the
		 {E}dinburgh {LF} with {$\eta$}-conversion",
  note = 	"Lecture given at the First Workshop on Logical
		 Frameworks, Sophia-Antipolis, France.",
  year = 	"1990",
  month = 	"May"
}



@Unpublished{sufrin89,
  author = 	"Bernard Sufrin",
  title = 	"{CSP}-Style Processes in {ML}",
  note = 	"(Private communication)",
  year = 	1989
}

@inproceedings{ sannella+86,
	author="Donald Sannella and Andrzej Tarlecki",
	title="Extended {ML}: An Institution-Independent Framework for Formal
Program Development",
	booktitle="Proc. Workshop on Category Theory and Computer Programming",
	address="Guildford",
	Publisher=springer,
	Volume=240,
	Series=lncs,
	pages="364--389",
	year=1986
}

@article{ sannella+88a,
	author="Donald Sannella and Andrzej Tarlecki",
	title="Specifications in an Arbitrary Institution",
	journal=ic,
	volume=76,
	year=1988,
	pages="165--210"
}


@inproceedings{ sannella+85,
	author="Donald Sannella and Andrzej Tarlecki",
	title="Program Specification and Development in {Standard} {ML}",
	booktitle=twelfth # popl,
	year=1985
}

@Article{ sannella+88b,
	Author="Donald Sannella and Andrzej Tarlecki",
	Title="Toward Formal Development of Programs from Algebraic Specifications: Implementations Revisited",
	Journal=ai,
	Volume="25",
	Pages="233-281",
	Year="1988"
}


@InProceedings{ sannella+83,
	Author="Donald Sannella and Rod Burstall",
	Title="Structured Theories in {LCF}",
	BookTitle="Proc. of the 8th Colloquium on Algebra and Trees in Programming",
	Address="L{'}Aquila, Italy",
	Pages="377--391",
	Year="1983"
}


@PhDThesis{ sander87,
	Author="Herbert P. Sander",
	Title="Categorical Combinators",
	School="University of G{\"o}teborg and Chalmers Institute of
	Technology",
	Month=jun,
	Year="1987"
}

@book{ schutte77,
	author="Kurt Sch{\"u}tte",
	title="Proof Theory",
	publisher=springer,
	year=1977
}

@book{ schoenfield67,
	author="Joseph R. Schoenfield",
	title="Mathematical Logic",
	publisher=aw,
	year=1967
}

@InProceedings{ seely84,
	Author="R. A. G. Seely",
	Title="Locally Cartesian Closed Categories and Type Theory",
	Organization="Cambridge Philosophical Society",
	BookTitle="Mathematical Proceedings of the Cambridge Philosophical Society",
	Volum=95,
	Pages="33--48",
	Year="1984"
}


@unpublished{ seely,
	Author="R. A. G. Seely",
	Title="Categorical Models for Higher-Order Polymorphic Lambda Calculus",
	Note="To appear in Journal of Symbolic Logic"
}

@TechReport{strachey+74,
  author = 	"Christopher Strachey and Christopher Wadsworth",
  title = 	"A Mathematical Semantics for Handling Full Jumps",
  institution = 	"Oxford University Computing Laboratory",
  year = 	1974,
  number = 	"Technical Monograph {PRG}--11"
}

@book{ stoy77,
	author="Joseph Stoy",
	title="Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory",
	publisher="{MIT} Press",
	year=1977
}

@book{ seldin+80,
        crossref="curryvolume"
}

@book{ seldin+70,
	editor="Jonathan P. Seldin and J. Roger Hindley",
	title="Symposium on Automated Deduction",
	publisher=springer,
	year=1970
}



@InProceedings{sitaram+90,
  author = 	"Dorai Sitaram and Matthias Felleisen",
  title = 	"Reasoning with Continuations {II}: Full
		 Abstraction for Models of Control",
  booktitle = 	"Proc. 1990 Conference on {LISP} and Functional Programming",
  year = 	1990,
  pages = 	"161--175",
  month = 	"June"
}

@book{	smullyan68,
	author="Raymond Smullyan",
	title="First-Order Logic",
	publisher=springer,
	year=1968
}



@TechReport{steele78,
  author = 	"Guy L. Steele, Jr.",
  title = 	"{RABBIT}: A Compiler for {SCHEME}",
  institution = 	"MIT AI Laboratory",
  year = 	1978,
  number = 	"Memo 474"
}

@book{	steele84,
	author="Guy L. {Steele Jr.}",
	title="Common {LISP}: The Language",
	publisher="Digital Press",
	year=1984
}

@book{	stenlund72,
	author="{S\"oren} Stenlund",
	title="Combinators, $\lambda$-terms and Proof Theory",
	publisher="D. Reidel",
	year=1972
}



@TechReport{sussman+75,
  author = 	"Gerald Jay Sussman and Guy Lewis Steele, Jr.",
  title = 	"Scheme: An Interpreter for Extended Lambda Calculus",
  institution = 	"MIT AI Laboratory",
  year = 	1975,
  number = 	"Memo No. 349",
  month = 	"December"
}



@TechReport{steele+78,
  author = 	 "Guy Lewis Steele, Jr. and Gerald Jay Sussman",
  title = 	 "The Revised Report on {Scheme}, a Dialect of {LISP}",
  institution =  "MIT AI Laboratory",
  year = 	 1978,
  number = 	 "Memo No. 452"
}

@inproceedings{ scott70,
	author="Dana Scott",
	title="Constructive Validity",
	booktitle="Symposium on Automatic Demonstration",
	publisher=springer,
	series="Lecture Notes in Mathematics",
	volume=125,
	year=1970,
	pages="237--275"
}

@article{ scott76,
	author="Dana Scott",
	title="Data Types as Lattices",
	journal=sicomp,
	volume=5,
	year=1976,
	pages="522--587"
}

@inproceedings{ scott80a,
        crossref="curryvolume",
	author="Dana Scott",
	title="Relating Theories of the Lambda Calculus",
        pages="403--450"
}

@inproceedings{ scott80b,
        crossref="kleenesymp",
	author="Dana Scott",
	title="The Lambda Calculus: Some Models, Some Philosophy",
        pages="381--421"
}

@unpublished{ scott80c,
	author="Dana Scott",
	title="A Space of Retracts",
	year=1980,
	note="Unpublished notes, Merton College, Oxford"
}

@inproceedings{ scott82,
	author="Dana Scott",
	title="Domains for Denotational Semantics",
	booktitle=ninth # icalp,
	publisher=springer,
	series=lncs, volume=140,
	editor="M. Nielson and E. M. Schmidt",
	pages="577--613", year=1982
}

@article{ schroeder-heister84,
	author="Peter {Schr\"oder--Heister}",
	title="A Natural Extension of Natural Deduction",
	journal=jsl,
	volume=49, number=4,
	month=dec, year=1984
}

@inproceedings{ schmidt84,
	author="David Schmidt",
	title="A Programming Notation for Tactical Reasoning",
	booktitle=seventh # cade,
	publisher=springer,
	series=lncs, volume=170,
	editor="R. E. Shostak",
	pages="445-459", year=1984
}

@inproceedings{ shamir+77,
	author="A. Shamir and W. W. Wadge",
	title="Data Types as Objects",
	booktitle=fourth # icalp,
	editor="A. Salomaa",
	publisher=springer,
	series=lncs, volume=52,
	year=1977, pages="465--479"
}

@inproceedings{ scherlis+83,
	author="William Scherlis and Dana Scott",
	title="First Steps Toward Inferential Programming",
	booktitle="Proceedings of the {IFIP} Congress",
	address="Paris",
	year=1983
}

@article{ smith84a,
	author="Jan Smith",
	title="An Interpretation of {Martin-L\"of's} Type Theory in a Type-Free Theory of Propositions",
	journal=jsl,
	volume=49,
	number=3,
	month=sep,
	year=1984,
	pages="730--753"
}

@inproceedings{ smith84b,
	author="Brian C. Smith",
	title="Reflection and Semantics in {LISP}",
	booktitle=eleventh # popl,
	year=1984, pages="23--35"
}

@article{ smyth+82,
	author="Michael B. Smyth and Gordon D. Plotkin",
	title="The Category-Theoretic Solution of Recursive Domain Equations",
	journal=sicomp,
	volume=11, year=1982, pages="761--783"
}

@phdthesis{ stansifer85,
	author="Ryan D. Stansifer",
	title="Representing Constructive Theories in High-Level Programming Languages",
	school="Cornell University",
	address="Ithaca, New York",
	year=1985
}

@article{ statman79a,
	author="Richard Statman",
	title="Intuitionistic Propositional Logic is Polynomial-Space Complete",
	journal=tcs,
	volume=9,
	year=1970,
	pages="73--81"
}

@article{ statman79b,
	author="Richard Statman",
	title="The Typed {$\lambda$}-Calculus is not Elementary Recursive",
	journal=tcs, volume=9, year=1979, pages="73--81"
}

@inproceedings{ statman80,
        crossref="curryvolume",
	author="Richard Statman",
	title="On the Existence of Closed Terms in the Typed {$\lambda$}-Calculus, {I}",
	pages="511-534"
}

@article{ statman81,
	author="Richard Statman",
	title="On the Existence of Closed Terms in the Typed {$\lambda$}-Calculus, {II}",
	journal=tcs, volume=15, year=1981,pages="329--338"
}

@article{ statman82a,
	author="Richard Statman",
	title="Completeness, Invariance, and Lambda-Definability",
	journal=jsl, volume=47, year=1982, pages="17--26"
}

@article{ statman82b,
	author="Richard Statman",
	title="{$\lambda$}-Definable Functionals and {$\beta\eta$} Conversion",
	journal="Archiv {f\"ur} Mathematische Logik und Grundlagenforschung",
	volume=22, year=1982, pages="1-6"
}

@Article{statman85,
  author = 	"Richard Statman",
  title = 	"Logical Relations and the Typed {$\lambda$}-Calculus",
  journal = 	icold,
  year = 	1985,
  volume = 	65,
  pages = 	"85--97"
}

@unpublished{ statman83a,
	author="Richard Statman",
	title="Equality between Functionals Revisited",
	year=1983, note="To appear, Friedman volume"
}

@unpublished{ statman83b,
	author="Richard Statman",
	title="Embeddings, Homomorphisms, and {$\lambda$}-Definability",
	year=1983, note="Unpublished notes"
}

@unpublished{ statman83c,
	author="Richard Statman",
	title="On the Existence of Closed Terms in the Typed {$\lambda$}-Calculus, {III}",
	year=1983, note="To appear"
}

@comment{*T*}



@Article{tofte90,
  author = 	 "Mads Tofte",
  title = 	 "Type Inference for Polymorphic References",
  journal = 	 ic,
  year = 	 1990,
  volume = 	 89,
  pages = 	 "1--34",
  month = 	 "November"
}

@PhdThesis{tofte88,
  author = 	"Mads Tofte",
  title = 	"Operational Semantics and Polymorphic Type Inference",
  school = 	"Edinburgh University",
  year = 	"1988",
  note =        "Available as Edinburgh University Laboratory for Foundations
		 of Computer Science Technical Report ECS--LFCS--88--54."
}

@article{ thatcher+82,
	author="James W. Thatcher and Eric G. Wagner and James B. Wright",
	title="Data Type Specification, Parameterization, and the Power of
Specification Techniques",
	journal=toplas,
	volume=4,
	pages="711--732",
	year=1982
}

@inproceedings{ tarlecki86a,
	author="Andrzej Tarlecki",
	title="Bits And Pieces of the Theory of Institutions",
	booktitle="Proc. Workshop on Category Theory and Computer Programming",
	address="Guildford",
	Publisher=springer,
	Volume=240,
	Series=lncs,
	pages="334--363",
	year=1986
}

@article{ tarlecki86b,
	author="Andrzej Tarlecki",
	title="Quasi-Varieties in Abstract Algebraic Institutions",
	journal=jcss,
	volume=33,
	year=1986,
	pages="333--360"
}

@unpublished{ tarlecki+89,
	author="Andrzej Tarlecki and Rod Burstall and Joseph Goguen",
	title="Some Fundamental Algebraic Tools for the Semantics of
Computation, {Part III}: {I}ndexed Categories",
	note="To appear, Theoretical Computer Science"
}

@book{ tennant81,
	author="Robert Tennant",
	title="Principles of Programming Languages",
	publisher=ph,
	year=1981
}

@book{ takeuti75,
	author="Gaisi Takeuti",
	title="Proof Theory",
	publisher=nh,
	year=1975
}



@InProceedings{ talcott88,
  author = 	"Carolyn Talcott",
  title = 	"Rum: An Intensional Theory of Function and Control
		 Abstractions",
  booktitle = 	"Proc. 1987 Workshop of Foundations of Logic and Functional
		 Programming",
  year = 	"1988",
  publisher =springer,
  series=lncs,
  volume=306
}

@book{ toledo75,
	author="Sue Ann Toledo",
	title="Tableau Systems for First-Order Number Theory and Certain Higher-Order Theories",
	publisher=springer,
	series=lnm,
	volume=447,
	year=1975
}

@book{	troelstra73,
	editor="Ann S. Troelstra",
	title="Metamathematical Investigation of Intuitionistic Arithmetic and Analysis",
	publisher=springer,
	year="1973",
	series=lnm,
	volume=344
}

@article{ tait67,
	author="William W. Tait",
	title="Intensional Interpretation of Functionals of Finite Type",
	journal=jsl,
	volume=32, number=2,
	year=1967,
	month=jun,
	pages="187--199"
}

@inproceedings{ tait73,
        crossref="logiccolloquium73",
	author="Willam W. Tait",
	title="A Realizability Interpretation of the Theory of Species",
        pages="22--37"
}

@article{ teitelbaum+81,
	author="R. Teitelbaum and T. Reps",
	title="The {C}ornell {P}rogram {S}ynthesizer: A Syntax-Directed Programming Environment",
	journal=cacm,
	volume=24, number=9,
	month=sep,
	year=1981,
	pages="563--573"
}

@comment{*U*}

@comment{*V*}

@comment{*W*}

@article{ winskel85,
	author="Glynn Winskel",
	title="Synchronization Trees",
	journal=tcs,
	volume=34,
	pages="33--82",
	year=1981
}

@book{	whitehead+25,
	author="Alfred North Whitehead and Bertrand Russell",
	title="Principia Mathematica, Volume 1",
	publisher="Cambridge University Press",
	year=1925
}

@book{ wikstrom87,
       author="{\AA}ke Wikstr{\"o}m",
       title="Functional Programming using {Standard} {ML}",
       publisher=ph,
       series="International Series in Computer Science",
       year=1987
}

@article{ wirsing86,
	title="Structured Algebraic Specifications: A Kernel Language",
	author="Martin Wirsing",
	journal=tcs,
	volume=42,
	pages="123--249",
	year=1986
}

@book{ wirth73,
	author="Niklaus Wirth",
	title="Systematic Programming: An Introduction",
	publisher=ph,
	year=1973
}



@InProceedings{wand80,
  author = 	"Mitchell Wand",
  title = 	"Continuation-Based Multiprocessing",
  booktitle = 	"Conference Record of the 1980 {LISP} Conference",
  year = 	1980,
  pages = 	"19--28"
}

@inproceedings{
	wand84,
	author="Mitchell Wand",
	title="A Types-as-Sets Semantics for {Milner}-Style Polymorphism",
	booktitle=eleventh # popl,
	month=jan, year=1984,
	pages="158--164"
}



@Unpublished{wright+90,
  author = 	"Andrew Wright and Matthias Felleisen",
  title = 	"The Nature of Exceptions in Polymorphic Lannguages",
  note = 	"Unpublished manuscript, Rice University",
  year = 	1990
}

@TechReport{wright+91,
  author = 	 "Andrew K. Wright and Matthias Felleisen",
  title = 	 "A Syntactic Approach to Type Soundness",
  institution =  "Department of Computer Science, Rice University",
  year = 	 1991,
  number = 	 "TR91--160",
  month = 	 "July"
}

@comment{*X*}

@comment{*Y*}

@book{ yeh78,
	editor="Raymond Yeh",
	title="Current Trends in Programming Methodology",
	publisher=ph,
	year=1978
}

@comment{*Z*}



@comment{Cross-referenced Material}

@book{ barwise77,
	editor="John Barwise",
	title="The Handbook of Mathematical Logic",
        booktitle="The Handbook of Mathematical Logic",
	publisher=nh,
	year=1977
}

@book{ boyer+81,
	editor="Robert S. Boyer and J S. Moore",
	title="The Correctness Problem in Computer Science",
	booktitle="The Correctness Problem in Computer Science",
	publisher=ap,
	year=1981
}

@Book{vanheijenoort67,
  title = 	"From Frege to G{\"o}del: A Source Book in Mathematical Logic, 1879-1931",
  booktitle=    "From Frege to G{\"o}del: A Source Book in Mathematical Logic, 1879-1931",
  publisher = 	"Harvard University Press",
  year = 	1967,
  editor = 	"Jean van Heijenoort",
  address = 	"Cambridge, MA"
}

@proceedings{kahn+84,
	editor="Gilles Kahn and David MacQueen and Gordon Plotkin",
	title="Semantics of Data Types",
        booktitle="Semantics of Data Types",
	publisher=springer,
	year=1984,
        month=jun,
	series=lncs,
	volume=173
}

@Proceedings{logiccolloquium73,
  title = 	"Logic Colloquium '73",
  booktitle=    "Logic Colloquium '73",
  year = 	1975,
  editor = 	"H. E. Rose and J. C. Shepherdson",
  publisher = 	nh,
  series="Studies in Logic and the Foundations of Mathematics",
  volume=80
}

@Proceedings{logiccolloquium75,
  title = 	"Logic Colloquium '75",
  booktitle=    "Logic Colloquium '75",
  year = 	1975,
  editor = 	"Rohit Parikh",
  publisher = 	nh,
  series="Studies in Logic and the Foundations of Mathematics"
}

@Proceedings{logiccolloquium77,
  title = 	"Logic Colloquium, '77",
  booktitle=    "Logic Colloquium, '77",
  year = 	1978,
  editor = 	"A. MacIntyre and L. Pacholaki and J. Paris",
  publisher = 	nh,
  series="Studies in Logic and the Foundations of Mathematics"
}

@Proceedings{logiccolloquium88,
  title = 	"Logic Colloquium, '88",
  booktitle =	"Logic Colloquium, '88",
  year = 	"1989",
  publisher = 	"North Holland",
  address = "Amsterdam"
}

@Proceedings{kleenesymp,
  title = 	"The {K}leene Symposium",
  booktitle="The {K}leene Symposium",
  year = 	1980,
  editor = 	"J. Keisler and J. Barwise and K. Kunen",
  publisher = 	nh,
  series="Studies in Logic and the Foundations of Mathematics"
}

@Proceedings{intandpfthy,
  title = 	"Intuitionism and Proof Theory",
  booktitle="Intuitionism and Proof Theory",
  year = 	1970,
  editor = 	"J. Myhill and A. Kino and R. E. Vesley",
  publisher = 	nh,
  series="Studies in Logic and the Foundations of Mathematics"
}

@Proceedings{curryvolume,
  title = 	"To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus
		 and Formalism",
  booktitle = 	"To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus
		 and Formalism",
  year = 	1980,
  editor = 	"J. P. Seldin and J. R. Hindley",
  publisher = 	ap
}

@Proceedings{secondscand,
  title = 	"Proceedings of the Second Scanindavian Logic Symposium",
  booktitle = 	"Proceedings of the Second Scanindavian Logic Symposium",
  year = 	1971,
  editor = 	"J. E. Fenstad",
  publisher = 	nh,
  series="Studies in Logic and the Foundations of Mathematics"
}

@Proceedings{thirdscand,
  title = 	"Proceedings of the Third Scandinavian Logic Symposium",
  booktitle = 	"Proceedings of the Third Scandinavian Logic Symposium",
  year = 	1975,
  editor = 	"S. Kanger",
  publisher = 	nh,
  series="Studies in Logic and the Foundations of Mathematics"
}

@Proceedings{ gray+89,
	Editor="John W. Gray and Andre Scedrov",
	Title="Categories in Computer Science and Logic",
	BookTitle="Categories in Computer Science and Logic",
	Publisher="American Mathematical Society",
	Series="Contemporary Mathematics",
	Volume=92,
	Year=1989
}

@Proceedings{lf-workshop,
  title = 	"Proceedings of the First Workshop on Logical Frameworks",
  year = 	1990,
  editor = 	"G{\'e}rard Huet and Gordon Plotkin",
  address = 	"Antibes, France",
  month = 	"May",
  note = 	"(To appear)"
}

@Book{nivat+85,
  title = 	"Algebraic Methods in Semantics",
  booktitle=    "Algebraic Methods in Semantics",
  publisher = 	"Cambridge University Press",
  year = 	1985,
  editor = 	"Maurice Nivat and John C. Reynolds",
  address = 	"Cambridge"
}

@Book{huet+91,
  title = 	"Logical Frameworks",
  booktitle=    "Logical Frameworks",
  publisher = 	"Cambridge University Press",
  year = 	"1991",
  editor = 	"G. Huet and G. Plotkin"
}

@Book{ odifreddi90,
  title = 	"Logic and Computation",
  booktitle =	"Logic and Computation",
  editor = 	"P. Odifreddi",
  publisher = 	"Academic Press",
  year = 	"1990"
}

@Book{ huet90,
  title = 	"Logical Foundations of Functional Programming",
  booktitle =	"Logical Foundations of Functional Programming",
  publisher = 	"Addison-Wesley",
  series = "University of Texas at Austin Year of Programming Series",
  year = 	"1990",
  editor = 	"G\'erard Huet"
}

@Book{vanleeuwen91,
  editor = 	"Jan van Leeuwen",
  booktitle = 	"Handbook of Theoretical Computer Science",
  publisher = 	"Elsevier",
  year = 	"1991",
  volume = 	"B: Formal Models and Semantics",
  address = 	"Amsterdam"
}

@Book{turner90,
  title =	"Research Topics in Functional Programming",
  booktitle = 	 "Research Topics in Functional Programming",
  publisher = 	 aw,
  year = 	 1990,
  editor = 	 "David A. Turner"
}
