bib.bib

@phdthesis{westbrook-thesis,
author = {Edwin Westbrook},
title = {Higher-Order Encodings with Constructors},
year = 2008,
school = {Washington University in Saint Louis}
}

@inproceedings{westbrook09,
  author = {Edwin Westbrook and Aaron Stump and Evan Austin},
  booktitle = {Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice ({LFMTP} '09)},
  year = 2009,
  pages = {74--83},
  title = {The calculus of nominal inductive constructions: an intensional approach to encoding name-bindings}
}

@book{girard-proofs-types,
title={{Proofs and Types}},
author={J.-Y. Girard and Y. Lafont and P. Taylor},
publisher="Cambridge University Press",
year=1989}

@manual{coq,
author={{The Coq Development Team}},
title={{The Coq Proof Assistant Reference Manual, Version V8.3}},
year=2010,
note="http://coq.inria.fr/doc/"}

@incollection{martinlof72,
  author={Per Martin-L\"{o}f},
  title="An Intuitionistic Theory of Types",
  booktitle="Twenty-Five Years of Constructive Type Theory",
  editor="G Sambin and J Smith",
  publisher="Oxford University Press",
  year=1998
}

@article{coquand88,
 author = {T. Coquand and G. Huet},
 title = {{The Calculus of Constructions}},
 journal = {Information and Computation},
 volume = {76},
 number = {2-3},
 year = {1988},
 pages = "95--120"}

@book{nps90,
title={{Programming in Martin-L\"{o}f's Type Theory}},
author={B. Nordstr\"{o}m and K. Petersson and J. Smith},
publisher="Oxford University Press",
year=1990}

@book{baader-nipkow98,
author = "Franz Baader and Tobias Nipkow",
title = {{Term Rewriting and All That}},
publisher = "Cambridge University Press",
year="1998"}


@inproceedings{werner97,
  author    = {Benjamin Werner},
  title     = {Sets in Types, Types in Sets},
  booktitle = {Third International Symposium on Theoretical Aspects of Computer Software (TACS)},
  year      = {1997},
  pages     = {530--346}
}

@inproceedings{miquel02,
 author = {Alexandre Miquel and Benjamin Werner},
 title = {The not so simple proof-irrelevant model of CC},
 booktitle = {The 2002 international conference on Types for proofs and programs (TYPES)},
 year = {2002},
 pages = {240--258}
} 

@inproceedings{miquel00,
 author = {Alexandre Miquel},
 title = {A Model for Impredicative Type Systems, Universes, Intersection Types and Subtyping},
 booktitle = {15th Annual IEEE Symposium on Logic in Computer Science (LICS)},
 year = {2000}
} 

@article{werner08,
  author    = {Benjamin Werner},
  title     = {On the strength of proof-irrelevant type theories},
  journal   = {Logical Methods in Computer Science},
  volume    = {4},
  issue     = {3},
  year      = {2008}
}

@INPROCEEDINGS{stefanova96,
    author = {M. Stefanova and H. Geuvers},
    title = {A Simple Model Construction for the Calculus of Constructions},
    booktitle = {The 1996 International Conference on Types for Proofs and Programs (TYPES)},
    year = {1996},
    pages = {5--8}
}

@inproceedings{aczel77,
author = "Peter Aczel",
title = "The Type Theoretic Interpretation of Constructive Set Theory",
booktitle = "Logic Colloqium '77",
year = "1977"
}


@inproceedings{aczel83,
author = "Peter Aczel",
title = "The Type Theoretic Interpretation of Constructive Set Theory: Inductive Definitions",
booktitle = "Seventh International Congress of Logic, Methodology and Philosophy of Science",
year = "1983"
}

@article{barras10,
 author = "Bruno Barras",
 title = "Sets in Coq, Coq in Sets",
 journal = "Journal of Formalized Reasoning",
 volume = "3",
 number = "1",
 year = "2010",
 pages = "29--48"
}

@phdthesis{goguen94,
 author = "Healfdene Goguen",
 title = "A Typed Operational Semantics for Type Theory",
 year = "1994",
 school = "University of Edinburgh"
}

@article{geuvers91,
 author = "Herman Geuvers and Mark-Jan Nederhof",
 title = "Modular proof of Strong Normalization for the Calculus of Constructions",
 journal = "Journal of Functional Programming",
 volume = "1",
 number = "2",
 pages = "155--189",
 year = "1991"
}

@techreport{coquand90,
 author = "Thierry Coquand and Jean Gallier",
 title = "A Proof of Strong Normalization for the Theory of Constructions Using a Kripke-like Interpretation",
 institution = "University of Pennsylvania",
 number = "MS-CIS-90-44",
 year = "1990"
}

@phdthesis{luo90,
 author = "Zhaohui Luo",
 title = "An Extended Calculus of Constructions",
 school = "University of Edinburgh",
 year = "1990"
}

@inproceedings{geuvers94,
 author = {Herman Geuvers},
 title = {A short and flexible proof of Strong Normalization for the Calculus of Constructions},
 booktitle = {International Workshop on Types for Proofs and Programs},
 year = {1995},
 pages = {14--38}
} 

@phdthesis{altenkirch93,
 author = "Thorsten Altenkirch",
 title = "Constructions, Inductive Types and Strong Normalization",
 school = "University of Edinburgh",
 year = "1993"
}

@article{gallier91,
    author = {Jean Gallier},
    journal = {Annals of Pure and Applied Logic},
    volume = {53},
    number = {3},
    pages = {199--260},
    title = {{What's so special about Kruskal's theorem and the ordinal {$\Gamma_0$}? A survey of some results in proof theory}},
    year = {1991}
}

@misc{coquand97,
  author = {Thierry Coquand and Peter Hancock and Anton Setzer},
  title = {Ordinals in Type Theory},
  year = {1997},
  note = {invited talk at Computer Science Logic (CSL '97)}
}

@book{enderton77,
  author = {Herbert B. Enderton},
  title = {Elements of Set Theory},
  publisher = {Academic Press},
  year = {1977}
}

@techreport{westbrook-techreport,
  author = "Edwin Westbrook",
 title = "Uniform Logical Relations",
 institution = "Rice University",
 number = "TR11-01",
 year = "2011"
}

@book{pohlers89,
  author = {Wolfram Pohlers},
  title = {Proof Theory: The First Step into Impredicativity},
  publisher = {Springer-Verlag},
  year = {1989}
}