)
 author       = "1",
@unknown(altenkirch+07,
 author       = "T. Altenkirch and C. McBride and W. Swierstra",
 year         = "2007",
 title        = "{Observational Equality, Now!}",
 editor       = "A. Stump and H. Xi",
 booktitle    = "PLPV '07: Proceedings of the 2007 Workshop on Programming Languages meets Program Verification",
 pages        = "57--68",
)
@unknown(barras+08,
 author       = "B. Barras and B. Bernardo",
 year         = "2008",
 title        = "{The Implicit Calculus of Constructions as a Programming Language with Dependent Types}",
 editor       = "Roberto M. Amadio",
 booktitle    = "Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008",
 series       = "Lecture Notes in Computer Science",
 volume       = "4962",
 publisher    = "Springer",
 pages        = "365--379",
)
@unknown(C86,
 author       = "R. Constable and the PRL group",
 year         = "1986",
 title        = "{Implementing Mathematics with the Nuprl Proof Development System}",
 publisher    = "Prentice-Hall",
)
@unknown(CoppoDezani78,
 author       = "M. Coppo1 and M. Dezani-Ciancaglini",
 year         = "1978",
 title        = "A New Type Assignment for {$\lambda $}-terms",
 journal      = "Archiv. Math. Logik",
 volume       = "19",
 number       = "1",
 pages        = "139--156",
)
@unknown(HHP93,
 author       = "R. Harper and F. Honsell and G. Plotkin",
 year         = "1993",
 title        = "{A Framework for Defining Logics}",
 journal      = "Journal of the Association for Computing Machinery",
 volume       = "40",
 number       = "1",
 pages        = "143--184",
)
@unknown(ml84,
 author       = "P. Martin-L{\"o}f",
 year         = "1984",
 title        = "Intuitionistic Type Theory",
 publisher    = "Bibliopolis",
)
@unknown(mcbride99,
 author       = "C. McBride",
 year         = "1999",
 title        = "{Dependently Typed Functional Programs and Their Proofs}",
 type         = "Ph.D. thesis",
 school       = "University of Edinburgh",
)
@unknown(miquel01,
 author       = "A. Miquel",
 year         = "2001",
 title        = "{The Implicit Calculus of Constructions}",
 booktitle    = "Typed Lambda Calculi and Applications",
 series       = "Lecture Notes in Computer Science",
 volume       = "2044",
 publisher    = "Springer",
 pages        = "344--359",
)
@unknown(mishra-linger+08,
 author       = "N. Mishra-Linger and T. Sheard",
 year         = "2008",
 title        = "{Erasure and Polymorphism in Pure Type Systems}",
 editor       = "Roberto M. Amadio",
 booktitle    = "Foundations of Software Science and Computational Structures, 11th International Conference (FOSSACS)",
 series       = "Lecture Notes in Computer Science",
 volume       = "4962",
 publisher    = "Springer",
 pages        = "350--364",
)
@unknown(guru09,
 author       = "A. Stump and M. Deters and A. Petcher and T. Schiller and T. Simpson",
 year         = "2009",
 title        = "{Verified Programming in Guru}",
 editor       = "T. Altenkirch and T. Millstein",
 booktitle    = "Programming Languges meets Program Verification (PLPV)",
 pages        = "49--58",
)