@inproceedings(abel:fossacs11,
 author       = "Andreas Abel",
 year         = "2011",
 title        = "Irrelevance in Type Theory with a Heterogeneous Equality Judgement",
 booktitle    = "14th international conference on Foundations of Software Science and Computational Structures (FOSSACS 2011)",
 series       = "LNCS",
 volume       = "6604",
 publisher    = "Springer",
 pages        = "57--71",
 doi          = "10.1007/978-3-642-19805-2\_5",
)
@article(alti:pisigma-new,
 author       = "Thorsten Altenkirch and Nils Anders Danielsson and Andres L\"oh and Nicolas Oury",
 year         = "2010",
 title        = "{$\Pi $}{$\Sigma $}: Dependent Types Without the Sugar",
 journal      = "Functional and Logic Programming",
 pages        = "40--55",
 doi          = "10.1007/978-3-642-12251-4\_5",
)
@inproceedings(alti:ott-conf,
 author       = "Thorsten Altenkirch and Conor Mc{B}ride and Wouter Swierstra",
 year         = "2007",
 title        = "Observational equality, now!",
 booktitle    = "PLPV '07: Proceedings of the 2007 workshop on Programming Languages meets Program Verification",
 publisher    = "ACM",
 pages        = "57--68",
 doi          = "10.1145/1292597.1292608",
)
@inproceedings(augustsson98,
 author       = "Lennart Augustsson",
 year         = "1998",
 title        = "Cayenne -- a Language With Dependent Types",
 booktitle    = "ICFP '98: Proceedings of the 3rd ACM SIGPLAN international conference on Functional Programming",
 publisher    = "ACM",
 pages        = "239--250",
 doi          = "10.1145/289423.289451",
)
@incollection(Bar84,
 author       = "Henk P. Barendregt",
 year         = "1984",
 title        = "The Lambda Calculus: Its Syntax and Semantics",
 editor       = "J. Barwise and D. Kaplan and H. J. Keisler and P. Suppes and A.S. Troelstra",
 booktitle    = "Studies in Logic and the Foundation of Mathematics",
 volume       = "103",
 publisher    = "North-Holland",
)
@inproceedings(Barendregt92lambdacalculi,
 author       = "Henk P. 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",
 publisher    = "Oxford University Press",
 pages        = "117--309",
)
@inproceedings(barras+08,
 author       = "Bruno Barras and Bruno Bernardo",
 year         = "2008",
 title        = "{The Implicit Calculus of Constructions as a Programming Language with Dependent Types}",
 booktitle    = "11th international conference on Foundations of Software Science and Computational Structures (FOSSACS 2008)",
 series       = "LNCS",
 volume       = "4962",
 publisher    = "Springer",
 pages        = "365--379",
 doi          = "10.1007/978-3-540-78499-9\_26",
)
@inproceedings(Brady04inductivefamilies,
 author       = "Edwin Brady and Conor Mc{B}ride and James Mc{K}inna",
 year         = "2004",
 title        = "Inductive families need not store their indices",
 booktitle    = "Types for Proofs and Programs: International Workshop (TYPES 2003)",
 series       = "LNCS",
 volume       = "3085",
 publisher    = "Springer",
 pages        = "115--129",
 doi          = "10.1007/978-3-540-24849-1\_8",
)
@techreport(Cardelli86apolymorphic,
 author       = "Luca Cardelli",
 year         = "1986",
 title        = "A Polymorphic lambda-calculus with Type:Type",
 type         = "Technical Report",
 institution  = "DEC SRC, 130 Lytton Avenue, Palo Alto, CA 94301. May. SRC Research Report",
)
@misc(chlipala:cpdt,
 author       = "Adam Chlipala",
 year         = "2011",
 title        = "Certified programming with dependent types",
 url          = "http://adam.chlipala.net/cpdt",
)
@book(nuprl,
 author       = "Robert Constable and the PRL group",
 year         = "1986",
 title        = "{Implementing Mathematics with the Nuprl Proof Development System}",
 publisher    = "Prentice-Hall",
)
@inproceedings(jia+08,
 author       = "Limin Jia and Jeffrey A. Vaughan and Karl Mazurak and Jianzhou Zhao and Luke Zarko and Joseph Schorr and Steve Zdancewic",
 year         = "2008",
 title        = "{AURA}: {A} Programming Language for Authorization and Audit",
 booktitle    = "ICFP '08:Proceedings of the 13th ACM SIGPLAN international conference on Functional Programming)",
 pages        = "27--38",
 doi          = "10.1145/1411204.1411212",
)
@inproceedings(jia:lambdaeek,
 author       = "Limin Jia and Jianzhou Zhao and Vilhelm Sj\"{o}berg and Stephanie Weirich",
 year         = "2010",
 title        = "Dependent types and program equivalence",
 booktitle    = "POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages",
 pages        = "275--286",
 doi          = "10.1145/1706299.1706333",
)
@techreport(licata:dml,
 author       = "Daniel R. Licata and Robert Harper",
 year         = "2005",
 title        = "A Formulation of Dependent ML with Explicit Equality Proofs",
 type         = "Technical Report",
 number       = "CMU-CS-05-178",
 institution  = "Carnegie Mellon University Department of Computer Science",
)
@inproceedings(mcbride:motive,
 author       = "Conor Mc{B}ride",
 year         = "2002",
 title        = "{E}limination with a {M}otive",
 booktitle    = "Types for {P}roofs and {P}rograms: International Workshop (TYPES 2000)",
 series       = "LNCS",
 volume       = "2277",
 publisher    = "Springer",
 pages        = "197--216",
 doi          = "10.1007/3-540-45842-5\_13",
)
@inproceedings(Miquel01theimplicit,
 author       = "Alexandre Miquel",
 year         = "2001",
 title        = "The Implicit Calculus of Constructions - Extending Pure Type Systems with an Intersection Type Binder and Subtyping",
 booktitle    = "TLCA '01: Proceeding of 5th international conference on Typed Lambda Calculi and Applications",
 series       = "LNCS",
 volume       = "2044",
 publisher    = "Springer",
 pages        = "344--359",
 doi          = "10.1007/3-540-45413-6\_27",
)
@inproceedings(mishra-linger+08,
 author       = "Nathan Mishra-Linger and Tim Sheard",
 year         = "2008",
 title        = "{Erasure and Polymorphism in Pure Type Systems}",
 booktitle    = "11th international conference on Foundations of Software Science and Computational Structures (FOSSACS 2008)",
 series       = "LNCS",
 volume       = "4962",
 publisher    = "Springer",
 pages        = "350--364",
 doi          = "10.1007/978-3-540-78499-9\_25",
)
@inproceedings(ou:dependent,
 author       = "Xinming Ou and Gang Tan and Yitzhak Mandelbaum and David Walker",
 year         = "2004",
 title        = "Dynamic typing with dependent types",
 booktitle    = "{IFIP} International Conference on Theoretical Computer Science",
 pages        = "437--450",
 doi          = "10.1007/1-4020-8141-3\_34",
)
@inproceedings(pj-vytiniotis:wobbly,
 author       = "Simon {Peyton-Jones} and Dimitrios Vytiniotis and Stephanie Weirich and Geoffrey Washburn",
 year         = "2006",
 title        = "Simple unification-based type inference for {GADTs}",
 booktitle    = "ICFP '06: Proceedings of the 11th ACM SIGPLAN international conference on Functional Programming",
 pages        = "50--61",
 doi          = "10.1145/1159803.1159811",
)
@inproceedings(pfenning01,
 author       = "Frank Pfenning",
 year         = "2001",
 title        = "Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory",
 booktitle    = "Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS)",
 pages        = "221--230",
 doi          = "10.1109/LICS.2001.932499",
)
@techreport(reed:irrelevance,
 author       = "Jason Reed",
 year         = "2002",
 title        = "Proof irrelevance and strict definitions in a logical framework",
 type         = "Technical Report",
 institution  = "Carnegie-Mellon University",
 note         = "Senior Thesis, published as technical report CMU-CS-02-153",
)
@inproceedings(sheard,
 author       = "Tim Sheard",
 year         = "2006",
 title        = "Type-level Computation Using Narrowing in {$\Omega $}omega.",
 booktitle    = "PLPV '06: Proceedings of the 1st workshop on Programming Languages meets Program Verification",
 pages        = "105--128",
 doi          = "10.1016/j.entcs.2006.10.040",
)
@inproceedings(sjoberg:quasi,
 author       = "Vilhelm Sj\"{o}berg and Aaron Stump",
 year         = "2010",
 title        = "Equality, Quasi-Implicit Products, and Large Eliminations",
 booktitle    = "ITRS 2010: Proceedings of the 5th workshop on Intersection Types and Related Systems",
 doi          = "10.4204/EPTCS.45.7",
)
@misc(streicher:iiitt,
 author       = "Thomas Streicher",
 year         = "1993",
 title        = "Investigations into Intensional Type Theory",
 note         = "Habilitation Thesis, Ludwig Maximilian Universit\"at",
)
@inproceedings(guru09,
 author       = "Aaron Stump and Morgan Deters and Adam Petcher and Todd Schiller and Timothy Simpson",
 year         = "2009",
 title        = "Verified Programming in Guru",
 booktitle    = "PLPV '09: Proceedings of the 3rd workshop on Programming Languages meets Program Verification",
 pages        = "49--58",
 doi          = "10.1145/1481848.1481856",
)
@inproceedings(sulzmann-fc,
 author       = "Martin Sulzmann and Manuel M. T. Chakravarty and Simon {Peyton-Jones} and Kevin Donnelly",
 year         = "2007",
 title        = "System F with type equality coercions",
 booktitle    = "TLDI 07: Proceedings of the 2007 ACM SIGPLAN international workshop on Types in Languages Design and Implementation",
 publisher    = "ACM",
 pages        = "53--66",
 doi          = "10.1145/1190315.1190324",
)
@inproceedings(swamy-fstar,
 author       = "Nikhil Swamy and Juan Chen and C{\'e}dric Fournet and Pierre-Yves Strub and Karthikeyan Bhargavan and Jean Yang",
 year         = "2011",
 title        = "{Secure Distributed Programming with Value-dependent Types}",
 booktitle    = "ICFP '11: Proceedings of the 16th ACM SIGPLAN international conference on Functional Programming",
 publisher    = "ACM",
 pages        = "285--296",
 doi          = "10.1145/2034574.2034811",
)
@misc(vytiniotis-practical11,
 author       = "Dimitrios Vytiniotis and Simon {Peyton-Jones}",
 year         = "2011",
 title        = "Practical aspects of evidence-based compilation in {S}ystem {F}{C}",
 note         = "Unpublished",
)
@inproceedings(vytiniotis:pie,
 author       = "Dimitrios Vytiniotis and Stephanie Weirich",
 year         = "2007",
 title        = "Dependent types: Easy as {PIE}",
 booktitle    = "8th Symposium on Trends in Functional Programming",
 doi          = "10.1.1.81.4449",
)
@incollection(xi:ats,
 author       = "Hongwei Xi",
 year         = "2004",
 title        = "Applied Type System",
 booktitle    = "Types for Proofs and Programs: International Workshop (TYPES 2003)",
 series       = "LNCS",
 volume       = "3085",
 publisher    = "Springer",
 pages        = "394--408",
 doi          = "10.1007/978-3-540-24849-1\_25",
)
@inproceedings(XP98,
 author       = "Hongwei Xi and Frank Pfenning",
 year         = "1999",
 title        = "Dependent Types in Practical Programming",
 booktitle    = "POPL '99: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages",
 pages        = "214--227",
 doi          = "10.1145/292540.292560",
)