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.
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.
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.
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.
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.
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.
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.
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.
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.
Robert Constable & the PRL group (1986):
Implementing Mathematics with the Nuprl Proof Development System.
Prentice-Hall.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Thomas Streicher (1993):
Investigations into Intensional Type Theory.
Habilitation Thesis, Ludwig Maximilian Universität.
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.
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.
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.
Dimitrios Vytiniotis & Simon Peyton-Jones (2011):
Practical aspects of evidence-based compilation in System FC.
Unpublished.
Dimitrios Vytiniotis & Stephanie Weirich (2007):
Dependent types: Easy as PIE.
In: 8th Symposium on Trends in Functional Programming,
doi:10.1.1.81.4449.
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.
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.