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