Abstract
Bundy and Richardson [7] presented a technique for reasoning about lists using ellipsis (the dots in 1 + 2 + ... + 10), where a polymorphic function, denoted by \(\Box\), is used to encapsulate recursive definitions of list functions and a portrayal system using ellipsis gives an informal proof. We highlight certain limitations of this technique and address these limitations using the recently developed theory of containers which capture the idea that many important datatypes consist of templates where data is stored. We implement our ideas in Coq and demonstrate how they can be used to prove theorems that eluded Bundy and Richardson in [7].
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.
References
Abbott, M.: Categories of Containers. PhD thesis, University of Leicester (2003)
Abbott, M., Altenkirch, T., Ghani, N.: Categories of Containers. In: Gordon, A.D. (ed.) ETAPS 2003 and FOSSACS 2003. LNCS, vol. 2620, pp. 23–38. Springer, Heidelberg (2003)
Altenkirch, T., McBride, C., Morris, P.: Generic Programming with Dependent Types. In: Backhouse, R., Gibbons, J., Hinze, R., Jeuring, J. (eds.) SSDGP 2006. LNCS, vol. 4719, pp. 209–257. Springer, Heidelberg (2007)
Bundy, A.: The automation of proof by mathematical induction. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, ch. 13, pp. 845–911. Elsevier, Amsterdam (2001)
Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-level Guidance for Mathematical Reasoning. Cambridge Tracts in Theoretical Computer Science, vol. 56. Cambridge University Press, Cambridge (2005)
Bundy, A., Jamnik, M., Fugard, A.: What is a proof? In: Philosophical Transactions of The Royal Society A: Mathematical, Physical and Engineering Sciences, vol. 363, pp. 2377–2392 (2005)
Bundy, A., Richardson, J.: Proofs about lists using ellipsis. In: Logic Programming and Automated Reasoning (1999)
Ghani, N., Abbott, M., Altenkirch, T.: Containers - constructing strictly positive types. Theoretical Computer Science 341(1), 3–27 (2005)
INRIA. The Coq Proof Asistant Reference Manual Version 8.1 (2006), http://coq.inria.fr/V8.1pl3/refman/index.html
McBride, C.: Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh (1999)
McBride, C.: Elimination with a motive. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol. 2277, pp. 197–216. Springer, Heidelberg (2002)
McBride, C., McKinna, J.: The view from the left. Journal of Functional Programming 14(1), 69–111 (2004)
Morris, P.: Constructing Universes for Generic Programming. PhD thesis, University of Nottingham (2007)
Prince, R.: An extension of the ellipsis technique. Master’s thesis, University of Edinburgh (2005)
Pugh, W.: The Omega test: A fast and practical integer programming algorithm for dependence analysis. In: Supercomputing 1991: Proceedings of the 1991 ACM/IEEE conference on Supercomputing, pp. 4–13. ACM Press, New York (1991)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Prince, R., Ghani, N., McBride, C. (2008). Proving Properties about Lists Using Containers. In: Garrigue, J., Hermenegildo, M.V. (eds) Functional and Logic Programming. FLOPS 2008. Lecture Notes in Computer Science, vol 4989. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78969-7_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-78969-7_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78968-0
Online ISBN: 978-3-540-78969-7
eBook Packages: Computer ScienceComputer Science (R0)