Abstract
This project report presents Cedille, a dependent type theory based on lambda encodings. Cedille is an extension of the Calculus of Constructions with new type features enabling induction and large eliminations (computing a type by recursion on a term) for lambda encodings, which are not available for lambda-encoded data in related type theories. Cedille is presented through a number of examples, including both programs and proofs.
A. Guneratne and C. Reynolds are doctoral students.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Basold, H., Geuvers, H.: Type theory based on dependent inductive and coinductive types. In: Shankar, N. (ed.) IEEE Symposium on Logic in Computer Science (LICS) (2016)
Bezem, M., Coquand, T., Huber, S.: A model of type theory in cubical sets. In: Matthes, R., Schubert, A. (eds.) 19th International Conference on Types for Proofs and Programs, TYPES 2013 of LIPIcs, vol. 26, pp. 107–128. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2014)
Böhm, C., Berarducci, A.: Automatic synthesis of typed lambda-programs on term algebras. Theor. Comput. Sci. 39, 135–154 (1985)
Church, A.: The Calculi of Lambda Conversion. Princeton University Press, Princeton (1941). Ann. Math. Stud. (6)
Coquand, T., Huet, G.: The calculus of constructions. Inf. Comput. 76(2–3), 95–120 (1988)
Coquand, T., Paulin, C.: Inductively defined types. In: Martin-Löf, P., Mints, G. (eds.) COLOG 1988. LNCS, vol. 417, pp. 50–66. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52335-9_47
The Agda Development Team: Agda, Version 2.5.1 (2016)
Fortune, S., Leivant, D., O’Donnell, M.: The expressiveness of simple and second-order type structures. J. ACM 30(1), 151–185 (1983)
Geuvers, H.: Induction is not derivable in second order dependent type theory. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 166–181. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45413-6_16
Hofmann, M., Streicher, T.: The groupoid interpretation of type theory. In: Twenty-Five Years of Constructive Type Theory of Oxford Logic Guides, vol. 36, pp. 83–111. Oxford University Press, Oxford (1998)
Koopman, P., Plasmeijer, R., Jansen, J.M.: Church encoding of data types considered harmful for implementations. In: Plasmeijer, R., Tobin-Hochstadt, S. (eds.) 26th Symposium on Implementation and Application of Functional Languages (IFL) (2014). Presented version
Kopylov, A.: Dependent intersection: a new way of defining records in type theory. In: 18th IEEE Symposium on Logic in Computer Science (LICS), pp. 86–95 (2003)
Leivant, D.: Finitely stratified polymorphism. Inf. Comput. 93(1), 93–113 (1991)
Luo, Z.: An extended calculus of constructions. Ph.D. thesis (1990)
The Coq Development Team: The Coq Proof Assistant Reference Manual. LogiCal Project, Version 8.5 (2016)
McAllester, D.A.: Implementation and abstraction in mathematics. CoRR, abs/1407.7274 (2014)
McBride, C.: Elimination with a motive. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R., Pollack, R. (eds.) TYPES 2000. LNCS, vol. 2277, pp. 197–216. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45842-5_13
Miquel, A.: The implicit calculus of constructions extending pure type systems with an intersection type binder and subtyping. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 344–359. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45413-6_27
Parigot, M.: Programming with proofs: a second order type theory. In: Ganzinger, H. (ed.) ESOP 1988. LNCS, vol. 300, pp. 145–159. Springer, Heidelberg (1988). https://doi.org/10.1007/3-540-19027-9_10
Parigot, M.: On the representation of data in lambda-calculus. In: Börger, E., Büning, H.K., Richter, M.M. (eds.) CSL 1989. LNCS, vol. 440, pp. 309–321. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52753-2_47
Pierce, B.C., Turner, D.N.: Local type inference. ACM Trans. Program. Lang. Syst. 22(1), 1–44 (2000)
Stump, A.: From realizability to induction via dependent intersection. Available from the author’s web page, under review as of 19 June 2017
Stump, A.: The calculus of dependent lambda eliminations. J. Funct. Program. 27, e14 (2017)
Stump, A., Fu, P.: Efficiency of lambda-encodings in total type theory. J. Funct. Program. 26, e3 (31 p.) (2016)
The Univalent Foundations Program: Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study (2013). https://homotopytypetheory.org/book
Washburn, G., Weirich, S.: Boxes go bananas: encoding higher-order abstract syntax with parametric polymorphism. J. Funct. Program. 18(1), 87–140 (2008)
Werner, B.: Une Théorie des constructions inductives. Ph.D. thesis, Paris Diderot University, France (1994)
Acknowledgments
Thanks to the anonymous TFP 2016 pre-proceedings reviewer for helpful comments which helped improve the paper. This work has been supported by NSF on a grant titled “Lambda Encodings Reborn” (award 1524519), and through the DoD MURI project “Semantics, Formal Reasoning, and Tools for Quantum Programming” (award FA9550-16-1-0082). Thanks also to Matthew Heimerdinger and Richard Blair who made contributions to the tool summer 2016.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Guneratne, A., Reynolds, C., Stump, A. (2019). Project Report: Dependently Typed Programming with Lambda Encodings in Cedille. In: Van Horn, D., Hughes, J. (eds) Trends in Functional Programming. TFP 2016. Lecture Notes in Computer Science(), vol 10447. Springer, Cham. https://doi.org/10.1007/978-3-030-14805-8_7
Download citation
DOI: https://doi.org/10.1007/978-3-030-14805-8_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-14804-1
Online ISBN: 978-3-030-14805-8
eBook Packages: Computer ScienceComputer Science (R0)