@incollection(Barendregt1992,
 author       = {H. Barendregt},
 year         = {1992},
 title        = {Lambda calculi with types},
 editor       = {S. Abramsky and D.M. Gabbay and T.S.E. Maibaum},
 booktitle    = {Handbook of {Logic} in {Computer} {Science}},
 volume       = {2},
 publisher    = {Oxford University Press},
 pages        = {117--309},
)
@inproceedings(Blanqui,
 author       = {F. Blanqui},
 year         = {2001},
 title        = {Definitions by Rewriting in the Calculus of Constructions},
 booktitle    = {Logic in Computer Science},
 publisher    = {{IEEE} Computer Society},
 pages        = {9--18},
 doi          = {10.1109/LICS.2001.932478},
)
@inproceedings(Sacerdoti,
 author       = {C. Sacerdoti Coen},
 year         = {2004},
 title        = {Mathematical Libraries as Proof Assistant Environments},
 editor       = {A. Asperti and G. Bancerek and A. Trybulec},
 booktitle    = {Mathematical Knowledge Management},
 series       = {Lecture Notes in Computer Science},
 volume       = {3119},
 publisher    = {Springer},
 pages        = {332--346},
 doi          = {10.1007/978-3-540-27818-4\_24},
)
@article(CoquandHuet,
 author       = {T. Coquand and G. Huet},
 year         = {1988},
 title        = {The Calculus of Constructions},
 journal      = {Information and Computation},
 volume       = {76},
 number       = {2/3},
 pages        = {95--120},
 doi          = {10.1016/0890-5401(88)90005-3},
)
@inproceedings(CD,
 author       = {D. Cousineau and G. Dowek},
 year         = {2007},
 title        = {Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo},
 editor       = {S. Ronchi Della Rocca},
 booktitle    = {Typed Lambda Calculi and Applications},
 series       = {Lecture Notes in Computer Science},
 volume       = {4583},
 publisher    = {Springer},
 pages        = {102--117},
 doi          = {10.1007/978-3-540-73228-0\_9},
)
@inproceedings(GeuversKrebbersMcKinnaWiedijk,
 author       = {H. Geuvers and R. Krebbers and J. McKinna and F. Wiedijk},
 year         = {2010},
 title        = {Pure Type Systems without Explicit Contexts},
 editor       = {K. Crary and M. Miculan},
 booktitle    = {Logical Frameworks and Meta-languages: Theory and Practice},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {34},
 publisher    = {Open Publishing Association},
 pages        = {53--67},
 doi          = {10.4204/EPTCS.34.6},
)
@article(GeuversNederhof,
 author       = {H. Geuvers and M.-J. Nederhof},
 year         = {1991},
 title        = {Modular proof of strong normalization for the calculus of constructions},
 journal      = {Journal of Functional Programming},
 volume       = {1},
 number       = {2},
 pages        = {155--189},
 doi          = {10.1017/S0956796800020037},
)