Skip to content

Latest commit

 

History

History
68 lines (48 loc) · 2.59 KB

bibliography.md

File metadata and controls

68 lines (48 loc) · 2.59 KB
Raw

Unification and metavariables

  • Cockx, Jesper. "Dependent Pattern Matching and Proof-Relevant Unification." (2017).

  • Norell, Ulf, and Catarina Coquand. "Type checking in the presence of meta-variables." Submitted to Typed Lambda Calculi and Applications (2007).

  • Abel, Andreas, and Brigitte Pientka. "Higher-order dynamic pattern unification for dependent types and records." Typed Lambda Calculi and Applications (2011): 10-26.

  • Mazzoli, Francesco, and Andreas Abel. "Type checking through unification." arXiv preprint arXiv:1609.09709 (2016).

Modules

  • Lillibridge, Mark. Translucent sums: A foundation for higher-order module systems. Diss. Carnegie Mellon University, 1997.

  • Xavier Leroy. Manifest types, modules, and separate compilation. In Proceedings of the Twenty-first Annual ACM Symposium on Principles of Programming Languages, Portland, pages 109–122. ACM, January 1994.

  • Leroy, Xavier. "A modular module system." Journal of Functional Programming 10.3 (2000): 269-303.

  • Coquand, Thierry, Randy Pollack, and Makoto Takeyama. "A logical framework with dependently typed records." International Conference on Typed Lambda Calculi and Applications. Springer, Berlin, Heidelberg, 2003.

Subtyping and singletons

  • Aspinall, David. "Subtyping with singleton types." International Workshop on Computer Science Logic. Springer, Berlin, Heidelberg, 1994.

  • Aspinall, David, and Adriana Compagnoni. "Subtyping dependent types." Logic in Computer Science, 1996. LICS'96. Proceedings., Eleventh Annual IEEE Symposium on. IEEE, 1996.

  • Abel, Andreas, Thierry Coquand, and Miguel Pagano. "A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance." TLCA. Vol. 5608. 2009.

  • Fridlender, Daniel, and Miguel Pagano. "A type-checking algorithm for Martin-Löf type theory with subtyping based on normalisation by evaluation." International Conference on Typed Lambda Calculi and Applications. Springer, Berlin, Heidelberg, 2013.

Parametric and irrelevant quantifiers

  • The Syntax and Semantics of Quantitative Type Theory, Bob Atkey, Under submission.

  • McBride, Conor. "I got plenty o’nuttin’." A List of Successes That Can Change the World. Springer International Publishing, 2016. 207-233.

  • Nuyts, Andreas, Andrea Vezzosi, and Dominique Devriese. "Parametric quantifiers for dependent type theory." Proceedings of the ACM on functional programming. Vol. 1. No. ICFP. 2017.

  • Abel, Andreas, and Gabriel Scherer. "On irrelevance and algorithmic equality in predicative type theory." arXiv preprint arXiv:1203.4716 (2012).