)
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",
)