@inproceedings(bernardy11,
 author       = {Jean{-}Philippe Bernardy and Marc Lasson},
 year         = {2011},
 title        = {{Realizability and Parametricity in Pure Type Systems}},
 editor       = {Martin Hofmann},
 booktitle    = {Foundations of Software Science and Computational Structures - 14th International Conference, {FOSSACS} 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, {ETAPS} 2011, Saarbr{\"{u}}cken, Germany, March 26-April 3, 2011. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {6604},
 publisher    = {Springer},
 pages        = {108--122},
 doi          = {10.1007/978-3-642-19805-2\_8},
)
@book(bird+97,
 author       = {Richard S. Bird and Oege de Moor},
 year         = {1997},
 title        = {Algebra of programming},
 series       = {Prentice Hall International series in computer science},
 publisher    = {Prentice Hall},
 doi          = {10.1017/S095679689922326X},
)
@incollection(debruijn80,
 author       = {N.G. de Bruijn},
 year         = {1994},
 title        = {A Survey of the Project Automath**Reprinted from: Seldin, J. P. and Hindley, J. R., eds., To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, p. 579-606, by courtesy of Academic Press Inc., Orlando.},
 editor       = {R.P. Nederpelt and J.H. Geuvers and R.C. de Vrijer},
 booktitle    = {Selected Papers on Automath},
 series       = {Studies in Logic and the Foundations of Mathematics},
 volume       = {133},
 publisher    = {Elsevier},
 pages        = {141 -- 161},
 doi          = {10.1016/S0049-237X(08)70203-9},
)
@book(constable+86,
 author       = {Robert L. Constable and Stuart F. Allen and Mark Bromley and Rance Cleaveland and J. F. Cremer and R. W. Harper and Douglas J. Howe and Todd B. Knoblock and N. P. Mendler and Prakash Panangaden and James T. Sasaki and Scott F. Smith},
 year         = {1986},
 title        = {Implementing mathematics with the Nuprl proof development system},
 publisher    = {Prentice Hall},
)
@article(diehl18,
 author       = {Larry Diehl and Denis Firsov and Aaron Stump},
 year         = {2018},
 title        = {Generic Zero-cost Reuse for Dependent Types},
 journal      = {Proc. ACM Program. Lang.},
 volume       = {2},
 number       = {ICFP},
 pages        = {104:1--104:30},
 doi          = {10.1145/3236799},
)
@inproceedings(firsov18b,
 author       = {Denis Firsov and Richard Blair and Aaron Stump},
 year         = {2018},
 title        = {{Efficient Mendler-Style Lambda-Encodings in Cedille}},
 editor       = {Jeremy Avigad and Assia Mahboubi},
 booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP} 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {10895},
 publisher    = {Springer},
 pages        = {235--252},
 doi          = {10.1007/978-3-319-94821-8\_14},
)
@inproceedings(firsov18,
 author       = {Denis Firsov and Aaron Stump},
 year         = {2018},
 title        = {Generic Derivation of Induction for Impredicative Encodings in Cedille},
 booktitle    = {Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs},
 series       = {CPP 2018},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {215--227},
 doi          = {10.1145/3167087},
)
@inproceedings(geuvers01,
 author       = {Herman Geuvers},
 year         = {2001},
 title        = {{Induction Is Not Derivable in Second Order Dependent Type Theory}},
 booktitle    = {Typed Lambda Calculi and Applications (TLCA)},
 pages        = {166--181},
 doi          = {10.1007/3-540-45413-6\_16},
)
@phdthesis(girard72,
 author       = {Jean-Yves Girard},
 year         = {1972},
 title        = {Interpr{\'e}tation functionelle et {\'e}limination des coupures dans l\IeC{\textquoteright}arithm{\'e}tique d\IeC{\textquoteright}ordre sup{\'e}rieure},
 school       = {Universit{\'e} Paris VII},
)
@book(hindleyseldin,
 author       = {J. Roger Hindley and Jonathan P. Seldin},
 year         = {2008},
 title        = {{Lambda-Calculus and Combinators: An Introduction}},
 edition      = {2},
 publisher    = {Cambridge University Press},
 address      = {New York, NY, USA},
 doi          = {10.1017/CBO9780511809835},
)
@inproceedings(kopylov03,
 author       = {A. Kopylov},
 year         = {2003},
 title        = {Dependent intersection: a new way of defining records in type theory},
 booktitle    = {18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings.},
 pages        = {86--95},
 doi          = {10.1109/LICS.2003.1210048},
)
@phdthesis(luo90,
 author       = {Zhaohui Luo},
 year         = {1990},
 title        = {An extended calculus of constructions},
 school       = {University of Edinburgh, {UK}},
 url          = {http://hdl.handle.net/1842/12487},
)
@inproceedings(martinlof73,
 author       = {Martin-L{\"o}f, P.},
 year         = {1975},
 title        = {An intuitionisitc theory of types, Predicative part},
 booktitle    = {Logic Colloquium 1973},
 pages        = {73--118},
)
@article(mendler91,
 author       = {N. P. Mendler},
 year         = {1991},
 title        = {Inductive Types and Type Constraints in the Second-Order lambda Calculus},
 journal      = {Ann. Pure Appl. Logic},
 volume       = {51},
 number       = {1-2},
 pages        = {159--172},
 doi          = {10.1016/0168-0072(91)90069-X},
)
@article(miller05,
 author       = {Dale Miller and Alwen Tiu},
 year         = {2005},
 title        = {A proof theory for generic judgments},
 journal      = {{ACM} Trans. Comput. Log.},
 volume       = {6},
 number       = {4},
 pages        = {749--783},
 doi          = {10.1145/1094622.1094628},
)
@incollection(miquel01,
 author       = {Alexandre Miquel},
 year         = {2001},
 title        = {The Implicit Calculus of Constructions Extending Pure Type Systems with an Intersection Type Binder and Subtyping},
 editor       = {Samson Abramsky},
 booktitle    = {Typed Lambda Calculi and Applications},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {344--359},
 doi          = {10.1007/3-540-45413-6_27},
)
@article(mitchell+1991,
 author       = {John C. Mitchell and Eugenio Moggi},
 year         = {1991},
 title        = {Kripke-Style Models for Typed lambda Calculus},
 journal      = {Ann. Pure Appl. Logic},
 volume       = {51},
 number       = {1-2},
 pages        = {99--124},
 doi          = {10.1016/0168-0072(91)90067-V},
)
@inproceedings(mohring93,
 author       = {Paulin-Mohring, Christine},
 year         = {1993},
 title        = {Inductive Definitions in the System Coq - Rules and Properties},
 booktitle    = {Proceedings of the International Conference on Typed Lambda Calculi and Applications},
 series       = {TLCA '93},
 publisher    = {Springer-Verlag},
 address      = {London, UK, UK},
 pages        = {328--345},
 doi          = {10.1007/BFb0037116},
)
@inproceedings(pfenning88,
 author       = {Frank Pfenning and Conal Elliott},
 year         = {1988},
 title        = {{Higher-Order Abstract Syntax}},
 editor       = {Richard L. Wexelblat},
 booktitle    = {Proceedings of the {ACM} SIGPLAN'88 Conference on Programming Language Design and Implementation (PLDI), Atlanta, Georgia, USA, June 22-24, 1988},
 publisher    = {{ACM}},
 pages        = {199--208},
 doi          = {10.1145/53990.54010},
)
@inproceedings(pfenning89,
 author       = {Frank Pfenning and Paulin-Mohring, Christine},
 year         = {1989},
 title        = {Inductively Defined Types in the {Calculus of Constructions}},
 editor       = {M. Main and A. Melton and M. Mislove and D. Schmidt},
 booktitle    = {Proceedings of the Fifth Conference on the Mathematical Foundations of Programming Semantics, Tulane University, New Orleans, Louisiana},
 publisher    = {Springer-Verlag LNCS 442},
 pages        = {209--228},
 doi          = {10.1007/BFb0040259},
)
@article(pierce+00,
 author       = {Benjamin C. Pierce and David N. Turner},
 year         = {2000},
 title        = {Local type inference},
 journal      = {{ACM} Trans. Program. Lang. Syst.},
 volume       = {22},
 number       = {1},
 pages        = {1--44},
 doi          = {10.1145/345099.345100},
)
@inproceedings(reynolds74,
 author       = {John C. Reynolds},
 year         = {1974},
 title        = {Towards a theory of type structure},
 editor       = {Bernard Robinet},
 booktitle    = {Programming Symposium, Proceedings Colloque sur la Programmation, Paris, France, April 9-11, 1974},
 series       = {Lecture Notes in Computer Science},
 volume       = {19},
 publisher    = {Springer},
 pages        = {408--423},
 doi          = {10.1007/3-540-06859-7_148},
)
@inproceedings(reynolds83,
 author       = {John C. Reynolds},
 year         = {1983},
 title        = {{Types, Abstraction and Parametric Polymorphism}},
 booktitle    = {{IFIP} Congress},
 pages        = {513--523},
)
@article(schurmann+01,
 author       = {Carsten Sch{\"{u}}rmann and Jo{\"{e}}lle Despeyroux and Frank Pfenning},
 year         = {2001},
 title        = {Primitive recursion for higher-order abstract syntax},
 journal      = {Theor. Comput. Sci.},
 volume       = {266},
 number       = {1-2},
 pages        = {1--57},
 doi          = {10.1016/S0304-3975(00)00418-7},
)
@article(selinger02,
 author       = {Peter Selinger},
 year         = {2002},
 title        = {The lambda calculus is algebraic},
 journal      = {J. Funct. Program.},
 volume       = {12},
 number       = {6},
 pages        = {549--566},
 doi          = {10.1017/S0956796801004294},
)
@article(stump17a,
 author       = {Aaron Stump},
 year         = {2017},
 title        = {The calculus of dependent lambda eliminations},
 journal      = {Journal of Functional Programming},
 volume       = {27},
 pages        = {e14},
 doi          = {10.1017/S0956796817000053},
)
@article(stump18,
 author       = {Aaron Stump},
 year         = {2018},
 title        = {From realizability to induction via dependent intersection},
 journal      = {Ann. Pure Appl. Logic},
 volume       = {169},
 number       = {7},
 pages        = {637--655},
 doi          = {10.1016/j.apal.2018.03.002},
)
@article(stump18b,
 author       = {Aaron Stump},
 year         = {2018},
 title        = {Syntax and Semantics of Cedille},
 journal      = {CoRR},
 volume       = {abs/1806.04709},
 url          = {http://arxiv.org/abs/1806.04709},
)
@article(stump18c,
 author       = {Aaron Stump},
 year         = {2018},
 title        = {Syntax and Typing for Cedille Core},
 journal      = {CoRR},
 volume       = {abs/1811.01318},
 url          = {http://arxiv.org/abs/1811.01318},
)
@article(stump16,
 author       = {Aaron Stump and Peng Fu},
 year         = {2016},
 title        = {Efficiency of lambda-encodings in total type theory},
 journal      = {Journal of Functional Programming},
 volume       = {26},
 doi          = {10.1017/S0956796816000034},
)
@manual(agda,
 author       = {The Agda development team},
 year         = {2016},
 title        = {Agda},
 url          = {http://wiki.portal.chalmers.se/agda/pmwiki.php},
 note         = {Version 2.5.1},
)
@manual(coq,
 author       = {{The Coq development team}},
 year         = {2016},
 title        = {The Coq proof assistant reference manual},
 organization = {LogiCal Project},
 url          = {http://coq.inria.fr},
 note         = {Version 8.5},
)
@manual(wadler90,
 author       = {Philip Wadler},
 year         = {1990},
 title        = {Recursive types for free!},
 url          = {http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt},
)
@article(washburn08,
 author       = {Geoffrey Washburn and Stephanie Weirich},
 year         = {2008},
 title        = {Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism},
 journal      = {J. Funct. Program.},
 volume       = {18},
 number       = {1},
 pages        = {87--140},
 doi          = {10.1017/S0956796807006557},
)
@article(Wells99,
 author       = {J. B. Wells},
 year         = {1999},
 title        = {Typability and Type Checking in System {F} are Equivalent and Undecidable},
 journal      = {Ann. Pure Appl. Logic},
 volume       = {98},
 number       = {1-3},
 pages        = {111--156},
 doi          = {10.1016/S0168-0072(98)00047-5},
)
@phdthesis(werner94,
 author       = {Benjamin Werner},
 year         = {1994},
 title        = {{Une Th{\'e}orie des Constructions Inductives}},
 school       = {{Universit{\'e} Paris-Diderot - Paris VII}},
 url          = {https://tel.archives-ouvertes.fr/tel-00196524},
)
@article(wiedijk12,
 author       = {Freek Wiedijk},
 year         = {2012},
 title        = {Pollack-inconsistency},
 journal      = {Electr. Notes Theor. Comput. Sci.},
 volume       = {285},
 pages        = {85--100},
 doi          = {10.1016/j.entcs.2012.06.008},
)