Coq to C Translation with Partial Evaluation
Akira Tanaka
tanaka-akira@aist.go.jp
National Institute of Advanced Industrial Science and Technology (AIST)
Tsukuba, Ibaraki, Japan

Abstract

is to be able to use features that are available for usual C
programs from Gallina programs.
Gallina is a purely functional ML-like language provided
by Coq and is used for programs and proofs. However it
shares several features with many imperative languages including C.

Coq proof assistant can be used to prove various properties ofprograms written in the Gallina language. It is also possible
to translate Gallina programs to OCaml programs. However,OCaml is not suitable for low-level programs. Therefore, weare developing a Coq plugin for Gallina to C translation. Thisplugin transforms functions written in Gallina into a form
as close to C as possible within Gallina. This transformation
includes partial evaluation, which improves execution efficiency and eliminates polymorphism and dependent types.
We can easily verify in Coq that this transformation does
not change the execution result, and thus it is highly reliable.
And Gallina functions after this transformation can be easilytranslated to C.

• function definition• function invocation• conditional• variable declaration and its initialization• variable reference• recursive function
With these features, basic programming is possible. Therefore, it is possible to translate a Gallina subset of these features into a C subset to achieve translation without overheads.
But there are also gaps between Gallina and C.

CCS Concepts: • Software and its engineering → Compilers; Software verification.
Keywords: Coq, C, Gallina, translator, compiler, verification,
partial evaluation, tail recursion

1. Gallina has type polymorphism, but C does not.
2. Gallina has dependent types, but C does not.
3. Gallina can use any evaluation strategy, but C is strict.
4. Gallina uses curried functions, but C does not.
5. Gallina has first-class functions, but C does not.
6. Gallina’s data types (such as Peano’s naturals defined
as an inductive type) are suitable for proof but its naive
implementation is too inefficient. C has efficient datatypes such as 64 bit integer.
7. All Gallina programs terminate but C does not.
8. Gallina uses only immutable values but C uses mutablevalues.
9. Gallina does not require to release memory but C requires.
10. Gallina does not have a loop, but C does.

ACM Reference Format:
Akira Tanaka. 2021. Coq to C Translation with Partial Evaluation. In Proceedings of the 2021 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM ’21), January 18–
19, 2021, Virtual, Denmark. ACM, New York, NY, USA, 18 pages.
https://doi.org/10.1145/3441296.3441394

1

Introduction

We are developing a Gallina to C translator, Codegen1 plugin
for Coq proof assistant [10], which can generate low-level
C programs. The initial target of Codegen is libraries that
handle complex data structures such as succinct data structures [8]. To achieve this, we must be able to easily use
various low-level features such as 64 bit integers, built-infunctions for CPU instructions, hardware specific types suchas for SIMD registers, and so on. In other words, the goal

In this paper, we describe how we used partial evaluation
to address the first two of these gaps in the translator from
Gallina to C. Gallina achieves type polymorphism and dependent types as type computation. We eliminate them bycomputing them statically.
We also describe several Gallina transformations to makeGallina functions suitable to translate to C. The result of
these transformations (including partial evaluation) is easily
verified by Coq because they are convertible.
The 3rd and 4th gaps relate evaluation strategy. Codegengenerates C functions that implement the strict evaluation of
Gallina terms. It does not violate Gallina semantics because
Gallina can use any evaluation strategy. We assume that a

1 https://github.com/akr/codegen

Publication rights licensed to ACM. ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate ofa national government. As such, the Government retains a nonexclusive,royalty-free right to publish or reproduce this article, or to allow others to
do so, for Government purposes only.
PEPM ’21, January 18–19, 2021, Virtual, Denmark© 2021 Copyright held by the owner/author(s). Publication rights licensed
to ACM.
ACM ISBN 978-1-4503-8305-9/21/01. . . $15.00
https://doi.org/10.1145/3441296.3441394

14

PEPM ’21, January 18–19, 2021, Virtual, Denmark

Akira Tanaka

Gallina function body is evaluated after all arguments havebeen given, just as in C. This means that the evaluation of apartial application evaluates the function position and thearguments but does not evaluate the body of the function.
Codegen eliminates tail recursion using goto to address
the last gap. Codegen can generate a C function that contains multiple loops and nested loops from Gallina terms
which contain fixpoints at non-tail positions and nested fixpoints. Codegen also supports mutually tail-recursive Gallina
functions by generating a single C function that contains
multiple function bodies. Although goto is not usable forindirect calls, direct calls are enough to represent loops.
Solutions to the other gaps are not the subject of this paper
and are summarized in Appendix A.
Section 2 explains that Coq has a feature similar to partial evaluation but it has problems. Section 3 explains thewhole structure of our translation. Section 4 explains thetransformations in Gallina terms. Section 5 explains C code
generation. Section 6 explains several examples. We describe
related work in Section 7 and conclude in Section 8.

2variable|cconstant|C

constructor

|T

type

| λx :T . t

abstraction|tuapplication| let x := t : T in u

let-in| match t 0 with (Ci ⇒ ti )i=1...h end

conditional| fix (fi /ki :Ti := ti )i=1...h for f j

fixpoint

Note:• u represents a term as t.
y, z, and f represent a variable as x.
U represents a type as T .
• We write (· · · ((t u 1 ) u 2 ) · · · un ) as t u 1 . . . un .
• k is an integer.
ki for fixpoint specify the decreasing argument for fi .
• If it is unambiguous, we omit type annotations for the sakeof simplicity. We also omit ki in fixpoints if they are notused.
• We omitted the elimination predicate (as-in-return clauseof match-expression). It is not used in reductions.
• match-branches ti are functions that take the constructor
members (constructor arguments without inductive typeparameters). This formalism is taken from CIC [11].
• We omitted the detail of the types. Actual Gallina permits
any Gallina term which evaluates to a type.

Partial Evaluation with Stock Coq?

Gallina syntax is shown in Figure 1. Gallina has conversion
rules shown in Figure 2 to test the equality of terms. If two
terms are confluent by the conversion rules, they are said tobe convertible.
The six reductions in the conversion rules define the evaluation of Gallina. Since the reductions are strong normalization, any reduction can be applied to any subterm in any
order. Coq also has a command to define a reduced term as
a new constant.
These features are similar to partial evaluation. However,it has two problems: (1) the reductions can duplicate computations to produce inefficient programs; (2) Coq cannot
replace a function and its static arguments with a specialized
function.
2.1

t =x

Figure 1. Gallina syntax.
But Coq has no feature to replace pow invocations in theenvironment. We cannot replace pow z 3 with pow3 z infunctions already defined. If we have a function f that uses
pow z 3 and generate OCaml definition of f using the Extraction plugin, the generated function uses pow, not pow3.
Another problem is that the reduction rules can duplicatecomputations.

Reduction of pow

We can define a power function in Coq.

Definition pow_2x_3 x :=Eval cbv beta iota delta [pow] in pow (x + x) 3.

Fixpoint pow x y := match y with| 0 ⇒ 1| S y' ⇒ x * pow x y'
end.

This is the same as follows.

We can define the normal form of pow x 3 with reductions(beta, iota-match, iota-fix, and delta-global for the constantpow) using call-by-value strategy.

This result contains 3 times of x + x. Thus, it is not as efficient as we want.

Definition pow_2x_3 x :=(x + x) * ((x + x) * ((x + x) * 1)).

Definition pow3 x :=Eval cbv beta iota delta [pow] in pow x 3.

We can verify that pow x 3 and pow3 x are equal in Coq.

This definition is the same as follows.

Goal ∀ x, pow x 3 = pow3 x. Proof. reflexivity. Qed.

2.2

Definition pow3 x := x * (x * (x * 1)).

Verification of pow3

This equality means that evaluation of them produces thesame value. The reflexivity tactic confirms that pow x 3
and pow3 x are convertible.

The result has no recursive call and conditional. It should
run efficiently.

15

Coq to C Translation with Partial Evaluation

beta: E[Γ] ⊢ ((λx . t) u) ▷ t {x/u}

PEPM ’21, January 18–19, 2021, Virtual, Denmark

delta-local:(x := t) ∈ ΓE[Γ] ⊢ x ▷ tdelta-global:(c := t) ∈ E
E[Γ] ⊢ c ▷ tzeta: E[Γ] ⊢ let x := t in u ▷ u{x/t }iota-match:iota-fix:E[Γ] ⊢ C j u 1 . . . up+m : T p is the number of parameters of the inductive type TE[Γ] ⊢ match (C j u 1 . . . up+m ) with (Ci ⇒ ti )i=1...h end ▷ t j up+1 . . . up+m′
uk j = C u 1′ . . . um

E[Γ] ⊢ (fix (fi /ki := ti )i=1...h for f j ) u 1 . . . uk j ▷ t j { fk /fix (fi /ki := ti )i=1...h for fk }k =1...h u 1 . . . uk jE[Γ] ⊢ t : ∀x :T . U
eta expansion:
E[Γ] ⊢ t ▷ λx :T . (t x)

Note:• The rules shown here are reductions, except the eta expansion.
• t {x/u} means a term in which x in term t is replaced by u. This notation is taken from the Coq reference manual [11].
• Variables cannot conflict because Coq uses de Bruijn’s indexes to represent variables.
• E is a global environment which is a list of global assumptions (c :T ), global definitions (c := t :T ), and inductive definitions(Ind [p] (ΓI := ΓC )).
• Γ is a local context which is a list of local assumptions (x :T ) and local definitions (x := t :T ). The local assumptions represent
variables bounded by outer abstractions and fixpoints. The local definitions represent variables bounded by outer let-in.
• If it is unambiguous, we omit type annotations in these definitions for the sake of simplicity.
• Iota-match reduces match @cons nat 1 nil with (nil ⇒ t 1 ) (cons ⇒ t 2 ) end to t 2 1 nil because list has one parameter (p = 1)
and cons has two members (m = 2).

Figure 2. Gallina conversion rules.

3

Translation from Gallina to C

4

We implement the Gallina to C translation with the following
two kinds of translation phases.

Convertible Transformations

Codegen defines two constants with the convertible transformations: terms before and after the transformations.
For example, when a user specifies the second argumentof pow static and Codegen find an invocation of pow with theactual argument 3, Codegen defines two constants3 :• Convertible transformations• C code generation
The former transforms Gallina functions in a convertible
way. The latter translates Gallina functions to C functions.
We implement translation phases in the former as muchas possible. This allows us to verify with Coq that thesetransformations do not change the result of the function.
A user can configure the translation as follows.

Definition p_pow3 x := pow x 3. (* before trans. *)Definition s_pow3 x := . . . (* after trans. *)The convertible transformations generate the latter (prefixedwith s_) from the former (prefixed with p_). Codegen verifies
the convertibility of them when the latter is defined.
Codegen applies seven convertible transformations described in Section 4.2 to Section 4.8.

• constant, constructor and inductive type name mappings between Gallina and C (Gallina names are usedas-is2 by default)• zero-argument constructors to translate without parenthesis (Codegen generates parenthesis by default but
possible to translate true to true instead of true() andO to 0)• code snippets to translate match-expression to switchstatement (they are generated from the inductive typeand constructor names by default)• which the arguments are static or dynamic (only typearguments are static by default)• functions to inline (no functions to inline by default)• which types are linear (no linear types by default)

4.1

Computation Size

We define the convertible transformations that do not duplicate computations. For this purpose, we define “computationsize” as an approximation of running time4 .
We define the computation size as the number of matchexpression evaluated at run time. The size estimates a loop
count. Because a loop is represented by recursion in Gallina
and recursive functions must use match-expression to obtaina subterm of the decreasing argument for a recursive call.
3 We use longer names in actual implementation.
4 The computation size is not an approximation of code size. If we want toavoid exponential code bloat, we can disable delta-fun, iota-fix-var, and iotafix-var’. This makes complex partial evaluation impossible but monomorphization is still possible.

2 Invalid characters for a C identifier are replaced by _.

16

PEPM ’21, January 18–19, 2021, Virtual, Denmark

Akira Tanaka

E[Γ] ⊢ ti : Ti t 0 is not an application ti is not a variable x i is a fresh variable
E[Γ] ⊢ t 0 x 1 . . . x i−1 ti ti+1 . . . tn ▷ let x i := ti : Ti in t 0 x 1 . . . x i−1 x i ti+1 . . . tn
E[Γ] ⊢ t 0 : T0 t 0 is not a variable x 0 is a fresh variablezeta-item:
E[Γ] ⊢ match t 0 with (Ci ⇒ ti )i=1...h end ▷ let x 0 := t 0 : T0 in match x 0 with (Ci ⇒ ti )i=1...h end

zeta-arg:

Figure 3. V-reductions.
redex occurs in the function position of a nested applicationthat returns an inductive value. This avoids to reduce partial
applications and follows our strict evaluation strategy thatinvokes a function with all arguments. The arguments of thebeta-var redex are variables because of V-normal form. It
does not duplicate computation because the argument does
not contain a match-expression.

t = x | c | C | T | λx :T . t | let x := t : T in u
| fix (fi /ki :Ti := ti )i=1...h for f j
|tx

← (1)

| match x with (Ci ⇒ ti )i=1...h end← (2)Figure 4. V-normal form restricts Gallina terms that (1) application arguments and (2) match items to variables.
4.2

delta-var. The delta-var reduction is a restricted versionof the delta-local reduction. It can be applied only when
the local definition maps the variable to another variable.
This happens when the outer let-in bounds the variable toanother variable. Since a variable does not contain a matchexpression, delta-var reduction does not change the computation size.

Inlining

Codegen inlines user-specified functions using delta-global
reduction. (The target of specialization, pow in p_pow3 forexample, is inlined automatically.) This phase does not apply
further reductions such as beta reduction.
Since delta-global is part of the conversion rules, this transformation is convertible.
We assume functions inlined are defined as terms formed
as an abstraction or a fixpoint. In this case, inlining does notchange the computation size because the evaluation of themdoes not cause an evaluation of match-expression.
4.3

delta-fun. The delta-fun reduction is another restricted version of the delta-local reduction. It can be applied only whenthe variable f occurs in the function position of an application, f y1 . . . yq (0 < q), and the bounded expression,t x 1 . . . xp (0 ≤ p), has no computation. The evaluation of
the function t has no computation because there is a premise
to avoid match-expression. The evaluation of the arguments,
x 1 . . . xp , has no computation because they are just variables.
t x 1 . . . xp is a partial application because it is the function off y1 . . . yq and 0 < q. The evaluation of t x 1 . . . xp does notevaluate the function body of t because our strict evaluation
strategy does not invoke the function of a partial application.
Thus, the bounded expression has no computation and thedelta-fun reduction does not change the computation size.

V-Normalization

Codegen transforms arguments of application and match
items as variables as A-normal form [4]. We call the result of
this transformation V-normal form. V-normal form permits
more expressions at binding expressions in let-in and function positions in applications than A-normal form. Figure 3
shows V-reductions to generate V-normal form shown in
Figure 4.
V-reductions introduce let-in expressions. V-reductions
produce a convertible term because they are zeta expansion.
V-reductions move an expression from an application argument and a match item. This moves computations but
does not change the computation size.
4.4

zeta-flat. The zeta-flat reduction commutes let-in expression to make any let-in expression does not bind a let-in
expression. This reduction can be considered as a combination of zeta reduction to delete the let-in expression for
x and zeta expansion to restore it in the different position.
The evaluation of the term before and after the reduction isboth that evaluation of t 1, t 2, t 0 . Thus, it does not change thecomputation size.

S-Normalization

We define S-reductions in Figure 5 to simplify V-normal
terms. S-reductions are the reduction rules for the partial
evaluation without computation duplication.
S-reductions resemble the conversion rules. Especially,
they are terminating because iota-fix-var (and iota-fix-var’)
has the same guard condition of iota-fix.

zeta-app. The zeta-app reduction moves a let-in binding
from the function position of an application outside of theapplication. This reduction can be considered as a combination of zeta reduction and zeta expansion such as zeta-flat
reduction. This reduction moves t but does not change thecomputation size.

beta-var. The beta-var reduction is a restricted version of
the beta reduction. It applies the beta reduction when a beta

17

Coq to C Translation with Partial Evaluation

PEPM ’21, January 18–19, 2021, Virtual, Denmark

E[Γ] ⊢ (λx . t) y1 . . . yn : T T is an inductive type(x := y) ∈ Γdelta-var:
E[Γ] ⊢ (λx . t) y1 . . . yn ▷ t {x/y1 } y2 . . . yn
E[Γ] ⊢ x ▷ y
0 ≤ p 0 < q (f := t x 1 . . . xp ) ∈ Γ t is one of x, c, C, λx . u, fix (fi /ki := ti )i=1...h for f j
delta-fun:E[Γ] ⊢ f y1 . . . yq ▷ t x 1 . . . xp y1 . . . yq
zeta-flat: E[Γ] ⊢ let y := (let x := t 1 in t 2 ) in t 0 ▷ let x := t 1 in (let y := t 2 in t 0 )beta-var:0<nzeta-app: E[Γ] ⊢ (let x 0 := t in u) x 1 . . . x n ▷ let x 0 := t in (u x 1 . . . x n )iota-match-var:iota-fix-var:(x := C j y1 . . . yp+m : T ) ∈ Γ p is the number of parameters of the inductive type TE[Γ] ⊢ match x with (Ci ⇒ ti )i=1...h end ▷ t j yp+1 . . . yp+m
(x k j := C y1 . . . ym ) ∈ Γ f 1′ . . . fh′ are fresh variables
E[Γ] ⊢ (fix (fi /ki := ti )i=1...h for f j ) x 1 . . . x n : T

T is an inductive type

E[Γ] ⊢ (fix (fi /ki := ti )i=1...h for f j ) x 1 . . . x n ▷let f 1′ := fix (fi /ki := ti )i=1...h for f 1 in . . . let fh′ := fix (fi /ki := ti )i=1...h for fh in
t j { fk /fk′ }k =1...h x 1 . . . x n(x k j := C y1 . . . ym ) ∈ Γ′(f 1 := fix (fi /ki := ti )i=1...h for f 1 ) ∈ Γ . . . (fh′ := fix (fi /ki := ti )i=1...h for fh ) ∈ Γ

iota-fix-var’:E[Γ] ⊢ (fix (fi /ki := ti )i=1...h for f j ) x 1 . . . x n : T

T is an inductive type

E[Γ] ⊢ (fix (fi /ki := ti )i=1...h for f j ) x 1 . . . x n ▷ t j { fk /fk′ }k =1...h x 1 . . . x n
Figure 5. S-reductions.

iota-match-var. The iota-match-var reduction reduces amatch-expression to one of its branches if the constructor
for the match item is known. Since the match item is always
a variable in V-normal form, the premise of this reduction
examines the local definition. We require that the local definition contains a constructor application with arguments
as variables. This requirement makes it possible to use theconstructor members in the reduced expression without duplicating computation. This reduction can be considered as a
combination of delta-local reduction to make the match item
constructor form and iota-match reduction. It decreases thecomputation size because it removes the evaluation of thematch-expression at run time.

iota-fix-var’. The iota-fix-var’ reduction is the same as iotafix-var reduction but reuses already bounded fixpoints. This
reduction is optional. This reduction can be considered as a
combination of the conversion rules the same as iota-fix-var
except that delta-local expansions are used instead of thelast zeta expansions. It has the property the same as iota-fixvar reduction except that the size of intermediate terms are
smaller.
4.5

Call Site Replacement

Codegen replaces a function and its static arguments with a
specialized function. When new values for static arguments
are found, a new specialized function (before transformations
prefixed by p_) is defined in the global environment.
The values of static arguments are obtained by normalizing the actual static arguments (variables) using the reductions in the conversion rules. Codegen requires that these
normal forms have no free variables.
This transformation does not start the convertible translations for other functions and does not define simplified
functions (prefixed with s_) for the other functions. Thus,
Codegen can transform one function at a time.
This transformation can be considered as delta-global expansion addition to the reductions for normalizing the static
arguments. If a dynamic argument exists before a static argument such as pow, beta expansion is also used before thedelta-global expansion: when the normal form of three is3, pow z three is transformed to (fun x ⇒ pow x 3) z and(fun x ⇒ pow x 3) is replaced with the constant p_pow3.

iota-fix-var. The iota-fix-var reduction reduces a fixpoint
application that returns an inductive value. We require allarguments, not only until the decreasing arguments, to avoid
reducing partial applications. This reduction introduces letin bindings for the fixpoints to preserve V-normal form. Since
the decreasing argument is a variable in V-normal form, thepremise examines the local definition. Thus, this reduction
can be considered as a combination of delta-local reduction
to make the decreasing argument constructor form, iota-fix
reduction, delta-local expansion to restore the decreasingargument, and zeta expansions to extract the fixpoints substituted by the iota-fix reduction. Since the introduced let-in
bindings have no computation (because they are fixpoints
without arguments), this reduction does not change the computation size.

18

PEPM ’21, January 18–19, 2021, Virtual, Denmark

zeta-del:Akira Tanaka

x does not occur in u
E[Γ] ⊢ let x := t in u ▷ uformalized it in Appendix C to generates a variable mappingfrom Gallina to C.
Codegen implements this allocation by renaming variables in Gallina terms. This “renaming” does not change deBruijn’s indexes but changes variable names. Therefore, we
can inspect the renaming by printing the result of the convertible transformations. This is the reason that we define
this as one of the convertible transformations. This transformation does not affect the evaluation of Gallina terms.

Figure 6. Unused let-in deletion.

Although delta-global expansion introduces new constantin the global environment, convertibility test still works
because it can use delta-global reduction.
It does not change the computation size because the function position is a constant and the static arguments are variables and they do not contain match-expression.
4.6

4.9

The transformations produce convertible terms because they
are combinations of the conversion rules. However, severaltransformations use the reverse of the conversion rules. Vnormalization uses zeta expansion. S-normalization uses
zeta expansion and delta-local expansion. Call site replacement uses delta-global expansion and beta expansion. Argument completion uses zeta expansion. Since the conversion
rules restore the original term, they do not break convertibility. Furthermore, zeta expansion, delta-local expansion,and delta-global expansion produces a well-typed term froma well-typed term. They replace an expression with a newvariable or constant which is convertible to the original expression. Since the Gallina typing rules do not distinguishconvertible terms, they produce a well-typed term. The beta
expansion can produce an ill-typed term for a dependently
typed term [11] but we focus non-dependent terms after
S-normalization.

Unused let-in Deletion

This transformation deletes unused let-in expressions asshown in Figure 6. It is applied after call site replacement
because call site replacement removes variable referencessuch as three in the example in Section 4.5.
This reduction is a restricted zeta reduction.
This reduction removes the binding expression t in let-in
expression. Therefore, it can decrease the computation size
when an evaluation of t evaluates a match-expression. But
it does not increase the computation size.
4.7

Argument Completion

Codegen applies eta expansion to avoid partial applications
because C has no partial application. This makes all C variables5 explicit in Gallina. It simplifies the arguments generated by eta expansion by moving the arguments into abody of let-in expression and beta-var reduction. Thus, thistransformation can be considered as a combination of eta
expansion, zeta-app reduction, and beta-var reduction.
It also transforms match-branches into nested abstractions corresponding to the members of constructors. Thistransformation is also eta expansion.
This transformation does not change the computation size
because we apply eta expansion only when it does not delay
evaluation. Since a function body is evaluated after all arguments are given, we can apply eta expansion for the function
body (top-level functions and functions for fixpoints). If a
constructor has k members, the corresponding match-branchis evaluated with k arguments so we can apply k times ofeta expansion for the branch.
The detail of this transformation is shown in Appendix B.
4.8

Well-Typedness of the Transformations

5

C Code Generation

Codegen generates C code from the result of the convertible
transformations. However Codegen gives up code generation
if the result still contains type computations6 or closure
generation. We describe the subset of Gallina that can betranslated to C in Appendix D7 .
This translation is easy because:• No complex subexpressions because of V-normal form
(like A-normal form)• No type computations and closure generation• No partial applications and C variables are alreadyallocated
The convertible transformations may retain lambda abstractions not only at the top-level of a function. Codegencan generate C code for them as far as arguments are given
lexically outside of them. For example, Codegen can generate C code for match x with tt ⇒ fun y ⇒ y end z. Since

C Variable Allocation

This transformation allocates C variables for Gallina variables. It generates unique names that are valid in C. It may allocate one C variable for multiple Gallina variables when they
are always bound to the same value. For example, y is always
the same as z in match x with tt ⇒ fun y ⇒ y end z. We

6 The type computation includes type polymorphism, polymorphic recur-

sion, and dependent types
7 This is the intermediate representation for Codegen, not the defini-tion of the source Gallina terms for Codegen. We do not define thesource Gallina terms for Codegen because the convertible transformations
may remove arbitrary complex terms. For example, Codegen can handle
match u with true ⇒ 0 | false ⇒ t end for any t , as far as u is reduced
to true. It is not possible to determine that without actually reducing u.

5 The temporary variables for parallel assignments are the exception.

19

Coq to C Translation with Partial Evaluation

PEPM ’21, January 18–19, 2021, Virtual, Denmark

The convertible transformation for f generates p_pow3 ands_f as follows. (p_f is not generated because f has no static

Codegen does not support closures yet, lambda abstractions
that have no such actual arguments are not supported.
Codegen needs one more complicated task, tail recursion
elimination. Codegen guarantees it because Gallina has noloops and we need a reliable way to describe loops that do
not consume the stack. Since C compilers do not guarantee
tail recursion elimination, Codegen must do it.
We show the code generation in Figure 7 for non-tailposition and Figure 8 for tail position. Figure 9 defines auxiliary functions for them. Top-level function generation is
described in Appendix E.
Codegen translates a recursive call in a tail position using
goto. This is the traditional translation method and allows
us to generate a loop in a tail position.
We also generate a loop in a non-tail position. We want
this feature to generate loops for inlined small higher-orderfunctions such as fold_left. Such functions are used not
only in tail positions. Thus, we generate a loop from a fixpoint application in a non-tail position. However, not all ofthem can be a loop.
Whether a fixpoint application in a non-tail position canbe a loop is determined by TR in Figure 10. TR determinesthat a fixpoint can be a loop if all recursive calls to the functions bounded by the fixpoint are translated to goto. Thisis equivalent to a C compiler determining that a recursivefunction cannot be inlined, but a non-recursive function canbe inlined, even if it contains goto.
Codegen can generate a C function that contains multiple
Gallina functions. It is used to generate mutually recursivefunctions with goto. See Appendix E for details.

6

Translation Examples

6.1

Convertible Transformations without
Duplicating Computations

arguments.)
Definition p_pow3 x := pow x 3.
Definition s_f v1_x v2_y :=let v3_n := p_pow3 v1_x in
let v4_n := p_pow3 v2_y in
v3_n + v4_n.
s_pow3 can be generated by applying the convertible transformations to p_pow3.
Definition s_pow3 v1_x :=let v2_n := 0 in
let v3_n := S v2_n in
let v4_n := v1_x * v3_n in
let v5_n := v1_x * v4_n in
v1_x * v5_n

Codegen generates C functions for pow3 and f from s_pow3
and s_f as in Figure 11. This result shows that Codegen generates a specialized function that invokes another specialized
function: the invocation of pow in f is translated to the invocation of pow3. This is different from Coq reductions with
the Extraction plugin described in Section 2.1.
These functions depend on a C implementation of theinductive type and primitive functions. If a user wants toimplement nat by uint64_t, the implementation in Figure 12
is possible8 .
6.3

Monomorphization of List.rev

The convertible transformations are usable for monomorphization (type polymorphism elimination). Since Gallina isa dependently typed language, types are first-class values
and they can be passed as arguments. If a type is passed as
an argument and it is used for the type of a later argument,
the function is polymorphic. Thus, a beta reduction can eliminate a type argument. (If a fixpoint has a type argument,
we cannot monomorphize it. This means Codegen cannot
eliminate polymorphic recursion.)
Coq has a list reversal function rev in the standard library.
It is defined as follows10 .

The convertible transformations do not duplicate computations. Therefore, we can specialize pow_2x_3 in Section 2.1
properly. The convertible transformations in Codegen defines_pow_2x_3 as follows:
Definition s_pow_2x_3 v1_x :=let v2_n := v1_x + v1_x in
let v3_n := 0 in
let v4_n := S v3_n in
let v5_n := v2_n * v4_n in
let v6_n := v2_n * v5_n in
v2_n * v6_n.

The addition occurs only once and is not duplicated.

Definition rev := fun (A : Type) ⇒fix rev (l : list A) : list A :=match l with| nil ⇒ nil| x :: l' ⇒ rev l' ++ x :: nil
end.

6.2

8 nat and uint64_t are not isomorphic because nat has infinitely many

Specialized Function Application Generation

elements and uint64_t has a finite number of elements. We provide another
Coq plugin, monadification9 [9] to translate a function to use option monad.
We can use it to verify that this mismatch does not cause problems whenoverflow does not occur.
9 https://github.com/akr/monadification
10 The standard library uses Section to define this term.

Codegen generates a specialized function that invokes otherspecialized functions. Assume the following definition andthe second argument of pow is static.
Definition f x y := pow x 3 + pow y 3.

20

PEPM ’21, January 18–19, 2021, Virtual, Denmark

Akira Tanaka

AK Jt / x 1 . . . x n K generates C code for t x 1 . . . x n in a non-tail position. The result expression is passed to K.
K(e) = “v = e;” in simple situations.
AK Jx / K = K(“x”)

AK Jx / x 1 . . . x n K = “ passign(fvars′JxK, x 1 . . . x n ) goto entry_x;”n > 0 ∧ x is bounded by a fixpoint ∧ x ∈ TR

AK Jc / x 1 . . . x n K = K(“c(x 1, . . . , x n )”)n≥0

AK Jx / x 1 . . . x n K = K(“x(y1, . . . , yo , x 1, . . . , x n )”)n > 0 ∧ x is bounded by a fixpoint ∧ x < TR

AK JC / x 1 . . . x n K = K(“C(x 1, . . . , x n )”)n≥0

AK Jlet x := t 1 in t 2 / x 1 . . . x n K = “ AK ′ Jt 1 / K AK Jt 2 / x 1 . . . x n K”

where K ′(e) = “x = e;”

AK Jmatch x with (Ci ⇒ λyi1 . . . λyi NMCi . ti )i=1...h end / x 1 . . . x n K =where x : T

AK Jt x 0 / x 1 . . . x n K = AK Jt / x 0 x 1 . . . x n K

AK Jλx . t / x 1 x 2 . . . x n K = AK Jt / x 2 . . . x n K(x and x 1 are mapped to the same C variable)“switch (swfuncT (x)) {...
caselabelCi :yi1 = get_member Ci 1 (x); . . . ; yi NMCi = get_member Ci NMC (x);i

AK Jti / x 1 . . . x n K

break;...
}”AK Jfix (fi := ti )i=1...h for f j / x 1 . . . x n K =f j ∈ TR“ passign(fvarsJt j K, x 1 . . . x n )where K ′(e) =(K(e)K(e) contains goto
“K(e) goto exit_f j ;” otherwise

GENBODYATK ′ Jfix (f i := t i )i=1...h for f j K

exit_f j :”AK Jfix (fi := ti )i=1...h for f j / x 1 . . . x n K =f j < TR“K(f j (y1, . . . , yo , x 1 . . . , x n ))goto skip_f j ;GENBODYAN Jfix (fi := ti )i=1...h for f j K

skip_f j :”Note:
• “ . . . ” means a string. A string can contain characters in typewriter font and expressions starting in italic or roman font. The former
is preserved as-is. The latter embeds the value of the expression (with name translation from Gallina to C).
• Gallina types, constants, and constructors have corresponding (user-configurable) C names and they are implicitly translated. Gallina
variables are translated by the mapping defined in Section 4.8.
• TR = TRJtKn where the translating function is defined as Definition c := t and t is an n-arguments function.
• NMC is the number of the members of the constructor C (the number of arguments without the parameters for the inductive type):
NMC = m if C : T1 → · · · → Tp → Tp+1 → · · · → Tp+m → T0 and T0 is an inductive type which has p parameters.
• swfuncT , caselabelCi , and get_member Ci j are defined by a user to translate match-expressions for the inductive type T .
• passign(y1 . . . yn , x 1 . . . x n ) is a parallel assignment. It is translated to a sequence of assignments to assign x 1 . . . x n into y1 . . . yn . It
may require temporary variables.
• y1, . . . , yo are the outer variables of the fixpoint.
• We do not define AK Jλx . t / K because we do not support closures yet.
• Actual Codegen generates GENBODYAN JK in a different position to avoid the label skip_f j and goto skip_f j ;.

Figure 7. Translation to C for a non-tail position.

21

Coq to C Translation with Partial Evaluation

PEPM ’21, January 18–19, 2021, Virtual, Denmark

BK Jt / x 1 . . . x n K generates C code for t x 1 . . . x n in a tail position. The result expression is passed to K.
K(e) = “return e;” in simple situations.
BK Jx / K = K(“x”)

BK Jx / x 1 . . . x n K = “ passign(fvars′JxK, x 1 . . . x n ) goto entry_x;”

BK Jc / x 1 . . . x n K = K(“c(x 1, . . . , x n )”)n > 0 ∧ x is bounded by a fixpointn≥0

BK JC / x 1 . . . x n K = K(“C(x 1, . . . , x n )”)n≥0

BK Jlet x := t 1 in t 2 / x 1 . . . x n K = “ AK ′ Jt 1 / K BK Jt 2 / x 1 . . . x n K”

where K ′(e) = “x = e;”

BK Jt x 0 / x 1 . . . x n K = BK Jt / x 0 x 1 . . . x n K

BK Jλx . t / x 1 x 2 . . . x n K = BK Jt / x 2 . . . x n K(x and x 1 are mapped to the same C variable)

BK Jmatch x with (Ci ⇒ λyi1 . . . λyi NMCi . ti )i=1...h end / x 1 . . . x n K = where x : T“switch (swfuncT (x)) {...
caselabelCi : yi1 = get_member Ci 1 (x); . . . ; yi NMCi = get_member Ci NMC (x);i
BK Jti / x 1 . . . x n K...
}”
BK Jfix (fi := ti )i=1...h for f j / x 1 . . . x n K =“ passign(fvarsJt j K, x 1 . . . x n )Note:

GENBODYBK Jfix (fi := ti )i=1...h for f j K”

We do not define BK Jλx . t / K because a tail position cannot be a function after the argument completion.

Figure 8. Translation to C for a tail position.
“x; fvarsJuK” t = λx . ufvarsJtK = fvarsJt j K
t = fix (fi := ti )i=1...h for f j “”otherwisefvars′Jfi K = fvarsJti K for functions bounded by fix (fi := ti )i=1...h for f j
GENBODYAT
t = λx . u

K JuK



AT


“entry_fi : GENBODYK Jti K”
t = fix (fi := ti )i=1...h for f j
GENBODYATK JtK = 
for
i
=
j,
1,
.
.
.
,
(j
−
1),
(j
+
1),
.
.
.
,
h



 A Jt / Kotherwise
 K
AN GENBODY JuK
t = λx . u




AN


“entry_fi : GENBODY Jti K” t = fix (fi := ti )i=1...h for f j
GENBODYAN JtK =
for i = 1, . . . , h B Jt / Kotherwise where t : T K(e) = “*(T *)ret = e; return;” Kt = λx . u
 GENBODYBK JuK



B


“entry_f:
GENBODYJt
K”t= fix (fi := ti )i=1...h for f jiiKGENBODYBK JtK =
for i = j, 1, . . . , (j − 1), (j + 1), . . . , h B Jt / Kotherwise
 K

Note:
• fvars and fvars ′ returns a list of variables: x 1 ; . . . ; x n ;. For simplicity, we omit “;” if not ambiguous.
• “д(i)” for i = j 1, . . . , jn means “д(j 1 ) . . . д(jn )”.

Figure 9. Auxiliary functions for translation to C.

22

PEPM ’21, January 18–19, 2021, Virtual, Denmark

Akira Tanaka

TRJtKn is the first element of RNTJtKn .
(R, N ,T ) = RNTJtKn classify variables in t assuming that it is called with n arguments as t x 1 . . . x n :R : tail-recursive fixpoint bounded functions that do not need to be real functions
N : free variables at non-tail positions of t
T : free variables at tail positions of t
“tail position” is extended to the function position of the application at a tail position.
R distinguishes fixpoint bounded functions translatable without actual functions (but with goto) or not.
TRJtKn = R

where (R, N ,T ) = RNTJtKn

RNTJtKn = (∅, ∅, {x })






(∅, ∅, ∅) (R, N ∪ {x },T ) (R 1 ∪ R 2, N 1 ∪ T1 ∪ N 2 − {x },T2 − {x })






Ð
Ð
Ð


 hi=1 Ri , hi=1 Ni , hi=1 Ti (R, N − {x },T − {x })(R, (N ∪ T ) − {x }, ∅)



Ðh



i=1 R i ∪ { f 1, . . . , fh },

Ð

h


 Ði=1 Ni − { f 1, . . . , fh },h i=1 Ti − { f 1, . . . , fh }Ð hi=1 Ri ,


Ðh




i=1 (Ni ∪ Ti ) − { f 1, . . . , fh },

 ∅


t =x
t =c ∨t =C
t = u x where (R, N ,T ) = RNTJuKn+1
t = let x := t 1 in t 2
where (R 1, N 1,T1 ) = RNTJt 1 K0 (R 2, N 2,T2 ) = RNTJt 2 Kn
t = match x with (Ci ⇒ ti )i=1...h end where (Ri , Ni ,Ti ) = RNTJti KNMCi +nt = λx . u ∧ n > 0 where (R, N ,T ) = RNTJuKn−1
t = λx . u ∧ n = 0 where (R, N ,T ) = RNTJuKNAu (closure)t = fix (fi := ti )i=1...h for f j ∧Ð
n = NAt ∧ hi=1 Ni ∩ { f 1, . . . , fh } = ∅where (Ri , Ni ,Ti ) = RNTJti KNAti
t = fix (fi := ti )i=1...h for f j ∧ (real function, maybe closure)Ð¬(n = NAt ∧ hi=1 Ni ∩ { f 1, . . . , fh } = ∅ )where (Ri , Ni ,Ti ) = RNTJti KNAti

Note:• NAt is the number of arguments of t: NAt = m if t : T1 → · · · → Tm → T0 and T0 is an inductive type.
• The variables in t are unique. Codegen uses de Bruijn’s indexes for N and T ; the variables renamed by Section 4.8 for R.

Figure 10. Detection of tail recursive fixpoint bounded functions.
static nat pow3(nat v1_x) {nat v2_n; nat v3_n; nat v4_n; nat v5_n;
v2_n = O();v3_n = S(v2_n);v4_n = mul(v1_x, v3_n);v5_n = mul(v1_x, v4_n);
return mul(v1_x, v5_n);}typedef uint64_t nat;#define O() 0#define S(n) ((n)+1)#define add(x,y) ((x) + (y))#define mul(x,y) ((x) * (y))

static nat f(nat v1_x, nat v2_y) {nat v3_n; nat v4_n;
v3_n = pow3(v1_x);v4_n = pow3(v2_y);
return add(v3_n, v4_n);}

We can monomorphize rev by the convertible transformations as Figure 16. s_rev_bool is a monomorphic function
without type arguments.
Codegen generates a C function as Figure 17 for it. Thisfunction depends on the implementation of bool type (booltype), list bool type (list_bool type; lb_nil and lb_cons
for constructors; lb_is_nil, lb_head, and lb_tail for matchexpression implementation), and the implementation of app(++ operator) for list bool type (app_bool). See Appendix F
for details.

Figure 12. nat implementation using uint64_t.

Figure 11. pow3 and f generated by Codegen.

23

Coq to C Translation with Partial Evaluation

PEPM ’21, January 18–19, 2021, Virtual, Denmark

Fixpoint sprintf_type (fmt : string) : Type := match fmt with
| EmptyString ⇒ buffer| String "%"%char (String "d"%char rest) ⇒ nat → sprintf_type rest
| String "%"%char (String "b"%char rest) ⇒ bool → sprintf_type rest
| String "%"%char (String "s"%char rest) ⇒ string → sprintf_type rest
| String "%"%char (String _ rest) ⇒ sprintf_type rest
| String "%"%char EmptyString ⇒ buffer| String _ rest ⇒ sprintf_type rest end.
Fixpoint sprintf (buf : buffer) (fmt : string) : sprintf_type fmt := match fmt return sprintf_type fmt with
| EmptyString ⇒ buf| String "%"%char (String "d"%char rest) ⇒ fun (n : nat) ⇒ sprintf (buf_addnat buf n) rest
| String "%"%char (String "b"%char rest) ⇒ fun (b : bool) ⇒ sprintf (buf_addbool buf b) rest
| String "%"%char (String "s"%char rest) ⇒ fun (s : string) ⇒ sprintf (buf_addstr buf s) rest
| String "%"%char (String ch rest) ⇒ sprintf (buf_addch (buf_addch buf "%") ch) rest
| String "%"%char EmptyString ⇒ buf_addch buf "%"%char| String ch rest ⇒ sprintf (buf_addch buf ch) rest end.

Figure 13. sprintf definition using dependent type.
Definition s_sprintf_x_eq_nat v1_buf v2_n :=let v3_b := false in let v4_b := false in let v5_b := false in let v6_b := true inlet v7_b := true in let v8_b := true in let v9_b := true in let v10_b := false in
let v11_a := Ascii v3_b v4_b v5_b v6_b v7_b v8_b v9_b v10_b in
let v12_b := true in let v13_b := false in let v14_b := true in let v15_b := true inlet v16_b := true in let v17_b := true in let v18_b := false in let v19_b := false in
let v20_a := Ascii v12_b v13_b v14_b v15_b v16_b v17_b v18_b v19_b in
let v21_b := buf_addch v1_buf v11_a in let v22_b := buf_addch v21_b v20_a in
let v23_b := buf_addnat v22_b v2_n in v23_b• Ascii is the constructor of ascii type defined in the standard library of Coq.
• v11_a and v20_a are the characters "x" and "=" (0x78 and 0x3d in ASCII).

Figure 14. sprintf specialized with respect to the format string "x=%d".
typedef unsigned char ascii;#define Ascii(b0,b1,b2,b3,b4,b5,b6,b7) \((b0) | (b1) << 1 | (b2) << 2 | (b3) << 3 | (b4) << 4 | (b5) << 5 | (b6) << 6 | (b7) << 7)static buffer sprintf_x_eq_nat(buffer v1_buf, nat v2_n) {bool v3_b; bool v4_b; bool v5_b; bool v6_b; bool v7_b; bool v8_b; bool v9_b; bool v10_b; ascii v11_a;bool v12_b; bool v13_b; bool v14_b; bool v15_b; bool v16_b; bool v17_b; bool v18_b; bool v19_b; ascii v20_a;buffer v21_b; buffer v22_b; buffer v23_b;v3_b = false; v4_b = false; v5_b = false; v6_b = true; v7_b = true; v8_b = true; v9_b = true; v10_b = false;
v11_a = Ascii(v3_b, v4_b, v5_b, v6_b, v7_b, v8_b, v9_b, v10_b);v12_b = true; v13_b = false; v14_b = true; v15_b = true; v16_b = true; v17_b = true;
v18_b = false; v19_b = false; v20_a = Ascii(v12_b, v13_b, v14_b, v15_b, v16_b, v17_b, v18_b, v19_b);v21_b = buf_addch(v1_buf, v11_a); v22_b = buf_addch(v21_b, v20_a); v23_b = buf_addnat(v22_b, v2_n);return v23_b;}• ascii type and Ascii macro are a user-defined implementation of ascii type.

Figure 15. C code generation of sprintf specialized with respect to the format string "x=%d".

24

PEPM ’21, January 18–19, 2021, Virtual, Denmark

Akira Tanaka

has no feature to specialize functions. When a Gallina function uses a dependent type which is not typable in OCaml,
Obj.magic is used. This requires a uniform data representation where all values can be represented by a single type(single word, typically) at run time. Codegen does not havethis requirement and any specific representation is usablefor each inductive type.
CertiCoq [1] and Œuf [7] are compilers for Gallina togenerate executable code using CompCert [5]. They use a
uniform data representation and have no specialization.
A-normal form [4], K-normal form [2], and our V-normal
form restricts application arguments as variables. They also
restrict condition expressions as variables. A-normal form
prohibits a let-in and conditional expression in a let-in binding but K-normal form and V-normal form permit it. Anormal form restricts function position with values (constant, variable, lambda abstraction) and primitive operations.
K-normal form restricts function position with variables(including letrec-bounded functions). V-normal form permits in function position any V-normal term including let-in,
conditional expression, and fixpoint. This permissibility ofV-normal form is important to represent a loop using anapplication which function position is a fixpoint.
Continuation Passing Style (CPS) is another choice for anintermediate language of compilers. CPS and V-normal form
restricts arguments as variables. The naive CPS translation
produces many administrative redexes that can be reduced
at compile time [3]. Our V-reduction restricts arguments aterm as variables and S-reduction simplifies the term. The
difference between them is V-reduction does not introduce
extra constructs if an argument is already a variable and Sreduction reduces redexes not only administrative redexes.

Definition p_rev_bool := rev bool.
Definition s_rev_bool :=fix rev_bool (v1_l : list bool) : list bool :=match v1_l with| nil ⇒ lb_nil| v2_x :: v3_l_ ⇒let v4_l := rev_bool v3_l_ in
let v5_l := lb_nil in
let v6_l := lb_cons v2_x v5_l in
p_app_bool v4_l v6_l
end

Figure 16. The monomorphized rev function.
static list_bool rev_bool(list_bool v1_l){ bool v2_x; list_bool v3_l_; list_bool v4_l;
list_bool v5_l; list_bool v6_l;
switch (lb_is_nil(v1_l)){ default: return lb_nil;case 0: v2_x = lb_head(v1_l);v3_l_ = lb_tail(v1_l);v4_l = rev_bool(v3_l_);v5_l = lb_nil;
v6_l = lb_cons(v2_x, v5_l);
return app_bool(v4_l, v6_l);} }Figure 17. Generated C code for rev bool.
6.4

Dependent Type Elimination of sprintf

Gallina can use dependent types to define functions which
type depends on (non-type) arguments. For example, sprintf
in Figure 13 is a function that the second argument fmt defines types of subsequent arguments. The types of subsequent arguments are computed by sprintf_type.
Codegen can specialize sprintf function to eliminate dependent types. Codegen specializes sprintf with respect tothe format string "x=%d" as in Figure 14. The result does notcontain dependent types. The result is very long because
all bits of all characters in the format string are bound byvariables. Figure 15 shows the C function generated for the
specialized sprintf function.
sprintf takes a buffer as the first argument and returns
a buffer that formatted string is appended. buffer type is
expected to be declared as linear and the buf_addch function
modifies the buffer destructively. See Appendix G for details.

78Conclusion

We described that conversion rules-based partial evaluationis possible and its result is easily verifiable in Coq. The partial
evaluation is usable for monomorphization and dependent
type elimination. We formalized the partial evaluation as
reductions over a subset of Gallina term, V-normal form.
Codegen implements the partial evaluation and generates
C functions. We defined several transformations to makea result of the partial evaluation close to C to ease C code
generation. These transformations are also convertible as
the partial evaluation and its result is easily verifiable.
The C code generation in Codegen guarantees tail recursion elimination. It eliminates tail recursion in a tail position
and also eliminates tail recursion in a non-tail position if
possible.

Related WorkAcknowledgments

The Extraction plugin [6] is a standard plugin of Coq. It translates Gallina to OCaml, Haskell, and Scheme. It translates
one Gallina function to one function in a target language andThis research was partially supported by the JSPS Bilateral
Joint Research (Number: 20203001)/Inria AYAME Program
Project FLAVOR.

25

Coq to C Translation with Partial Evaluation

A

B

PEPM ’21, January 18–19, 2021, Virtual, Denmark

Summary of Solutions to the Gaps
between Gallina and C

D• Gallina has type polymorphism, but C does not.
→ Codegen uses partial evaluation to eliminate type
polymorphism if possible.
• Gallina has dependent types, but C does not.
→ Codegen uses partial evaluation to eliminate dependent types if possible.
• Gallina can use any evaluation strategy, but C is strict.
→ Codegen applies the strict evaluation strategy to
Gallina terms.
• Gallina uses curried functions, but C does not.
→ Codegen applies the semantics that evaluates afunction body after all arguments are given.
• Gallina has first-class functions, but C does not.
→ We have a plan to implement restricted closures(downward funarg).
• Gallina’s data types (such as Peano’s naturals defined
as an inductive type) are suitable for proof but its naive
implementation is too inefficient. C has efficient datatypes such as 64 bit integer.
→ Codegen is data representation agnostic. A user cancustomize the implementation of inductive types.
• All Gallina programs terminate but C does not.
→ Our target is library functions and most of themterminate.
• Gallina uses only immutable values but C uses mutablevalues.
→ Local variables are modifiable at tail recursive calls
which are translated to assignments and goto. Also,
Codegen has a linearity checker for destructive updates on heap structures safely. It checks the linearityof variables of user-specified types: one variable is usedexactly once. It guarantees that destructive update isinvisible from Gallina program.
• Gallina does not require to release memory but C requires.
→ The linearity checker guarantees to consume a linear variable. It can be used to force a user to invoke amemory freeing function.
• Gallina does not have a loop, but C does.
→ Codegen implements reliable tail recursion elimination.

Our C code generator can generate a C function if E[] ⊢f t.
Figure 21 defines E[Γ] ⊢f t and E[Γ] ⊢b t. E[Γ] ⊢f t determinesthat t is valid function for our C code generator. E[Γ] ⊢b t
determines that t is valid body for our C code generator.

E

Top-Level C Function Generation

Figure 22, Figure 23, and Figure 24 explains the top-level
function generation.
Figure 22 generates C definitions for a Gallina functionthat needs multiple C functions. Figure 23 generates a C function for a Gallina function that needs only one C function.
Figure 24 chooses them. Assuming a Gallina function c is defined as Definition c := t, it needs multiple functions whena function bounded by a fixpoint in t is called as a function(not goto) and c itself is not usable to call the function.
For example, half function defined as follows is mutually
defined with uphalf function. half invokes uphalf in a tailposition but uphalf invokes half in a non-tail position.
Definition half :=fix half n :=match n with O ⇒ O | S m ⇒ uphalf m end
with uphalf n :=match n with O ⇒ O | S m ⇒ S (half m) end
for half.

Codegen generates half as a single function that contains
the bodies of both functions. This is because all recursive
calls are translatable to goto or a function call to the toplevel function (half): half invokes uphalf using goto; uphalf
invokes half using a usual function call.
static nat half(nat v1_n) {nat v2_m, v3_n, v4_m, v5_n;switch (v1_n) {case 0: return 0;
default: v2_m = pred(v1_n);v3_n = v2_m;
goto entry_uphalf;}entry_uphalf:switch (v3_n) {case 0: return 0;
default: v4_m = pred(v3_n);v5_n = half(v4_m);
return succ(v5_n);}}

Details of Argument Completion

Figure 18 explains the detail of argument completion.

C

The Gallina Subset for C Code
Generation

Formalized C Variable Allocation

Figure 19 and Figure 20 formalizes C variable allocation. Figure 19 defines the syntax of a mapping from Gallina variables
to C variables. Figure 20 generates a variable mapping for a
Gallina term.

26

PEPM ’21, January 18–19, 2021, Virtual, Denmark

Akira Tanaka• FJtK considers t to be a top-level function or a closure-generating expression. F transforms t to be a nested abstraction
expression that takes all arguments. Fixpoint expressions are allowed outside or between the abstractions.
• BRJtKm,q transforms a branch of a match expression into a nested abstraction expression that takes constructor
members. Fixpoint expressions are not allowed.
• EJt / x 1 . . . xp Kq is a term convertible with t x 1 . . . xp that does not contain a partial application. EJt / x 1 . . . xp Kq
traverses t while tracking the arguments for t to find closure-generating expressions. The number of arguments given tot is p + q. The first p arguments are x 1 . . . xp and they can be the argument of beta-var redex. The last q arguments
cannot be the argument of beta-var redex.

λx . FJuKt = λx . u
FJtK = fix (fi := FJti K)i=1...h for f j t = fix (fi := ti )i=1...h for f jλx 1 . . . λxm . EJt / x 1 . . . xm K0 otherwise (eta expansion)
where t : T1 → · · · → Tm → T0
T0 is an inductive typex 1 . . . xm are fresh variables
EJt / Kq

BRJtKm,q = λx . BRJuKm−1,qλx 1 . . . λxm . EJt / x 1 . . . xm Kq
where x 1 . . . xm are fresh variables

m=0
m > 0 ∧ t = λx . uotherwise (eta expansion)x
t = x ∧p = q = 0x x . . . x
t = x ∧ ¬(p = q = 0) ∧ r = 0
1
p





FJx
x
.
.
.
x
K
t
= x ∧ ¬(p = q = 0) ∧ r > 0
1
p





(t = c ∨ t = C) ∧ r = 0
t x 1 . . . x p(t = c ∨ t = C) ∧ r > 0 FJt x 1 . . . xp K
 FJtKt = λx . u ∧ p = q = 0
EJt / x 1 . . . xp Kq =

EJu{x/x 1 } / x 2 . . . xp Kq
t = λx . u ∧ p > 0 ∧ r = 0 (beta-var)





λx
.
EJu
/
K
t = λx . u ∧ ((p = 0 ∧ q > 0) ∨ r > 0)
p+q−1





EJu / x 0 x 1 . . . xp Kq
t = u x0
t = let x := t 1 in t 2 (zeta-app)
 let x := EJt 1 / K0 in EJt 2 / x 1 . . . xp Kq match x with (Ci ⇒ BRJti KNMC ,p+q )i=1...h end x 1 . . . xp t = match x with (Ci ⇒ ti )i=1...h endi (fix (f := FJt K)
t = fix (fi := ti )i=1...h for f ji
i i=1...h for f j ) x 1 . . . x p
where t : T1 → · · · → Tp → Tp+1 → · · · → Tp+q → Tp+q+1 → · · · → Tp+q+r → T0
T0 is an inductive type
Note:

This transformation assumes t is not dependently typed: no type terms and no dependent match-expressions.

Figure 18. Argument completion.

Gx : Gallina variablebuffer Implementationbuffer type can be implemented in C as Figure 26. unit typev : C variable

is also implemented.
make_buffer allocates a buffer, buf_addch adds a characterto the buffer destructively, and free_buffer deallocates thebuffer.
buf_addch and free_buffer have side effects but it is not
visible from Gallina as far as buffer type is used linearly.
Codegen causes an error for a non-linear use of buffer typevariables when buffer type is declared as linear.

V = empty | x 7→ v | V ; V
Figure 19. Variable mapping from Gallina to C.

F list bool Implementation
list bool type can be implemented in C as Figure 25. This
implementation uses malloc() but not free(). Thus a con-servative GC is required.

27

Coq to C Translation with Partial Evaluation

PEPM ’21, January 18–19, 2021, Virtual, Denmark

CVJt / x 1 . . . x n KV is the variable mapping of the variables declared in t.
x 1 . . . x n are arguments for t. V is the variable mapping for variables declared outside.

empty





CVJu / KV ;M ; M





CVJu / x 2 . . . x n KV ;M ; M





CVJu / x 0 x 1 . . . x n KV CVJt 1 / KV ; CVJt 2 / x 1 . . . x n KV ;M ; MCVJt / x 1 . . . x n KV =
( CVJt 1 / x 1 . . . x n KV ;M1 ; . . . ;





CVJth / x 1 . . . x n KV ;Mh ; M 1 ; . . . ; Mh )CVJt 1 / KV ;M ; . . . ; CVJth / KV ;M ; M





where v, vi , vi j are fresh C variablesNote:t = x ∨t =c ∨t =C ∨t =T
t = λx . u ∧ n = 0 where M = x 7→ v
t = λx . u ∧ n > 0 where M = x 7→ V (x 1 )t = u x0t = let x := t 1 in t 2 where M = x 7→ v
t = match x with (Ci ⇒ λyi1 . . . λyi NMCi . ti )i=1...h end
where Mi = yi1 7→ vi1 ; . . . ; yi NMCi 7→ vi NMCit = fix (fi := ti )i=1...h for f j
where M = f 1 7→ v 1 ; . . . ; fh 7→ vh

We consider Gallina variables unique.

Figure 20. C variable allocation.
E[Γ] ⊢b x

E[Γ] ⊢b c

E[Γ] ⊢b t

E[Γ] ⊢ x : T

E[Γ] ⊢b C

T is a non-dependent inductive type
E[Γ] ⊢b t x
E[Γ] ⊢b t E[Γ :: (x := t :T )] ⊢b u T is a non-dependent inductive type
E[Γ] ⊢b let x := t : T in u
E[Γ] ⊢ x : T T is a non-dependent inductive type with p parameters: I u 1 . . . up
E[] ⊢ Ci u 1 . . . up : Ti1 → · · · → Ti NMCi → T

Ti j are non-dependent inductive types

E[Γ :: (yi1 :Ti1 ) :: · · · :: (yi NMCi :Ti NMCi )] ⊢b ti
E[Γ] ⊢b match x with (Ci ⇒ λyi1 . . . λyi NMCi . ti )i=1...h end
E[Γ :: (x :T )] ⊢b t

T is a non-dependent inductive type
E[Γ] ⊢b λx :T . t
E[Γ] ⊢f fix (fi : Ti := ti )i=1...h for f j
E[Γ] ⊢b fix (fi : Ti := ti )i=1...h for f j
E[Γ] ⊢ t : T

T is a non-dependent inductive type E[Γ] ⊢b t
E[Γ] ⊢f t
E[Γ :: (x :T )] ⊢f t T is a non-dependent inductive type
E[Γ] ⊢f λx :T . t
E[Γ :: (f 1 :T1 ) :: · · · :: (fh :Th )] ⊢f ti
E[Γ] ⊢f fix (fi : Ti := ti )i=1...h for f j
Figure 21. The Gallina subset for C code generation.

28

PEPM ’21, January 18–19, 2021, Virtual, Denmark

Akira Tanaka

GENFUNM JcK translates the function (constant) c with one or more auxiliary functions. We assume c is defined as
Definition c := t . The auxiliary functions f 1 . . . fn are fixpoint bounded functions in t which are invoked as functions. We
assume the types of them:c : T01 → · · · → T0m0 → T00
fi : Ti1 → · · · → Timi → Ti0

i = 1. . .n

where Ti0 are inductive types (i = 0 . . . n)
The formal arguments of c are x 01 . . . x 0m0 = fvarsJtK and the formal arguments of fi are x i1 . . . x imi = fvars′Jfi K.
fi invocation in C needs extra arguments, yi1 : Ui1 . . . yioi : Uioi , addition to the actual arguments in Gallina application
because the free variables of the fixpoint should also be passed. If the free variables contain a function bounded by an outer
fixpoint, the function itself is not passed but the free variables of the outer fixpoint are also passed. We iterate it until no
fixpoint functions.
GENFUNM JcK = “enum_entriesJcK arg_structdefsJcK forward_declJcK entry_functionsJcK body_functionJcK”

enum_entriesJcK = “enum enum_func_c {func_c,func_f 1 , . . . ,func_fn };”arg_structdefsJcK = “main_structdefJcK aux_structdefJcK1 . . . aux_structdefJcKn ”
main_structdefJcK = “struct arg_c {T01 arg1; . . . T0m0 argm 0 ; };”aux_structdefJcKi = “struct arg_fi { Ui1 outer1; . . . Uioi outeroi ;Ti1 arg1; . . . Timi argmi ; };”forward_declJcK = “static void body_function_c(enum enum_func_c g,void *arg,void *ret);”entry_functionsJcK = “main_functionJcK aux_functionJcK1 . . . aux_functionJcKn ”
main_functionJcK = “static T00 c(T01 x 01 , . . . ,T0m0 x 0m0 ) {struct arg_c arg = {x 01 , . . . ,x 0m0 }; T00 ret;body_function_c(func_c,&arg,&ret);return ret;}”
aux_functionJcKi = “static Ti0 fi (Ui1 yi1 , . . . ,Uioi yioi ,Ti1 x i1 , . . . ,Timi x imi ) {struct arg_fi arg = {yi1 , . . . ,yioi ,x i1 , . . . ,x imi }; Ti0 ret;body_function_c(func_fi ,&arg,&ret); return ret;}”body_functionJcK = “static void body_function_c(enum enum_func_c g,void *arg,void *ret) {decls
switch (g) { aux_caseJcK1 . . . aux_caseJcKn main_caseJcK }}”GENBODYBK JtK

aux_caseJcKi = “case func_fi :yi1 = ((struct arg_fi *)arg)->outer1; . . . ; yioi = ((struct arg_fi *)arg)->outeroi ;x i1 = ((struct arg_fi *)arg)->arg1; . . . ; x imi = ((struct arg_fi *)arg)->argmi ;goto entry_fi ;”main_caseJcK = “default:;
x 01 = ((struct arg_c *)arg)->arg1; . . . ; x 0m0 = ((struct arg_c *)arg)->argm 0 ;”where decls is local variable declarations for variables used in GENBODYBK JtK.
K(e) = “*(T00 *)ret = e;return;”

Figure 22. Translation for a top-level function which is translated to multiple C functions.

29

Coq to C Translation with Partial Evaluation

PEPM ’21, January 18–19, 2021, Virtual, Denmark

GENFUNS JcK translates the function (constant) c to a single C function.

GENFUNS JcK = “staticT0 c( fargs′JtK) { decls GENBODYBK JtK }”where c is defined as Definition c : T1 → · · · → Tn → T0 := t .
T0 is an inductive typedecls is local variable declarations for variables used in GENBODYBK JtK excluding fargsJtK.

K(e) = “return e;”“T x, fargsJuK” t = λx :T . ufargsJtK = fargsJt j K
t = fix (fi := ti )i=1...h for f j “”otherwise
fargs′JtK = fargsJtK without the trailing comma

Figure 23. Translation for a top-level function which is translated to a single C function.
(
GENFUNJcK =GENFUNM JcK t needs multiple functions
GENFUNS JcK otherwise

where c is defined as Definition c := t .

Figure 24. Translation for top-level function.
#include <stdlib.h>#include <stdbool.h> /* bool, true, false */typedef bool unit; static const unit tt = true;
typedef struct {unsigned char *mem; size_t len; size_t max;
} *buffer;

struct list_bool_tag {bool head;struct list_bool_tag *tail;};typedef struct list_bool_tag *list_bool;buffer make_buffer(nat max) {buffer buf;if ((buf = malloc(sizeof(*buf))) == NULL) abort();if (max == 0) max = 16; /* avoid malloc(0) */if ((buf→mem = malloc(max)) == NULL) abort();buf→len = 0; buf→max = max;
return buf;}
buffer buf_addch(buffer buf, unsigned char c) {if (buf→max <= buf→len) {unsigned char *mem; size_t max = buf→max * 2;
if ((mem = realloc(buf→mem, max)) == NULL)
abort();
buf→mem = mem; buf→max = max;}
buf→mem[buf→len++] = c;return buf;}
unit free_buffer(buffer buf) {free(buf→mem); free(buf);
return tt;}#define lb_nil NULL
static list_bool lb_cons(bool h, list_bool t) {list_bool c;if ((c = malloc(sizeof(*c))) == NULL)
abort();
c→head = h;c→tail = t;return c;}#define lb_is_nil(l) ((l) == lb_nil)#define lb_head(l) ((l)→head)#define lb_tail(l) ((l)→tail)Figure 25. list bool implementation in C.

Figure 26. buffer implementation in C.

30

PEPM ’21, January 18–19, 2021, Virtual, Denmark

Akira Tanaka

References[6] Pierre Letouzey. 2003. A New Extraction for Coq. In Types for Proofs
and Programs, Second International Workshop, TYPES 2002, Berg en Dal,
The Netherlands, April 24-28, 2002 (Lecture Notes in Computer Science,Vol. 2646), Herman Geuvers and Freek Wiedijk (Eds.). Springer-Verlag.
https://doi.org/10.1007/3-540-39185-1_12[7] Eric Mullen, Stuart Pernsteiner, James R Wilcox, Zachary Tatlock, and
Dan Grossman. 2018. Œuf: minimizing the Coq extraction TCB. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified
Programs and Proofs. 172–185. https://doi.org/10.1145/3167089[8] Gonzalo Navarro. 2016. Compact data structures: A practical approach. Cambridge University Press.
https://doi.org/10.1017/
CBO9781316588284[9] Akira Tanaka, Reynald Affeldt, and Jacques Garrigue. 2018. Safe lowlevel code generation in Coq using monomorphization and monadification. Journal of Information Processing 26 (2018), 54–72. https://doi.org/10.2197/ipsjjip.26.54[10] The Coq Development Team. 2020. The Coq Proof Assistant. https://coq.inria.fr/.
[11] The Coq Development Team. 2020. The Coq reference manual: Release
8.12.0. (2020).

[1] Abhishek Anand, Andrew Appel, Greg Morrisett, Zoe
Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu
Sozeau, and Matthew Weaver. 2017. CertiCoq: A verified compiler for
Coq. In The Third International Workshop on Coq for Programming
Languages (CoqPL).
[2] Lars Birkedal, Mads Tofte, and Magnus Vejlstrup. 1996. From region inference to von Neumann machines via region representation
inference. In Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 171–183. https://doi.org/10.1145/237721.237771[3] Olivier Danvy and Lasse R Nielsen. 2005. CPS transformation of betaredexes. Inform. Process. Lett. 94, 5 (2005), 217–224. https://doi.org/10.
1016/j.ipl.2005.02.002[4] Cormac Flanagan, Amr Sabry, Bruce F Duba, and Matthias Felleisen.
1993. The essence of compiling with continuations. In Proceedings of
the ACM SIGPLAN 1993 conference on Programming language design
and implementation. 237–247. https://doi.org/10.1145/155090.155113[5] Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun.
ACM 52, 7 (2009), 107–115. https://doi.org/10.1145/1538788.1538814

31