We are here presenting 24 Coq vernacular files in useful order: -list utils.v: One of the biggest files, all concerning list operations, list permutations, the lifting of relations to lists (Sect. 2) and segments of the natural numbers -auxiliary material with use at many places. -wf utils.v: The subtle tactics for measure recursion in one or two arguments with a N-valued measure function (Sect. 2.4) -this is crucial for smooth extraction throughout the paper. -llist.v: Some general material on coinductive lists, in particular proven finite ones (including append for those), but also the rotate operation of Okasaki, vol.13 ,
, 2) in relation with breadth-first traversal and structural relations on trees and forests (again Sect. 3.1). -fifo.v: the module type for abstract FIFOs (Sect. 5.1). -fifo triv.v: The trivial implementation of FIFOs through lists, mentioned in Sect. 5.1. -fifo 2lists.v: An efficient implementation that has amortized O(1) operations (see, e. g., the paper by Okasaki [13]), described in Sect. 7.1. -fifo 3llists.v: The much more complicated FIFO implementation that is slower but has worst-case O(1) operations, invented by Okasaki [13]; see Sect. 7.2. -bft std.v: Breadth-first traversal naively with levels (specified with the traversal of branches in suitable order), The largest file in this library, describing binary trees (Sect. 3.1), their branches and orders on those
Towards certified meta-programming with typed Template-Coq, ITP 2018, vol.10895, pp.20-39, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01809681
, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018.
Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00344237
Introduction to Algorithms, 1989. ,
A proof dedicated meta-language, Electr. Notes Theor. Comput. Sci, vol.70, issue.2, pp.96-109, 2002. ,
URL : https://hal.archives-ouvertes.fr/hal-01125072
A verified compiler from Isabelle/HOL to CakeML, ESOP 2018, vol.10801, pp.999-1026, 2018. ,
Linear-time breadth-first tree algorithms: an exercise in the arithmetic of folds and zips, 1993. ,
Simulating induction-recursion for partial algorithms, 24th International Conference on Types for Proofs and Programs, vol.2646, pp.200-219, 2003. ,
URL : https://hal.archives-ouvertes.fr/hal-02333374
Programmation fonctionnelle certifiée -L'extraction de programmes dans l'assistant Coq, 2004. ,
A Coq library for internal verification of running-times, Sci. Comput. Program, vol.164, pp.49-65, 2018. ,
OEuf: minimizing the Coq extraction TCB, Andronick and Felty, pp.172-185 ,
Simple and efficient purely functional queues and deques, J. Funct. Program, vol.5, issue.4, pp.583-592, 1995. ,
Breadth-first numbering: lessons from a small exercise in algorithm design, Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, pp.131-136, 2000. ,
, ML for the Working Programmer, 1991.
Permutations in coinductive graph representation, CMCS 2012, vol.7399, pp.218-237 ,
URL : https://hal.archives-ouvertes.fr/hal-01539884
, , 2012.
Subset coercions in Coq, TYPES 2006, vol.4502, pp.237-252, 2007. ,
URL : https://hal.archives-ouvertes.fr/inria-00628869
Equations: a dependent pattern-matching compiler, ITP 2010, vol.6172, pp.419-434, 2010. ,
URL : https://hal.archives-ouvertes.fr/inria-00628862
Total Haskell is reasonable Coq, Andronick and Felty, pp.14-27 ,