{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:56:26Z","timestamp":1776891386187,"version":"3.51.2"},"reference-count":46,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","issue":"3-4","license":[{"start":{"date-parts":[[2010,9,23]],"date-time":"2010-09-23T00:00:00Z","timestamp":1285200000000},"content-version":"unspecified","delay-in-days":84,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2010,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    The aim of our work is to be able to do fully formal, machine-verified proofs over Generic Haskell-style polytypic programs. In order to achieve this goal, we embed polytypic programming in the proof assistant\n                    <jats:italic>Coq<\/jats:italic>\n                    and provide an infrastructure for polytypic proofs. Polytypic functions are reified within Coq as a datatype and they can then be specialized by applying a dependently typed term specialization function. Polytypic functions are thus first-class citizens and can be passed as arguments or returned as results. Likewise, we reify polytypic proofs as a datatype and provide a lemma that a polytypic proof can be specialized to any datatype in the universe. The correspondence between polytypic functions and their polytypic proofs is very clear: programmers need to give proofs for, and only for, the same cases that they need to give instances for when they define the polytypic function itself. Finally, we discuss how to write (co)recursive functions and do (co)recursive proofs in a similar way that recursion is handled in Generic Haskell.\n                  <\/jats:p>","DOI":"10.1017\/s0956796810000158","type":"journal-article","created":{"date-parts":[[2010,9,23]],"date-time":"2010-09-23T05:35:08Z","timestamp":1285220108000},"page":"213-270","source":"Crossref","is-referenced-by-count":2,"title":["Formal polytypic programs and proofs"],"prefix":"10.46298","volume":"20","author":[{"given":"WENDY","family":"VERBRUGGEN","sequence":"first","affiliation":[]},{"given":"EDSKO","family":"DE VRIES","sequence":"additional","affiliation":[]},{"given":"ARTHUR","family":"HUGHES","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2010,9,23]]},"reference":[{"key":"S0956796810000158_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263763"},{"key":"S0956796810000158_ref46","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159838"},{"key":"S0956796810000158_ref45","unstructured":"Verbruggen W. (2009) Coq Sources [online]. Accessed November 23, 2010. Available at: http:\/\/www.wendyverbruggen.net\/publications."},{"key":"S0956796810000158_ref42","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596599"},{"key":"S0956796810000158_ref41","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411301"},{"key":"S0956796810000158_ref40","first-page":"233","volume-title":"ICFP'09: Proceeding of the 14th ACM SIGPLAN International Conference on Functional Programming, Edinburgh, UK","author":"Rodriguez","year":"2009"},{"key":"S0956796810000158_ref44","volume-title":"Lectures on the Curry-Howard Isomorphism","author":"S\u00f8rensen","year":"2006"},{"key":"S0956796810000158_ref34","volume-title":"CATS'07: The Australian Theory Symposium","author":"Morris","year":"2007"},{"key":"S0956796810000158_ref32","volume-title":"LICS'09: 24th IEEE","author":"Morris","year":"2009"},{"key":"S0956796810000158_ref2","unstructured":"Abel A. (2006) Type-Based Termination: A Polymorphic Lambda-Calculus with Sized Higher-Order Types. PhD thesis, Fak\u00fcltat f\u00fcr Mathematik, Informatik und Statistik der Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen."},{"key":"S0956796810000158_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/604174.604179"},{"key":"S0956796810000158_ref31","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/3-540-45842-5_13","volume-title":"TYPES'00: Selected Papers from the International Workshop on Types for Proofs and Programs","author":"McBride","year":"2002"},{"key":"S0956796810000158_ref5","first-page":"1","volume-title":"Proceedings of the IFIP TC2\/WG2.1 Working Conference on Generic Programming","author":"Altenkirch","year":"2003"},{"key":"S0956796810000158_ref19","first-page":"72","volume-title":"School on Datatype-Generic Programming","author":"Hinze","year":"2006"},{"key":"S0956796810000158_ref26","first-page":"251","volume-title":"Selected Papers of ESOP'94, the 5th European Symposium on Programming","author":"Jay","year":"1995"},{"key":"S0956796810000158_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80542-0"},{"key":"S0956796810000158_ref15","first-page":"1","volume-title":"School on Datatype-Generic Programming","author":"Gibbons","year":"2006"},{"key":"S0956796810000158_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"S0956796810000158_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36576-1_2"},{"key":"S0956796810000158_ref28","first-page":"137","volume-title":"PADL'02: Proceedings of the 4th International Symposium on Practical Aspects of Declarative Languages, Portland, OR, USA","author":"L\u00e4mmel","year":"2002"},{"key":"S0956796810000158_ref37","first-page":"18","volume-title":"ESOP'96: Proceedings of the European Symposium on Programming, Link\u00f6ping, Sweden","author":"Peyton","year":"1996"},{"key":"S0956796810000158_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/11617990_16"},{"key":"S0956796810000158_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014058"},{"key":"S0956796810000158_ref29","unstructured":"L\u00f6h A. (2004) Exploring Generic Haskell. PhD thesis, Instituut voor Programmatuurkunde en Algoritmiek, Utrecht, The Netherlands."},{"key":"S0956796810000158_ref20","first-page":"150","volume-title":"School on Datatype-Generic Programming","author":"Hinze","year":"2006"},{"key":"S0956796810000158_ref13","unstructured":"Coq Development Team. (2008a) Coq frequently asked questions (v8.1) [online]. Accessed September 12, 2010. Available at: http:\/\/www.lix.polytechnique.fr\/coq\/node\/16."},{"key":"S0956796810000158_ref23","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003640"},{"key":"S0956796810000158_ref39","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"S0956796810000158_ref36","unstructured":"Norell U. (2002) Functional Generic Programming and Type Theory. MPhil thesis, Computing Science, Chalmers University of Technology."},{"key":"S0956796810000158_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_5"},{"key":"S0956796810000158_ref17","volume-title":"Generic Programs and Proofs","author":"Hinze","year":"2000"},{"key":"S0956796810000158_ref4","unstructured":"Alimarine A. (2005) Generic Functional Programming: Conceptual Design, Implementation and Applications. PhD thesis, Radboud Universiteit Nijmegen, The Netherlands."},{"key":"S0956796810000158_ref6","unstructured":"Altenkirch T. , McBride C. & McKinna J. (April 2005). Why dependent types matter [online]. Accessed September 12, 2010. Available at: http:\/\/www.cs.nott.ac.uk\/~txa\/publ\/ydtm.pdf."},{"key":"S0956796810000158_ref30","unstructured":"McBride C. (1999) Dependently Typed Functional Programs and Their Proofs. PhD thesis, University of Edinburgh."},{"key":"S0956796810000158_ref18","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006022"},{"key":"S0956796810000158_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"S0956796810000158_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.05.018"},{"key":"S0956796810000158_ref8","first-page":"265","article-title":"Universes for generic programs and proofs in dependent type theory","volume":"10","author":"Benke","year":"2003","journal-title":"Nord. J. Comput."},{"key":"S0956796810000158_ref14","unstructured":"Coq Development Team. (2008b) Coq reference manual (version 8.2) [online]. Accessed September 12, 2010. Available at: http:\/\/www.lix.polytechnique.fr\/coq\/refman\/."},{"key":"S0956796810000158_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2008.01.004"},{"key":"S0956796810000158_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90108-T"},{"key":"S0956796810000158_ref35","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054109006462"},{"key":"S0956796810000158_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.10.006"},{"key":"S0956796810000158_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76786-2_5"},{"key":"S0956796810000158_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45191-4_3"},{"key":"S0956796810000158_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_9"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796810000158","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:19:20Z","timestamp":1776889160000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796810000158\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,7]]},"references-count":46,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2010,7]]}},"alternative-id":["S0956796810000158"],"URL":"https:\/\/doi.org\/10.1017\/s0956796810000158","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,7]]}}}