Suckerfish Menu

Publications

Formal Polytypic Programs and Proofs, Wendy Verbruggen, Edsko de Vries and Arthur Hughes. Journal of Functional Programming, 2010.
[PDF (Draft), Bibtex, Coq Source]

Formal Polytypic Programs and Proofs, Wendy Verbruggen, PhD thesis, Trinity College Dublin, Ireland, 2010.
[PDF, Bibtex, Coq Source]

Polytypic Properties and Proofs in Coq, Wendy Verbruggen, Edsko de Vries and Arthur Hughes. Proceedings of the ACM SIGPLAN Workshop on Generic Programming, Edinburgh, UK. August 2009.
(© Copyright 2009 by ACM, Inc., this copy is posted by permission of ACM and may not be redistributed)
[PDF, Bibtex, Coq source, Coq source in HTML]

Abstract: We formalize proofs over Generic Haskell-style polytypic programs in the proof assistant Coq. This makes it possible to do fully formal (machine verified) proofs over polytypic programs with little effort. Moreover, the formalization can be seen as a machine verified proof that polytypic proof specialization is correct with respect to polytypic property specialization.

 

Polytypic Programming in Coq, Wendy Verbruggen, Edsko de Vries and Arthur Hughes. Proceedings of the ACM SIGPLAN Workshop on Generic Programming, Victoria, BC, Canada. September 2008. (© Copyright 2008 by ACM, Inc., this copy is posted by permission of ACM and may not be redistributed)
[PDF, Bibtex, Coq source]

Abstract: The aim of our work is to provide an infrastructure for formal proofs over Generic Haskell-style polytypic programs. For this goal to succeed, we must have a definition of polytypic programming which is both fully formal and as close as possible to the definition in Generic Haskell. In this paper we show a formalization in the proof assistant Coq of type and term specialization. Our definition of term specialization can be interpreted as a formal proof that the result of term specialization has the type computed by type specialization.