Computational higher-dimensional type theory

Abstract

Formal constructive type theory has proved to be an effective language for mechanized proof. By avoiding non-constructive principles, such as the law of the excluded middle, type theory admits sharper proofs and broader interpretations of results. From a computer science perspective, interest in type theory arises from its applications to programming languages. Standard constructive type theories used in mechanization admit computational interpretations based on meta-mathematical normalization theorems. These proofs are notoriously brittle; any change to the theory potentially invalidates its computational meaning. As a case in point, Voevodsky's univalence axiom raises questions about the computational meaning of proofs.

We consider the question: Can higher-dimensional type theory be construed as a programming language? We answer this question affirmatively by providing a direct, deterministic operational interpretation for a representative higher-dimensional dependent type theory with higher inductive types and an instance of univalence. Rather than being a formal type theory defined by rules, it is instead a computational type theory in the sense of Martin-Löf's meaning explanations and of the NuPRL semantics. The definition of the type theory starts with programs; types are specifications of program behavior. The main result is a canonicity theorem stating that closed programs of boolean type evaluate to true or false.

References

1. S. F. Allen. A Non-Type-Theoretic Semantics for Type-Theoretic Language. PhD thesis, Cornell University, 1987.
2. S. F. Allen, M. Bickford, R. L. Constable, R. Eaton, C. Kreitz, L. Lorigo, and E. Moran. Innovations in computational type theory using Nuprl. Journal of Applied Logic, 4(4):428–469, 2006.
3. T. Altenkirch, C. McBride, and W. Swierstra. Observational equality, now! In Proceedings of the 2007 Workshop on Programming Languages Meets Program Verification, PLPV ’07, pages 57–68, New York, NY, USA, 2007. ACM. ISBN 978-1-59593-677-6.
4. C. Angiuli and R. Harper. Computational higher type theory II: Dependent cubical realizability. Preprint, June 2016.
5. C. Angiuli, R. Harper, and T. Wilson. Computational higher type theory I: Abstract cubical realizability. Preprint, April 2016.
6. C. Angiuli, E. Morehouse, D. R. Licata, and R. Harper. Homotopical patch theory. Journal of Functional Programming, 26, Jan 2016.
8. S. Awodey and M. A. Warren. Homotopy theoretic models of identity types. Mathematical Proceedings of the Cambridge Philosophical Society, 146(1):45–55, Jan. 2009. ISSN 0305-0041.
9. M. Bezem, T. Coquand, and S. Huber. A model of type theory in cubical sets. In 19th International Conference on Types for Proofs and Programs (TYPES 2013), volume 26 of Leibniz International Proceedings in Informatics (LIPIcs), pages 107–128, Dagstuhl, Germany, 2014. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.
10. L. Birkedal, A. Bizjak, R. Clouston, H. B. Grathwohl, B. Spitters, and A. Vezzosi. Guarded cubical type theory: Path equality for guarded recursion. Preprint, June 2016.
11. C. Cohen, T. Coquand, S. Huber, and A. Mörtberg. Cubical type theory: a constructive interpretation of the univalence axiom. In 21st International Conference on Types for Proofs and Programs (TYPES 2015), Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany, 2016. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. To appear.
12. R. L. Constable. Constructive mathematics as a programming logic I: Some principles of theory. In Annals of Mathematics, volume 24, pages 21–37. Elsevier Science Publishers, B.V. (North-Holland), 1985. Reprinted from Topics in the Theory of Computation, Selected Papers of the International Conference on Foundations of Computation Theory, FCT ’83.
13. R. L. Constable and N. P. Mendler. Recursive definitions in type theory. In Proceedings of the Logics of Programming Conference, pages 61–78, Jan. 1985. Cornell TR 85–659.
14. R. L. Constable and S. F. Smith. Computational foundations of basic recursive function theory. Theoretical Comput. Sci., 121(1&2):89– 112, Dec. 1993.
15. R. L. Constable, et al. Implementing Mathematics with the Nuprl Proof Development Environment. Prentice-Hall, 1985.
16. B. A. Davey and H. A. Priestley. Introduction to lattices and order. Cambridge University Press, Cambridge, UK, 2002. ISBN 0-521- 78451-4.
17. M. Escardo and T. Streicher. The intrinsic topology of Martin-Löf universes. To appear, Annals of Pure and Applied Logic, Feb. 2016.
18. N. Gambino and C. Sattler. Uniform fibrations and the Frobenius condition. Preprint, Oct 2015.
19. M. Grandis and W. Tholen. Natural weak factorization systems. Archivum Mathematicum, 042(4):397–408, 2006.
20. R. Harper. Constructing type systems over an operational semantics. J. Symb. Comput., 14(1):71–84, July 1992. ISSN 0747-7171.
21. R. Harper. Practical Foundations for Programming Languages. Cambridge University Press, second edition, 2016.
22. R. Harper and K.-B. (Favonia) Hou. A note on the uniform Kan condition in nominal cubical sets. Preprint, Jan 2015.
23. M. Hofmann and T. Streicher. The groupoid interpretation of type theory. In Twenty-five years of constructive type theory. Oxford University Press, 1998.
24. S. Huber. Cubical Interpretations of Type Theory. PhD thesis, University of Gothenburg, Expected November 2016.
25. D. M. Kan. Abstract homotopy. I. Proceedings of the National Academy of Sciences of the United States of America, 41(12):1092– 1096, 1955. ISSN 00278424.
26. D. R. Licata and G. Brunerie. A cubical type theory, November 2014.
27. D. R. Licata and G. Brunerie. A cubical approach to synthetic homotopy theory. In Proceedings of the 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), LICS ’15, pages 92–103, Washington, DC, USA, 2015. IEEE Computer Society. ISBN 978-1-4799-8875-4.
28. P. Martin-Löf. About models for intuitionistic type theories and the notion of definitional equality. In S. Kanger, editor, Proceedings of the Third Scandinavian Logic Symposium, volume 82 of Studies in Logic and the Foundations of Mathematics, pages 81– 109. Elsevier, 1975.
29. P. Martin-Löf. Constructive mathematics and computer programming. Philosophical Transactions of the Royal Society of London Series A, 312:501–518, Oct. 1984.
30. P. Martin-Löf. Intuitionistic type theory, volume 1 of Studies in Proof Theory. Bibliopolis, 1984. ISBN 88-7088-105-9. Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980.
31. P. Martin-Löf. Verificationism then and now. In M. van der Schaar, editor, Judgement and the Epistemic Foundation of Logic, volume 31 of Logic, Epistemology, and the Unity of Science, pages 3–14. Springer, 2013. ISBN 978-94-007-5136-1.
32. U. Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology, 2007.
33. A. M. Pitts. Nominal Sets: Names and Symmetry in Computer Science, volume 57 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2013. ISBN 9781107017788.
34. A. M. Pitts. Nominal Presentation of Cubical Sets Models of Type Theory. In H. Herbelin, P. Letouzey, and M. Sozeau, editors, 20th International Conference on Types for Proofs and Programs (TYPES 2014), volume 39 of Leibniz International Proceedings in Informatics (LIPIcs), pages 202–220, Dagstuhl, Germany, 2015. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. ISBN 978-3-939897- 88-0.
35. V. Rahli and M. Bickford. A nominal exploration of intuitionism. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016, pages 130–141, New York, NY, USA, 2016. ACM. ISBN 978-1-4503-4127-1.
36. V. Rahli and M. Bickford. Coq as a Metatheory for Nuprl with Bar Induction. Presented at Continuity, Computability, Constructivity – From Logic to Algorithms (CCC 2015), Sept 14, 2015.
37. M. Sipser. Introduction to the Theory of Computation, volume 2. Thomson Course Technology Boston, 2006.
38. J. Sterling, D. Gratzer, V. Rahli, D. Morrison, E. Akentyev, and A. Tosun. RedPRL – the People’s Refinement Logic. http://www. redprl.org/, 2016.
39. The Coq Project. The Coq proof assistant, 2016.
40. The NuPRL Project. Prl project, 2016.
41. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory. org/book, Institute for Advanced Study, 2013.
42. B. van den Berg and R. Garner. Types are weak ω-groupoids. Proceedings of the London Mathematical Society, 102(2):370–394, 2011.
43. V. Voevodsky. A very short note on homotopy λ-calculus, 09 2006.
44. V. Voevodsky. Univalent foundations of mathematics. In Logic, Language, Information and Computation - 18th International Workshop, WoLLIC 2011, Philadelphia, PA, USA, May 18-20, 2011. Proceedings, page 4, 2011.
45. V. Voevodsky. A simple type system with two identity types. Lecture notes, Feb. 2013.
46. V. Voevodsky. The UniMath project, 2016.
47. M. A. Warren. Homotopy theoretic aspects of constructive type theory. PhD thesis, Carnegie Mellon University, 2008.
48. R. Williamson. Combinatorial homotopy theory. Lecture notes, Oct 2012.

Index Terms

• Software and its engineering

  • Software notations and tools

    • Formal language definitions

• Theory of computation

  • Formal languages and automata theory

  • Semantics and reasoning

    • Program semantics