Abstract
We propose a new language for writing programs with dependent types on top of the Coq proof assistant. This language permits to establish a phase distinction between writing and proving algorithms in the Coq environment. Concretely, this means allowing to write algorithms as easily as in a practical functional programming language whilst giving them as rich a specification as desired and proving that the code meets the specification using the whole Coq proof apparatus. This is achieved by extending conversion to an equivalence which relates types and subsets based on them, a technique originating from the “Predicate subtyping” feature of PVS and following mathematical convention. The typing judgements can be translated to the (CIC) by means of an interpretation which inserts coercions at the appropriate places. These coercions can contain existential variables representing the propositional parts of the final term, corresponding to proof obligations (or PVS type-checking conditions). A prototype implementation of this process is integrated with the Coq environment.
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
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004)
Shankar, N., Owre, S.: Principles and pragmatics of subtyping in PVS. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol. 1827, pp. 37–52. Springer, Heidelberg (2000)
Owre, S., Shankar, N.: The formal semantics of PVS. Technical Report SRI-CSL-97-2, Computer Science Laboratory, SRI International, Menlo Park, CA (1997)
Parent, C.: Synthesizing proofs from programs in the Calculus of Inductive Constructions. In: Möller, B. (ed.) MPC 1995. LNCS, vol. 947, pp. 351–379. Springer, Heidelberg (1995)
Nordström, B., Petersson, K., Smith, J.M.: Programming in Martin-Löf’s Type Theory. Oxford University Press, Oxford (1990)
Constable, R.L., Allen, S.F., Bromley, H., Cleaveland, W., Cremer, J., Harper, R., Howe, D.J., Knoblock, T., Mendler, N., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the Nuprl Development System. Prentice-Hall, Englewood Cliffs (1986)
Coquand, T., Huet, G.: The Calculus of Constructions. Inf. Comp. 76, 95–120 (1988)
Sozeau, M.: Russell Metatheoretic Study in Coq, experimental development (2006), http://www.lri.fr/~sozeau/research/russell/proof.en.html
Chen, G.: Sous-typage, Conversion de Types et Élimination de la Transitivité. PhD thesis, Université Paris VII, Laboratoire d’Informatique de l’École Normale Supérieure, Paris (1998)
Luo, Z.: Coercive subtyping in type theory. In: van Dalen, D., Bezem, M. (eds.) CSL 1996. LNCS, vol. 1258, pp. 276–296. Springer, Heidelberg (1997)
Adams, R.: Pure Type Systems with Judgemental Equality. Journal of Functional Programming 16, 219–246 (2006)
Werner, B.: On the strength of proof-irrelevant type theories. In: 3rd International Joint Conference on Automated Reasoning (2006)
Miquel, A., Werner, B.: The not so simple proof-irrelevant model of CC. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 240–258. Springer, Heidelberg (2003)
Sozeau, M.: Coercion par prédicats en Coq. Master’s thesis, Université Paris VII, LRI, Orsay, extended version - (2005), http://www.lri.fr/~sozeau/research/russell/report.pdf
Augustsson, L.: Cayenne—A language with dependent types. In: ACM SIGPLAN International Conference on Functional Programming (ICFP), Baltimore, Maryland, pp. 239–250 (1998)
McBride, C., McKinna, J.: The view from the left. J. Funct. Program. 14(1), 69–111 (2004)
Xi, H.: Dependent Types in Practical Programming. PhD thesis, Carnegie Mellon University, Pittsburgh, Pennsylvania (1998)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sozeau, M. (2007). Subset Coercions in Coq . In: Altenkirch, T., McBride, C. (eds) Types for Proofs and Programs. TYPES 2006. Lecture Notes in Computer Science, vol 4502. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74464-1_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-74464-1_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74463-4
Online ISBN: 978-3-540-74464-1
eBook Packages: Computer ScienceComputer Science (R0)