A. Abel, and T. Altenkirch: A predicative analysis of structural recursion. Journal of Functional Programming 12.1, 2002. 1-41. L. Bachmair, and D. A. Plaisted, Termination orderings for associative-commutative rewriting systems. Journal of Symbolic Computation 1.4, 1985. 329-349. T. Coquand, Pattern matching with dependent types. Proceedings of the 1992 workshop on types for proofs and programs, Bastad, Sweden, ed. B. Nordstrom et al., 1992. 66-79. Available at www.cse.chalmers.se/research/group/logic/Types/proc92.ps (accessed 3 June, 2013). P. Dybjer, Inductive families. Formal Aspects of Computing 6.4, 1994. 440-465. H. Goguen, A typed operational semantics for type theory. PhD thesis, University of Edinburgh, 1994. G. Gonthier, Engineering mathematics: the odd order theorem proof. Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, Rome, Italy. New York: ACM, 2013. 1-2. H. Goguen, C. McBride, and J. McKinna, Eliminating dependent pattern matching. Algebra, Meaning, and Computation, ed. K. Futatsugi et al. (Lecture Notes in Computer Science, 4060). Berlin/Heidelberg: Springer, 2006. 521-540. A. Graf, Left-to-right tree pattern matching. Proceedings of the 4th international conference on rewriting techniques and applications, Como, Italy, ed. R.V. Book (Lecture Notes in Computer Science, 488). Berlin/Heidelberg: Springer, 1991. 323-334. C. S. Lee, N. D. Jones, and A. M. Ben-Amram, The size-change principle for program termination. ACM SIGPLAN Notices 36.3, 2001. 81-92. Z. Luo, Computation and reasoning: a type theory for computer science (International Series of Monographs on Computer Science, 11). New York/Oxford: Oxford University Press, Inc., 1994. C. McBride, Dependently typed functional programs and their proofs. PhD thesis, University of Edinburgh, 2000. C. McBride, H. Goguen, and J. McKinna, A few constructions on constructors. Types for Proofs and Programs, ed. J.-C. Filliatre et al. (Lecture Notes in Computer Science, 3839). Berlin/Heidelberg: Springer, 2006. 186-200. C. McBride, and J. McKinna, The view from the left. Journal of Functional Programming 14.1, 2004. 69-111. B. Nordstrom, K. Petersson, and J. M. Smith, Programming in Martin-Lof 's type theory (International Series of Monographs on Computer Science, 7). New York/Oxford: Oxford University Press, Inc., 1990. U. Norell, Towards a practical programming language based on dependent type theory. PhD Thesis, Chalmers University of Technology, 2007. E. Rijke, Homotopy type theory. Master Thesis, Utrecht University, 2012. M. Sozeau, Equations: A dependent pattern-matching compiler. Proceedings of the first international conference on interactive theorem proving, Edinburgh, UK, ed. M. Kaufmann et al. (Lecture Notes in Computer Science, 6172). Berlin/Heidelberg: Springer, 2010. 419-434. S. Thompson, Type theory and functional programming. Computing Laboratory, University of Kent, 1999. Available at http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ (accessed 3 June, 2013). D. Vytiniotis, T. Coquand, and D. Wahlstedt, Stop when you are Almost-Full. Proceedings of the third international conference on interactive theorem proving, Princeton, NJ, USA, ed. L. Beringer and A. Felty (Lecture Notes in Computer Science, 7406). Berlin/Heidelberg: Springer, 2012. 250-265. H. Xi, Dependently typed pattern matching. Journal of Universal Computer Science 9.8, 2003. 851-872.