References

  1. Andreas Abel (2011): Irrelevance in Type Theory with a Heterogeneous Equality Judgement. In: 14th international conference on Foundations of Software Science and Computational Structures (FOSSACS 2011), LNCS 6604. Springer, pp. 57–71, doi:10.1007/978-3-642-19805-2_5.
  2. Thorsten Altenkirch, Nils Anders Danielsson, Andres Löh & Nicolas Oury (2010): ΠΣ: Dependent Types Without the Sugar. Functional and Logic Programming, pp. 40–55, doi:10.1007/978-3-642-12251-4_5.
  3. Thorsten Altenkirch, Conor McBride & Wouter Swierstra (2007): Observational equality, now!. In: PLPV '07: Proceedings of the 2007 workshop on Programming Languages meets Program Verification. ACM, pp. 57–68, doi:10.1145/1292597.1292608.
  4. Lennart Augustsson (1998): Cayenne – a Language With Dependent Types. In: ICFP '98: Proceedings of the 3rd ACM SIGPLAN international conference on Functional Programming. ACM, pp. 239–250, doi:10.1145/289423.289451.
  5. Henk P. Barendregt (1984): The Lambda Calculus: Its Syntax and Semantics. In: J. Barwise, D. Kaplan, H. J. Keisler, P. Suppes & A.S. Troelstra: Studies in Logic and the Foundation of Mathematics 103. North-Holland.
  6. Henk P. Barendregt (1992): Lambda Calculi with Types. In: S. Abramsky, D. M. Gabbay & T. S. E. Maibaum: Handbook of Logic in Computer Science. Oxford University Press, pp. 117–309.
  7. Bruno Barras & Bruno Bernardo (2008): The Implicit Calculus of Constructions as a Programming Language with Dependent Types. In: 11th international conference on Foundations of Software Science and Computational Structures (FOSSACS 2008), LNCS 4962. Springer, pp. 365–379, doi:10.1007/978-3-540-78499-9_26.
  8. Edwin Brady, Conor McBride & James McKinna (2004): Inductive families need not store their indices. In: Types for Proofs and Programs: International Workshop (TYPES 2003), LNCS 3085. Springer, pp. 115–129, doi:10.1007/978-3-540-24849-1_8.
  9. Luca Cardelli (1986): A Polymorphic lambda-calculus with Type:Type. Technical Report. DEC SRC, 130 Lytton Avenue, Palo Alto, CA 94301. May. SRC Research Report.
  10. Adam Chlipala (2011): Certified programming with dependent types. Available at http://adam.chlipala.net/cpdt.
  11. Robert Constable & the PRL group (1986): Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall.
  12. Limin Jia, Jeffrey A. Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph Schorr & Steve Zdancewic (2008): AURA: A Programming Language for Authorization and Audit. In: ICFP '08:Proceedings of the 13th ACM SIGPLAN international conference on Functional Programming), pp. 27–38, doi:10.1145/1411204.1411212.
  13. Limin Jia, Jianzhou Zhao, Vilhelm Sjöberg & Stephanie Weirich (2010): Dependent types and program equivalence. In: POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pp. 275–286, doi:10.1145/1706299.1706333.
  14. Daniel R. Licata & Robert Harper (2005): A Formulation of Dependent ML with Explicit Equality Proofs. Technical Report CMU-CS-05-178. Carnegie Mellon University Department of Computer Science.
  15. Conor McBride (2002): Elimination with a Motive. In: Types for Proofs and Programs: International Workshop (TYPES 2000), LNCS 2277. Springer, pp. 197–216, doi:10.1007/3-540-45842-5_13.
  16. Alexandre Miquel (2001): The Implicit Calculus of Constructions - Extending Pure Type Systems with an Intersection Type Binder and Subtyping. In: TLCA '01: Proceeding of 5th international conference on Typed Lambda Calculi and Applications, LNCS 2044. Springer, pp. 344–359, doi:10.1007/3-540-45413-6_27.
  17. Nathan Mishra-Linger & Tim Sheard (2008): Erasure and Polymorphism in Pure Type Systems. In: 11th international conference on Foundations of Software Science and Computational Structures (FOSSACS 2008), LNCS 4962. Springer, pp. 350–364, doi:10.1007/978-3-540-78499-9_25.
  18. Xinming Ou, Gang Tan, Yitzhak Mandelbaum & David Walker (2004): Dynamic typing with dependent types. In: IFIP International Conference on Theoretical Computer Science, pp. 437–450, doi:10.1007/1-4020-8141-3_34.
  19. Simon Peyton-Jones, Dimitrios Vytiniotis, Stephanie Weirich & Geoffrey Washburn (2006): Simple unification-based type inference for GADTs. In: ICFP '06: Proceedings of the 11th ACM SIGPLAN international conference on Functional Programming, pp. 50–61, doi:10.1145/1159803.1159811.
  20. Frank Pfenning (2001): Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory. In: Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS), pp. 221–230, doi:10.1109/LICS.2001.932499.
  21. Jason Reed (2002): Proof irrelevance and strict definitions in a logical framework. Technical Report. Carnegie-Mellon University. Senior Thesis, published as technical report CMU-CS-02-153.
  22. Tim Sheard (2006): Type-level Computation Using Narrowing in Ωomega.. In: PLPV '06: Proceedings of the 1st workshop on Programming Languages meets Program Verification, pp. 105–128, doi:10.1016/j.entcs.2006.10.040.
  23. Vilhelm Sjöberg & Aaron Stump (2010): Equality, Quasi-Implicit Products, and Large Eliminations. In: ITRS 2010: Proceedings of the 5th workshop on Intersection Types and Related Systems, doi:10.4204/EPTCS.45.7.
  24. Thomas Streicher (1993): Investigations into Intensional Type Theory. Habilitation Thesis, Ludwig Maximilian Universität.
  25. Aaron Stump, Morgan Deters, Adam Petcher, Todd Schiller & Timothy Simpson (2009): Verified Programming in Guru. In: PLPV '09: Proceedings of the 3rd workshop on Programming Languages meets Program Verification, pp. 49–58, doi:10.1145/1481848.1481856.
  26. Martin Sulzmann, Manuel M. T. Chakravarty, Simon Peyton-Jones & Kevin Donnelly (2007): System F with type equality coercions. In: TLDI 07: Proceedings of the 2007 ACM SIGPLAN international workshop on Types in Languages Design and Implementation. ACM, pp. 53–66, doi:10.1145/1190315.1190324.
  27. Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan & Jean Yang (2011): Secure Distributed Programming with Value-dependent Types. In: ICFP '11: Proceedings of the 16th ACM SIGPLAN international conference on Functional Programming. ACM, pp. 285–296, doi:10.1145/2034574.2034811.
  28. Dimitrios Vytiniotis & Simon Peyton-Jones (2011): Practical aspects of evidence-based compilation in System FC. Unpublished.
  29. Dimitrios Vytiniotis & Stephanie Weirich (2007): Dependent types: Easy as PIE. In: 8th Symposium on Trends in Functional Programming, doi:10.1.1.81.4449.
  30. Hongwei Xi (2004): Applied Type System. In: Types for Proofs and Programs: International Workshop (TYPES 2003), LNCS 3085. Springer, pp. 394–408, doi:10.1007/978-3-540-24849-1_25.
  31. Hongwei Xi & Frank Pfenning (1999): Dependent Types in Practical Programming. In: POPL '99: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pp. 214–227, doi:10.1145/292540.292560.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org