10.6092/issn.1972-5787/5122
When verifying that compiler phases preserve some property of the compiled program, a major difficulty resides in how to represent and manipulate variable bindings, often imposing extra complexity both on the compiler writer and the verification effort.In this paper, we show how Beluga's dependent contextual types let us use higher-order abstract syntax (HOAS) to implement a type-preserving compiler for the simply-typed lambda-calculus, including transformations such as closure conversion and hoisting.  Unlike previous implementations, which have to abandon HOAS locally in favor of a first-order binder representation, we are able to take advantage of HOAS throughout the compiler pipeline, so that the compiler code stays clean and we do not need extra lemmas about binder manipulation.  Our work demonstrates that HOAS encodings offer substantial benefits to certified programming.Scope and type safety of the code transformations are statically guaranteed, and our implementation nicely mirrors the paper proof of type preservation, and can hence be seen as an encoding of the proof which happens to be executable as well.
application/pdf
1972-5787
5122
1
en
Brigitte Pientka
Journal of Formalized Reasoning
Type-preserving Compilation
Programming type-safe transformations using higher-order abstract syntax
Text.Serial.Journal
https://jfr.unibo.it/
8
Articles
2015-12-02
2015-05-22
2015-01-26
2019-11-05
49-91
JFR
Brigitte Pientka
2015/12/02
10.6092/issn.1972-5787/5122
49
School of Computer Science
McGill University
1972-5787
1
Type-preserving Compilation
en
91
Programming type-safe transformations using higher-order abstract syntax
https://jfr.unibo.it/article/download/5122/5330
8
Programming type-safe transformations using
higher-order abstract syntax
OLIVIER SAVARY BELANGER
McGill University
STEFAN MONNIER
Universite de Montreal
and
BRIGITTE PIENTKA
McGill University


When verifying that compiler phases preserve some property of the compiled program, a major
difficulty lies in how to represent and manipulate variable bindings. This often imposes extra
complexity both on the compiler writer and the verification effort.
   In this paper, we show how Beluga’s dependent contextual types let us use higher-order abstract
syntax (HOAS) to implement a type-preserving compiler for the simply-typed lambda-calculus,
including transformations such as closure conversion and hoisting. Unlike previous implementa-
tions, which have to abandon HOAS locally in favor of a first-order binder representation, we are
able to take advantage of HOAS throughout the compiler pipeline, so that the compiler code stays
clean and we do not need extra lemmas about binder manipulation. Our work demonstrates that
HOAS encodings offer substantial benefits to certified programming.
   Scope and type safety of the code transformations are statically guaranteed, and our implemen-
tation nicely mirrors the paper proof of type preservation. It can hence be seen as an encoding of
the proof which happens to be executable as well.




1.   INTRODUCTION
Formal methods are particularly important for compilers, since any compiler bug
could potentially completely defeat all the efforts put into proving properties of
your program.
   For this reason, while mainstream compilers still rely mostly on extensive test
suites, there have been many efforts at developing other ways to ensure the proper
behaviour of compilers. Proving actual correctness of a compiler is a very large
undertaking. Even just formalizing what it means for a compiler to be correct is
itself a lot of work, which involves formalizing the lexer, parser, and semantics of
both the source and the target languages.
   While some applications do require this amount of assurance, our work focuses on
a simpler problem, which is to prove that the compiler preserves the types. This is
an interesting compromise in the design space, because on the one hand we believe
type-preservation can be proved at a reasonable cost, and on the other hand this
property is sufficient to cover the vast majority of cases, namely those programs
where the only property proved and thus preservable is that it is properly typed.
   Earlier work in this area started with so-called typed intermediate representa-
tions, which amounted to testing type-preservation throughout the execution of
the compiler [Tarditi et al., 1996; Shao and Appel, 1995; Benton et al., 1998]. This
                                       Journal of Formalized Reasoning Vol. 8, No. 1, 2015, Pages 49–91.
50     ·     Olivier Savary Belanger et al.

came at a significant runtime cost, associated with engineering costs to try and
keep this runtime cost under control [Shao et al., 1998]. More recent work instead
tries to write the compiler in such a way that type-preservation can be verified stat-
ically [Chlipala, 2008; Guillemette and Monnier, 2008]. One of the main difficulties
when implementing code transformations relates to the representation of binders
in the source and target languages: in order for the verification tool to understand
how bindings are manipulated, the compiler typically needs to use techniques such
as de Bruijn indices, which tend to be very inconvenient and make the code harder
to understand and debug.
   A solution to this last problem is to use higher-order abstract syntax (HOAS), an
elegant and high-level representation of bindings in which binders are represented
in the object languages as binders in the meta-language. This eliminates the risk of
scoping errors, and saves the programmer the trouble to write the usual α-renaming
and the notoriously delicate capture-avoiding substitution. However, while the
power and elegance of HOAS encodings have been demonstrated in representing
proofs, for example in the Twelf system [Pfenning and Schürmann, 1999], it has
been challenging to exploit its power in program transformations which rearrange
abstract syntax trees and move possibly open code fragments. For example the
closure conversion phase of a compiler has generally been considered challenging to
implement with HOAS as we must calculate and reason about the free variables of
a term.
   In this work, we show how the rich type system and abstraction mechanisms of
the dependently-typed language Beluga [Pientka and Dunfield, 2010; Cave and
Pientka, 2012; Pientka and Cave, 2015] enable us to implement a type and scope
preserving compiler for the simply-typed lambda-calculus using HOAS for its stages,
including translation to continuation-passing style (CPS), closure conversion, and
hoisting. This hence also demonstrates that HOAS does support elegant implemen-
tations of program transformations such as closure conversion.
   Beluga is a dependently-typed proof and programming environment which pro-
vides a sophisticated infrastructure for implementing languages and formal systems
based on the logical framework LF [Harper et al., 1993]. This allows program-
mers to uniformly specify the syntax, inference rules, and derivation trees using
higher-order abstract syntax (HOAS) and relieves users from having to build up
a common infrastructure to manage variable binding, renaming, and (single) sub-
stitution. Beluga provides in addition support for first-class contexts [Pientka,
2008] and simultaneous substitutions [Cave and Pientka, 2013], two common key
concepts that frequently arise in practice. Compared to existing approaches, its
infrastructure is one of the most advanced for prototyping formal systems [Felty
et al., 2015].
   While Beluga’s infrastructure for specifying languages and formal systems is
very expressive, the proof and programming language used to analyze and ma-
nipulate HOAS trees that depend on assumptions remains simple. In terms of
proof-theoretical strength, Beluga provides a first-order proof language with in-
ductive definitions [Cave and Pientka, 2012] and domain-specific induction prin-
ciples [Pientka and Abel, 2015]. However instead of inductively reasoning about
simple domains such as natural numbers or lists, Beluga supports representing,
analyzing and manipulating HOAS trees that may depend on assumptions.
Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
      Programming type-safe transformations using higher-order abstract syntax             ·     51

   There are two key ingredients we crucially rely on in our work of encoding type-
preserving program transformations: First, we encode our source and target lan-
guages using HOAS within the logical framework LF, reusing the LF function space
to model object-level binders. As a consequence, we inherit support for α-renaming,
capture-avoiding substitution, and fresh name generation from LF. Second, we ex-
ploit Beluga’s ability to analyze and manipulate HOAS trees that depend on a
context of assumptions using pattern matching. In fact this is crucial to character-
ize abstract syntax trees with free variables, and to manipulate and rearrange open
code fragments. Both these ingredients provide an elegant conceptual framework to
tackle code transformations which re-arrange (higher-order) abstract syntax trees.
   Taking advantage of Beluga’s support for dependent types, our code uses the
technique of intrinsic typing. This means that rather than writing the compilation
phases and separately writing their type preservation proof, we write a single piece
of code which is both the compiler and the proof of its type preservation. If we
look at it from the point of view of a compiler writer, the code is made of fairly
normal compilation phases manipulating normal abstract syntax trees, except an-
notated with extra type annotations. But if we look at it from the point of view of
formal methods, what seemed like abstract syntax trees are actually encoding typ-
ing derivations, and the compilation phases are really encoding the proofs of type
preservation. In a sense, we get the proof of type preservation “for free”, although
in reality it does come at the cost of extra type annotations. This kind of technique
is particularly beneficial when the structure of the proof mirrors the structure of
the program, as is the case here.
   In the rest of this article, we first present our source code and how to encode
it in Beluga, and then for each of the three compilation phases we present, we
first show a manual proof of its type preservation and then show how that proof is
translated into an executable compilation phase in Beluga. The full development
is available online at http://complogic.cs.mcgill.ca/beluga/cc-code.

2.   SOURCE LANGUAGE:
We present, in this section, the source language for our compiler as well as its
encoding in Beluga. All our program transformations share the same source lan-
guage, a simply typed lambda calculus extended with tuples, selectors fst and rst,
let-expressions and unit written as () (see Fig. 1).
   We represent n-ary tuples as nested binary tuples and unit, i.e. a triple for ex-
ample is represented as (M1 , (M2 , (M3 , ()) ) ). In particular, environments arising
during the closure conversion phase will be represented as n-ary tuples.
   Dually, n-ary product types are constructed using the binary product T × S
and unit; the type of a triple can then be described as T1 × (T2 × (T3 × unit)).
Foreshadowing closure conversion and inspired by the type language of Guillemette
and Monnier [2007], we add a special type code S T . This type only arises as a

     (Type)    T, S ::= S → T | code S T | T × S | unit
     (Source) M, N ::= x | lam x. M | M N | fst M | rst M | (M1 , M2 ) | let x = N in M | ()
     (Context) Γ    ::= · | Γ, x : T


                             Fig. 1.   Syntax of the source language

                                                Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
52     ·       Olivier Savary Belanger et al.


           Γ ` M : T Source term M has type T in context Γ

                    Γ, x : T ` M : S            Γ ` M : T → S Γ ` N : T t app
                                       t lam
                  Γ ` lam x. M : T → S                Γ`M N :S

       Γ ` M : T Γ, x : T ` N : S            Γ`M :T ×S                 Γ`M :T ×S
                                  t let                    t first                   t rest
         Γ ` let x = M in N : S              Γ ` fst M : T             Γ ` rst M : S

              Γ`M :T Γ`N :S                     x:T ∈Γ
                                   t cons              t var                         t unit
               Γ ` (M, N ) : T × S              Γ`x:T                Γ ` () : unit


                           Fig. 2.   Typing rules for the source language

result of closure conversion. However since the type language will remain unchanged
during all our transformations, we include it from the beginning, although there
are no source terms of type code S T .
   The typing rules for the source language are given in Fig. 2 and are standard. The
lambda-abstraction lam x. M is well-typed, if M is well-typed in a typing context
extended with a typing assumption for x. The application M N has type S, if the
source term M has the function type T → S and N has type T . The let-expression
let x = M in N is well-typed at type S, if M has some type T and N has type S in
a context extended with the typing assumption x : T . Variables are well-typed, if
a typing assumption for them is present in the context. Selectors fst M and rst M
are well-typed, if M has a product type T × S.
2.1   Representing the Source Language in LF
The first obvious question when trying to encode the source language in a program-
ming environment is how to represent the binders present in the lambda-abstraction
lam x. M and the let-expression let x = M in N . We encode the source language in
the logical framework LF [Harper et al., 1993] which allows us to take advantage
of higher-order abstract syntax (HOAS), a technique where we model binders in
our object language (for example the variable x in lam x. M ) using the binders in
the logical framework LF. In other words, variables bound by lambda-abstraction
and let-expressions in the object-language will be bound by λ-abstraction in the
meta-language. As a consequence, we inherit α-renaming and term-level substitu-
tion. HOAS encodings relieve users from building up a common infrastructure for
dealing with variables, assumptions, and substitutions.
   In Beluga’s concrete syntax, the kind type declares an LF type family (see
Fig. 3). In particular, we declare the type family tp together with constructors
nat, arr, code, cross, and unit to model the types in our object language. This is
unsurprising. For representing source terms we use an intrinsically typed represen-
tation: by indexing source terms with their types, we represent typing derivations
of terms rather than terms themselves, such that we only manipulate well-typed
source terms. An LF term of type source T in a context Γ, where T is a tp, corre-
sponds to a typing derivation Γ ` M : T . We note that in LF itself, the context Γ
is ambient and implicit. However, as we will see shortly, we can pack the LF object
source T together with the context Γ in which it is meaningful forming a contextual
object [Nanevski et al., 2008] which can then be manipulated and analyzed via

Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
     Programming type-safe transformations using higher-order abstract syntax               ·     53


    LF tp: type =
    |   nat     :   tp
    |   arr     :   tp → tp → tp
    |   code    :   tp → tp → tp
    |   cross   :   tp → tp → tp
    |   unit    :   tp
    ;

    LF source : tp → type =
    |   lam     :   (source S → source T) → source (arr S T)
    |   app     :   source (arr S T) → source S → source T
    |   fst     :   source (cross S T) → source S
    |   rst     :   source (cross S T) → source T
    |   cons    :   source S → source T → source (cross S T)
    |   nil     :   source unit
    |   letv    :   source S → (source S → source T) → source T;


                          Fig. 3.   Encoding of the source language in LF

pattern matching in Beluga.
   We model lambda-abstractions in the source language by the constructor lam
which takes as argument an LF-abstraction of type source S → source T. Hence,
the source term lam x. lam y. x y is represented as lam (λx.lam (λy.app x y)) where
λ is an LF binder. Similarly, we represent the let-expression let x = M in N in the
source language by the constructor letv which takes in two arguments, the represen-
tation of the term M and the body of the let-expression N . The fact that the body of
the let-expression depends on the variable x is enforced by giving it the LF-function
type source S → source T. Hence the source term lam x. lam y. let w = x y in x w is
represented as lam (λx.lam (λy.letv (app x y) (λw.app x w))). We encode n-ary tu-
ples as lists, using constructors cons and nil, the latter doubling as representation
of (). We represent selectors fst and rst using the constructor fst and rst respec-
tively. We prefer this representation to one that would group an arbitrary number
of terms in a tuple for simplicity: as we index our terms with their types, and
without computation in types, such tuples would have to carry additional proofs of
the well-typedness of tuples and of their projections, which, while possible, would
be cumbersome.
   When manipulating such objects, we often have to manipulate open subterms,
which requires some way to clarify the context in which they are meant to be used.
Beluga represents and embeds such open fragments using the notions of contextual
objects and first-class contexts. A contextual object, written as [Γ ` M], charac-
terizes an open LF object M which may refer to the bound variables listed in the
context Γ. Correspondingly, the contextual type [Γ ` A] classifies the contextual
objects [Γ ` M] where M has type A in the context Γ. By embedding contextual ob-
jects into computations, users can not only characterize abstract syntax trees with
free variables, but also manipulate and rearrange open code fragments using pat-
tern matching. Both these ingredients provide an elegant conceptual framework to
tackle code transformations which re-arrange (higher-order) abstract syntax trees.
   Since contexts are first-class, we can also pattern match on them and for example
determine which variables indeed occur in M . This is critical in our implementation
of closure conversion.

                                                 Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
54     ·     Olivier Savary Belanger et al.

3.    CONTINUATION PASSING STYLE
As a first program transformation, we consider translating a direct-style source
language into a continuation-passing style (CPS) target language. This is typically
the first step in a compiler for functional languages. Continuation-passing style
means that the control flow of the program is passed explicitly to functions, as
an extra argument. This argument, called a continuation, will consume the result
of the function before proceeding with the execution of the program. In essence,
translating a program into continuation-passing style moves all function calls to
a tail position and enables further analysis and optimizations. Our continuation-
passing style transformation algorithm is adapted from Danvy and Filinski [1992].
3.1    Target Language
Let us first review the language targeted by our CPS transformation.

           (Value)        V     ::=      x | lam (x, k). P | (V1 , V2 ) | ()
           (Expression)   P, Q ::=       V1 V2 K | let x = V in P
                                   |     let x = fst V in P | let x = rst V in P | K V
           (Continuation) K     ::=      k | λx.P
           (Context)      ∆     ::=      · | ∆, x : T | ∆, k ⊥T


      ∆ ` V : T Value V has type T in context ∆

                      x:T ∈∆                 ∆, x : T, k ⊥S ` P ⊥
                             t kvar                                   t klam
                      ∆`x:T                 ∆ ` lam (x, k). P : T → S

                    ∆ ` V1 : S ∆ ` V2 : T
                                            t kcons                       t knil
                     ∆ ` (V1 , V2 ) : S × T               ∆ ` () : unit

      ∆ ` P ⊥ Expression P is well-formed in context ∆

      ∆ ` V1 : S → T ∆ ` V2 : S ∆ ` K ⊥T                      ∆ ` V : T ∆, x : T ` P ⊥
                                         t kapp                                        t klet
                  ∆ ` V1 V2 K ⊥                                 ∆ ` let x = V in P ⊥

        ∆ ` V : S × T ∆, x : S ` P ⊥                   ∆ ` V : S × T ∆, x : T ` P ⊥
                                     t kfst                                         t ksnd
           ∆ ` let x = fst V in P ⊥                       ∆ ` let x = rst V in P ⊥

      ∆ ` K⊥T Continuation K expects as input values of type T in context ∆

                          k ⊥T ∈ ∆                ∆, x : T ` P ⊥
                                   t kvark                       t klamk
                          ∆ ` k ⊥T                ∆ ` λx.P ⊥T



                     Fig. 4.   Typing Rules for the Target Language of CPS

  The target language is divided into values, expressions, and continuations and we
define typing judgments for each. Values consist of variables, lambda-abstractions
and tuples of values. They are typed using judgement ∆ ` V : T , describing that
a value V has type T in the typing context ∆. The typing context ∆ contains
typing assumptions for values x : T , where the variable x stands for a value of
type T , and for continuations k ⊥T , where the variable k stands for a well-typed
Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
      Programming type-safe transformations using higher-order abstract syntax              ·   55


         JxKk               = kx
         Jlam x. M Kk       = k (lam (x, k1 ). P )                where   JM Kk1    =   P
         JM1 M2 Kk          = [(λp.[(λq.p q k)/k2 ]Q)/k1 ]P       where   JM1 Kk1   =   P
                                                                  and     JM2 Kk2   =   Q
         J(M, N )Kk         = [(λp.[(λq.k (p, q))/k2 ]Q)/k1 ]P    where   JM Kk1    =   P
                                                                  and     JN Kk2    =   Q
         Jlet x = N in M Kk = [(λq.let x = q in P )/k2 ]Q         where   JM Kk     =   P
                                                                  and     JN Kk2    =   Q
         Jfst M Kk          = [(λp.let x = fst p in k x)/k1 ]P    where   JM Kk1    =   P
         Jrst M Kk          = [(λp.let x = rst p in k x)/k1 ]P    where   JM Kk1    =   P
         J()Kk              = k ()


                                    Fig. 5.   CPS Algorithm

continuation of the type ⊥T . Continuations are formed either by variables k or
lambda-abstractions λx.P . We think of continuations here as meta-level functions
and we eagerly reduce any β-redexes arising from applying a continuation.
   The typing rules for values are straightforward and resemble the ones for source
terms, with the exception of t lam: lambda-abstractions of the target language take
a continuation as an additional argument. We say that the target term lam (x, k). P
has type T → S, if P is a well-formed expression which may refer to a variable x of
type T and a continuation variable k denoting a well-formed continuation expecting
values of type S as input.
   Expressions P are typed using the judgment ∆ ` P ⊥; it simply states that an
expression P is well-formed in the context ∆. By writing P ⊥ in the judgment
we represent the fact that the expression P does not return anything by itself
but instead relies on the continuation to carry on the execution of the program.
Expressions include application of a continuation K V , application of a function
V1 V2 K, a general let-construct, let x = V in P and two let-constructs to observe
lists, let x = fst V in P and let x = rst V in P .
   Finally, we define when a continuation K is well-typed using the following judg-
ment ∆ ` K⊥T : it must be either a continuation variable or a well-typed lambda-
abstraction expecting an input value of type T in the context ∆. By choosing to
represent continuations here using lambda-abstractions we are already foreshad-
owing our encoding of continuations in the logical framework LF. As we will see,
continuations will be modelled using the LF function space.
3.2   CPS Algorithm
We describe the translation to continuation-passing style following Danvy and Fil-
inski [1992] in Fig. 5 using the function JM Kk = P which takes as input a source
term M and produces a target term P depending on k, where k is a (fresh) variable
standing for the top-level continuation in the translated expression.
  In the variable and unit case, we simply call the continuation. To translate the
lambda-abstraction lam x. M with the continuation k, we translate M using a new
continuation k1 to obtain a term P and then call the continuation k with the term
lam (x, k1 ). P .
  The interesting cases are the ones for applications, pairs, projections, and let-
expressions. Consider translating the application M1 M2 given a continuation k:
                                               Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
56      ·    Olivier Savary Belanger et al.

we first recursively translate Mi using a new continuation ki and obtain resulting
terms P and Q. We now need to create a term which only depends on the original
continuation k. This is accomplished by replacing any occurrence of k2 in Q with the
meta-level function λq.p q k resulting in a term Q0 and replacing any occurrence
of k1 in P with λp.Q0 . We eagerly reduce meta-level β-redexes arising from the
application of these substitutions in the algorithm. This amounts to eliminating
administrative redexes on the fly. The remaining cases follow a similar principle.
  We now give the proof that the given transformation preserves types. While this
proof is standard, we give it in detail, since it will serve as a guide for explaining
our implementation of CPS translation as a function in Beluga. In particular,
we draw attention to structural lemmas, such as weakening and exchange, which
are often used silently in paper proofs, but can pose a challenge when mechanizing
and implementing the CPS-translation together with the guarantee that types are
preserved.
  As the type preservation proof relies crucially on the fact that we can replace
variables denoting continuations with a concrete continuation K, we first state and
prove the following substitution lemma.
   Lemma 3.1. Substitution (Continuation in Expression)
If Γ, k ⊥T ` P ⊥ and Γ ` K ⊥T then Γ ` [K/k]P ⊥
     Proof. Proof by induction on the derivation Γ, k ⊥T ` P ⊥.
  Our main Theorem 3.1 states that a source expression of type T will be trans-
formed by the algorithm given in Fig. 5 to a well-formed target expression expecting
a continuation k of type ⊥T . The typing context of the target language subsumes
the typing context of source term, such that we can use Γ in the conclusion, reading
typing assumptions for source terms as assumptions for target values. The proof of
Theorem 3.1 follows by structural induction on the typing derivation of the source
term. In the proof, terms with a substitution appearing in them should be read as
the terms resulting from the substitution, corresponding to the algorithm reducing
continuation applications eagerly, rather than as terms with a delayed substitution.
     Theorem 3.1. Type Preservation If Γ ` M : T then Γ, k ⊥T ` JM Kk ⊥.
  Proof. By induction on the typing derivation D0 :: Γ ` M : T . We consider
here some representative cases.
           x:T ∈Γ
Case D0 =           t var
           Γ`x:T

where M = x and JM Kk = k x.
Γ`x:T                                                                 by assumption
Γ, k ⊥T ` x : T                                                        by weakening
Γ, k ⊥T ` k ⊥T                                                            by t kvark
Γ, k ⊥T ` k x ⊥                                                           by t kappk
Γ, k ⊥T ` JM Kk ⊥                                                       by definition
                         D
                 Γ, x : T ` M 0 : S
Case D0 =                                 t lam
              Γ ` lam x. M 0 : T → S
Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
      Programming type-safe transformations using higher-order abstract syntax         ·     57

where M = lam x. M 0 and JM Kk = k (lam (. x, k) JM 0 Kk ).
Γ, x : T, k1 ⊥S ` JM 0 Kk1 ⊥                                                    by i.h. on D
Γ ` lam (x, k1 ). JM 0 Kk1 : T → S                                                 by t klam
Γ, k ⊥T →S ` lam (x, k1 ). JM 0 Kk1 : T → S                                    by weakening
Γ, k ⊥T →S ` k ⊥T →S                                                              by t kvark
Γ, k ⊥T →S ` k (lam (x, k1 ). JM 0 Kk1 ) ⊥                                        by t kappk
Γ, k ⊥T →S ` Jlam x. M 0 Kk ⊥                                                   by definition
                  D1                     D2
             Γ ` M0 : S → T            Γ`N :S
Case D0 =                                           t app
                        Γ ` M0 N : T

where M = M 0 N and JM Kk = [λp.[λq.p q k/k2 ] JN Kk2 /k1 ] JM 0 Kk1 .
Γ, k2 ⊥S ` JN Kk2 ⊥                                                         by i.h. on D2
Γ, k ⊥T , p : S → T, q : S ` p : S → T                                           by t kvar
Γ, k ⊥T , p : S → T, q : S ` q : S                                               by t kvar
Γ, k ⊥T , p : S → T, q : S ` k ⊥T                                              by t kvark
Γ, k ⊥T , p : S → T, q : S ` p q k ⊥                                            by t kapp
Γ, k ⊥T , p : S → T ` λq.p q k ⊥S                                              by t klamk
Γ, k ⊥T , p : S → T, k2 ⊥S ` JN Kk2 ⊥                                      by weakening
Γ, k ⊥T , p : S → T ` [λq.p q k/k2 ] JN Kk2 ⊥               by substitution (Lemma 3.1)
Γ, k ⊥T ` λp.[λq.p q k/k2 ] JN Kk2 ⊥S→T                                        by t klamk
Γ, k1 ⊥S→T ` JM 0 Kk1 ⊥                                                     by i.h. on D1
Γ, k ⊥T , k1 ⊥S→T ` JM 0 Kk1 ⊥                                             by weakening
Γ, k ⊥T ` [λp.[λq.p q k/k2 ] JN Kk2 /k1 ] JM 0 Kk1 ⊥        by substitution (Lemma 3.1)
Γ, k ⊥T ` JM 0 N Kk ⊥                                                   by definition
3.3   Representing the Target Language in LF
As with the source language (see Section 2), we encode the target language in
the LF logical framework as intrinsically well-typed terms (see Fig. 6). We reuse
tp, the type index of the source language, to index elements of type value, which
correspond to values. An LF term of type value T in a context Γ, where T is a
tp, corresponds to a typing derivation Γ ` V : T for a (unique) value V in the
target language. Similarly, we use the type exp here to represent well-typed CPS-
expressions: an LF term of type exp corresponds directly to a typing derivation
Γ ` E ⊥ for a (unique) expression E. Continuations are not present at this level;
they are directly represented as LF functions from values to expressions written as
value T → exp.

3.4   Implementation of the Main Theorem
We now implement the translation J−Kk on intrinsically well-typed expressions as
a recursive function in Beluga. Its development mirrors the type preservation
proof and may be viewed as an executable version of it. A central challenge lies
in the fact that our CPS translation (see Fig. 5) is defined on open terms M ,
meaning that they may contain free variables. Since we aim to implement the
translation on intrinsically well-typed terms, M must be well-typed in the context
                                            Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
58     ·      Olivier Savary Belanger et al.


     LF exp : type =
      |    kapp    :   value     (arr S T) → value S → (value T → exp) → exp
      |    klet    :   value     T → (value T → exp) → exp
      |    klet-fst:   value     (cross S T) → (value S → exp) → exp
      |    klet-rst:   value     (cross S T) → (value T → exp) → exp

     and value : tp → type =
      | klam      : (value S → (value T → exp) → exp) → value (arr S T)
      | kcons     : value S → value T → value (cross S T)
      | knil      : value unit ;


                       Fig. 6.    Encoding of the Target Language of CPS in LF

Γ, i.e. all the free variables in M must be declared in Γ. Similarly, P , the result
of our CPS-translation, is open and is well-typed in a context Γ0 which stands
in a one-to-one relation to Γ, i.e. for every source variable declared in Γ there
is a corresponding target variable in Γ0 . Note that in the type preservation proof
(Theorem 3.1) we were cheating a little by conflating the source and target context.
In a mechanization however we are forced to be more precise.
   Because every source variable corresponds to exactly one target variable, we can
give a more uniform view of the context in which both the source and target term
are well-typed, namely as a context containing pairs of variables of type source T
and value T. This could be for example captured informally as follows where x
stands for a source variable and y for a target variable of the same type.

                                  (Context) ∆ ::= · | ∆, (x : T, y : T )
  As an alternative we could have stated the relationship between the source and
target contexts explicitly, but we then would need to separately establish the fact
that the i-th declaration in the source context corresponds exactly to the i-th
declaration in the target context. Using a joint context where we pair assumptions
about source and target variables, we obtain this correspondance for free.
  In Beluga, we define the type of this joint context using a schema, more precisely
we define the type each declaration in the context must satisfy. The keyword block
defines a variable declaration in the context that stands for a pair. So we use it to
associate our source and target variables and we explicitly quantify over the shared
type using the keyword some:
        schema ctx = some [t:tp] block x:source t, y:value t;

  Contexts of schema ctx are ordered sequences of declarations where each variable
declaration in the context is an instances of the given schema. Here are a few
examples.
              b1:block (x1:source nat, y1:value nat),
              b2:block (x2:source (arr nat nat), y2:value (arr nat nat))         X
              b1:block (x:source nat, y:value nat),
              b2:block (x:source unit, y:value unit)                             X
              b1:block (x1:source nat, y1:value unit),
              b2:block (x2:source unit, y2:value unit)
              b1:block (x1:source nat, y1:value nat),
              x2:source (arr nat nat), y2:value (arr nat nat)
Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
     Programming type-safe transformations using higher-order abstract syntax         ·     59

   The first two contexts are well-formed according to the given schema. Each
element is an instance of the schema declaration. The last two contexts are not well-
formed according to the given schema: in the first counter example the elements
in the block do not share the same type and in the second counter example the
context declarations are not grouped into pairs (i.e. blocks).
   Beluga’s schema declarations are similar to world declarations in Twelf [Pfen-
ning and Schürmann, 1999]. However, there is a subtle distinction: in Beluga a
schema declaration simply declares the type of a context; we do not verify that a
given LF type satisfies this context. Instead we use the type of a context to ex-
press invariants about contextual object and their types when we pack an LF term
together with the context in which it is meaningful.
   Our CPS translation function cpse, presented in Fig. 7, takes as input a source
term M of type source S in a joined context Γ and returns a well-typed expression
which depends on Γ and the continuation k of type ⊥S . This is stated in Beluga
as follows:
    rec cpse : (Γ:ctx)[Γ ` source S[]] → [Γ, k: value S[] → exp ` exp]

   where [Γ ` source S[]] is the contextual type describing the type and scoping of
the source argument. Similarly, [Γ, k: value S[] → exp ` exp] describes how the
output can depend on Γ and on the continuation k of type ⊥S .
   By writing (Γ:ctx) we quantify over Γ in the given type and state the schema
Γ must satisfy. The type checker will then guarantee that the function cpse only
manipulates contexts of schema ctx and we are only considering source terms in such
a context. By wrapping the context declaration in round parenthesis we express
at the same time that Γ remains implicit in the use of this function, where curly
brackets would denote an explicit dependent argument. In other words, (Γ:ctx) is
simply a type annotation stating the schema the context Γ must have, but we do
not need to pass an instantiation for Γ explicitly to the function cpse when making
a function call.
   We refer to variables occurring inside a contextual object (such as the S in [Γ `
source S[]] above) as meta-variables to distinguish them from variables bound by
function abstraction in the actual program. All meta-variables are associated with a
postponed substitution which can be omitted, if the substitution is the identity. In
stating the type of the function cpse we however want to make sure that the type S
of the expression is closed. We therefore associate it with a weakening substitution,
written as [], which weakens the closed type S (i.e. ` S:tp). In other words [] is a
substitution from the empty context to the context Γ.
   We further note that S was free in the type annotation for cpse. Beluga’s type
reconstruction [Pientka, 2013; Ferreira and Pientka, 2014] will infer the type of S
as [ ` tp] which can be read as “S has type tp in the empty context”.
   Our implementation of the CPS translation (see Fig. 7) consists of a single down-
ward pass on the input source program. It follows closely the proof of type preserva-
tion (Theorem 3.1) for the algorithm. The case analysis on the typing derivation in
the proof corresponds to the case analysis via pattern matching on the intrinsically
well-typed source expression. The appeals to the induction hypothesis in the proof
correspond to the recursive calls in our program.
   Let us look at the program more closely. The first pattern, #p.1 matches the first

                                           Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
60     ·     Olivier Savary Belanger et al.


     rec cpse : (Γ:ctx)[Γ ` source S[]] → [Γ, k: value S[] → exp ` exp]
     fn e ⇒ case e of
     | [Γ ` #p.1] ⇒ [Γ, k:value _ → exp ` k (#p.2[...])]
     | [Γ ` app M N] ⇒
       let [Γ, k1:value (arr T[] S[]) → exp ` P] = cpse [Γ ` M] in
       let [Γ, k2:value T[] → exp             ` Q] = cpse [Γ ` N] in
          [Γ, k:value S[] → exp ` P [..., (λf. Q[..., (λx. kapp f x k)])]]
     | [Γ ` lam λx. M] ⇒
        let [Γ, x:source S ` M] = [Γ, x:source _ ` M] in
        let [Γ, b:block (x:source S[], y:value S[]), k1:value T[]→ exp
              ` P[...,b.2, k1] =
             cpse [Γ, b:block (x:source S[], y:value S[]) ` M [..., b.1] in
           [Γ, k:value (arr S[] T[]) → exp ` k (klam (λx.λk1. P[..., x, k1]))]
     ...;


                           Fig. 7.   Implementation of CPS in Beluga

field of elements of Γ, corresponding to source variables. Formally, #p describes a
variable of type [Γ ` block (x:source T[], y:value T[]]) for some closed type T and
#p.1 extracts the first element. As mentioned above, meta-variables appearing in
contextual objects are associated with a substitution describing which part of the
context they may depend on. For convenience, Beluga allows users to omit writ-
ing the identity substitution stating that the meta-variable depends on the whole
context Γ. Therefore, we simply write #p.1 in the previous pattern. Alternatively,
we could have written #p.1[...], where ... represents the identity substitution over
Γ, making explicit the fact that a given parameter variable #p may depend on the
declarations from the context Γ.
   When we encounter a source variable #p.1, we apply the continuation k to the
corresponding target variable. Since we have paired up source and target variables
in Γ and #p describes such a pair, we simply call k with the second field of #p. Type
reconstruction fills in the _ in the type of k with the type of the matched variable.
Note that we apply the weakening substitution [..] to #p.2, as we return a target
term in the context Γ, k:value _ → exp.
   In the application case, we match on the pattern app M N and recursively transform
M and N to target terms P and Q respectively. We then substitute for the continuation
variable k2 in Q a continuation consuming the local argument of an application. A
continuation is then built from this, expecting the function to which the local
argument is applied and substituted for k1 in P producing a well-typed expression,
if a continuation for the resulting type S is provided.
   We take advantage of Beluga’s built-in substitution here to model the substi-
tution operation present in our algorithm in Fig. 5. The term (λx. kapp f x k) that
we substitute for references to k2 in Q will be β-reduced wherever that k2 appears
in a function call position, such as the function calls introduced by the #p.1 case.
We hence reduce administrative redexes using the built-in LF application.
   Note that in the type preservation proof we rely on weakening to justify applying
the substitution lemma. In our implementation we also rely on weakening although
it is subtle to see, since Beluga’s type system silently takes care of it. Weakening is
used to justify using the target term Q which is well-typed in Γ, k2:value T[] → exp
in the target term (λf. Q[..., (λx. kapp f x k)]) which is well-typed in the context
Γ, k:value S[] → exp.

Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
      Programming type-safe transformations using higher-order abstract syntax         ·     61

   In the λ-abstraction case, we want to recursively translate M which is well-typed
in the context Γ, x:source S[]. Note that from the pattern Γ ` lam λx.M we only
know [Γ, x: source _ ` M] where the underscore makes explicit the fact that we do
not yet have the name S for the type of x. We explicitly introduce a name for the
type of x by pattern matching on [Γ, x: source _ ` M] and then recursively trans-
late M in the context Γ, b:block (x:source S[],y:value S[]). Note that introducing
a name S is necessary in Beluga, since Beluga’s type reconstruction presently
does not take into account dependencies among blocks of declarations and hence
fails to infer the type for y. Moreover, we note that while M was well-typed in
the context Γ, x: source S[], when making the recursive call, we want to use it
in the context Γ, b:block (x:source S[], y:value S[]). We hence associate M with a
weakening substitution which maps x to the first part of the block b. The result
of recursively translating M is described as a target expression P which depends on
the continuation k1 and the target variable given by the second part of the block.
In other words, P is well-typed in Γ, y:value S[], k1:value T[]→ exp. In general, P
could depend on both variables declared in the block b, but because a target expres-
sion can never depend on source variables restricting P is justified. This is verified
in Beluga by the coverage checker which takes into account strengthening based
on subordination which constructs a dependency graph for type families (see for
a similar analysis [Virga, 1999; Harper and Licata, 2007]). Using this dependency
graph, we can justify that an object M of type A cannot depend on some objects
of type B, i.e. there is no way of constructing M using an assumption of type B.
Hence, if a term M was well-typed in a context that contained also declarations of
type B, we can always strengthen M to be well-typed in a context where we drop
all the assumptions of type B.
   We return [Γ, k:value (arr S[] T[]) → exp ` k (klam λx.λk1.P[...,x, k1])] as the
final result. To guarantee that the term k (klam λx.λk1. P[..., x, k1]) is well-typed,
we observe that P[..., x, k1] is well-typed in Γ, x:value S,k1:value T[] → exp, the
extended context, and Beluga’s typing rules will silently employ weakening (by
k:value (arr S[] T[]) → exp ) to type-check (klam λx.λk1. P[..., x, k1]) in the con-
text Γ, k:value (arr S[] T[]) → exp.
   The remaining cases are similar and in direct correspondence with the proof of
Theorem 3.1. In the let-expressions, we rely on inferring the type of variables in a
similar fashion as in the lambda-abstraction case.
3.5   Discussion
The implementation of the type-preserving transformation into continuation-passing
style in Beluga, including the definition of the type, source and target languages,
amounts to less than 65 lines of code. We rely crucially on the built-in support
for weakening, strengthening, and substitution. Beluga’s features such as pattern
variables, built-in substitution and first-class contexts make for a straightforward
representation of the transformation as a single function, while dependent types
allow us to build the type preservation proof into the representation of the trans-
formation with little overhead.
   The fact that this algorithm can be implemented elegantly in languages support-
ing HOAS is not a new result. A similar implementation was given as an example
in the Twelf tutorial presented at POPL 2009 [Car, 2009]. Guillemette and Mon-
                                            Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
62     ·     Olivier Savary Belanger et al.

nier [2006] and Chlipala [2008], both using a term representation based on HOAS,
achieve similar results, respectively in Haskell and in Coq.
  We have also implemented a CPS transformation in Beluga over System F,
an extension of the simply typed lambda calculus where types may depend on
type variables. Few changes are required for our simply typed implementation to
support System F: removing the weakening substitution (written as []) associated
with types so that they may depend on type variables in the context suffices as
sole modification to the cases included in the implementation over a simply-typed
language.
  While we present here the implementation using a joint context, an alternative
would be to have distinct contexts for source and target variables. We would have
to carry an explicit relation stating that for every variable in the source contexts,
a variable of the same type is present in the target context. This would be closer
to the technique used for the other transformations presented in this paper (see
Sections 4 and 5); however we would need to also explicitly infer that the i-th
declaration in the source context corresponds to the i-th declaration in the target
context. Carrying an explicit relation between contexts would also complicate the
extension to System F, as types would have to be transported from the source to
the target contexts in order to appear in different contextual objects.

4.    CLOSURE CONVERSION
The second program transformation we consider is closure conversion. It makes the
manipulation of closure objects explicit and results in a program whose functions
are closed so that they can be hoisted to the top-level.
   In a typical compiler pipeline, the CPS transformation precedes closure conver-
sion. However, closure conversion does not depend in any essential way on the fact
that its input is continuation-passing. For clarity, we present closure conversion as
a transformation on programs in direct style, i.e. not in continuation passing style.
4.1   Target Language
In addition to functions lam y. P , function application P Q, tuples (P, Q), selectors
fst and rst, and let-expressions let y = P in Q, our target language for closure
conversion now contains two new constructs (see Fig. 8): 1) we can form a closure
hP, Qi of an expression P with its environment Q, represented as an n-ary tuple.
2) we can break apart a closure P using let hyf , yenv i = P in Q.
   The idea of closure conversion is to make the evaluation context of functions
explicit; variables bound outside of a function are replaced by projections from
an environment variable. Given a source-level function lam x. M of type T →
S, we return a closure hlam yc . P, Qi consisting of a closed function lam yc . P and
its environment Q. The variable yc stands for a pair of the local argument y,
standing in for x, and an environment variable yenv whose projections replace free

               (Target)  P, Q ::= y | lam y. P | P Q | fst P | rst P | let y = P in Q
                                 | (P, Q) | () | hP, Qi | let hyf , yenv i = P in Q
               (Context) ∆    ::= · | ∆, y : T | ∆, l


                 Fig. 8.   Syntax of the Target Language for Closure Conversion

Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
      Programming type-safe transformations using higher-order abstract syntax                 ·    63


       ∆`P :T         Target P has type T in context ∆

               ∆, x : T ` P : S                    ∆ ` P : code T S ∆ ` Q : T
                                    t clam                                    t capp
            ∆ ` lam x. P : code T S                        ∆`P Q:S

                      ∆ ` P : T ∆, x : T ` Q : S                x:T ∈∆
                                                 t clet                t cvar
                       ∆ ` let x = P in Q : S                   ∆`x:T

             ∆`P :T ×S                   ∆`P :T ×S
                           t cfst                      t csnd                         t cnil
             ∆ ` fst P : T               ∆ ` rst P : S                ∆ ` () : unit

      · ` P : code (T × Tenv ) S    ∆ ` Q : Tenv                ∆`P :T ∆`Q:S
                                                    t cpack                         t ccons
                ∆ ` hP, Qi : T → S                               ∆ ` (P, Q) : T × S

               ∆`P :T →S           ∆, yf : code (T × l) S, yenv : l ` Q : S
                                                                              t cletpackl
                            ∆ ` let hyf , yenv i = P in Q : S


            Fig. 9.   Typing Rules for the Target Language of Closure Conversion

variables of M . Such packages are traditionally given an existential type such as
∃l.(code (T × l) S) × l where l is the type of the environment. We instead use
T → S to type the closure packages, hiding l and saving us from having to handle
existential types in their full generality. The rules for t pack and t letpack are
modelling implicitly the introduction and elimination rules for existential types.
Moreover, with the rule t pack, we enforce that P is closed. The remaining typing
rules are similar to the typing rules for the source language (see Fig. 9).
4.2   Closure Conversion Algorithm
Before describing the algorithm in detail, let us illustrate briefly closure conversion
using an example. Our algorithm translates the program (lam x. lam y. x + y) 5 2
to

          let hf1 , c1 i = let hf2 , c2 i = h lam e2 . let x     = fst e2
                                                           xenv = rst e2
                                                       in h lam e1 . let y      = fst e1
                                                                          yenv = rst e1
                                                                      in fst yenv + y
                                                          , (x, ()) i
                                            , () i
                           in f2 (5 , c2 )
          in f1 (2, c1 )
  Closure conversion introduces an explicit representation of the environment, clos-
ing over the free variables of the body of an abstraction. We represent the envi-
ronment as a tuple of terms, corresponding to the free variables in the body of the
abstraction.
  We define the algorithm for closure conversion in Fig. 10 using JM Kρ , where
M is a source term which is well-typed in some context Γ and ρ is a mapping of
source variables in Γ to target terms in some context ∆. Intuitively, ρ maps source
variables to the corresponding projection of the environment.
                                                   Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
64      ·      Olivier Savary Belanger et al.


     JxKρ                = ρ(x)
     Jlam x. M Kρ        = h lam yc . let y = fst yc in let yenv = rst yc in P , Penv i
                           where {x1 , . . . , xn } = FV(lam x. M )
                           and ρ0 = x1 7→ π1 yenv , . . . , xn 7→ πn yenv , x 7→ y
                           and Penv = (ρ(x1 ), . . . , ρ(xn )) and P = JM Kρ0
     JM N Kρ             = let hyf , yenv i = P        where P = JM Kρ and Q = JN Kρ
                           in yf (Q , yenv )
     Jlet x = M in N Kρ = let y = P in Q               where P = JM Kρ and Q = JN K(ρ,x7→y)
     J(M, N )Kρ          =   (P , Q)                   where P = JM Kρ and Q = JN Kρ
     Jfst M Kρ           =   fst P                     where P = JM Kρ
     Jrst M Kρ           =   rst P                     where P = JM Kρ
     J()Kρ               =   ()


                             Fig. 10.    Closure Conversion Algorithm




        ∆`ρ:Γ         ρ maps variables from source context Γ to target context ∆

                                            ∆`ρ:Γ ∆`P :T
                                  m id                               m dot
                     ∆ ` id : ·             ∆ ` ρ, x 7→ P : Γ, x : T
   The identity, written as id, maps the empty source context to any target context
(see rule m id). We may extend the domain of a map ρ from Γ to Γ, x : T by
appending the mapping x 7→ P to ρ, where P has type T in the target context ∆,
using rule m dot.
   Were the source and target languages the same, a map ∆ ` ρ : Γ would be the
exact encoding of substitution from context Γ to context ∆. For this reason, we
refer to maps as substitutions interchangeably in the remainder of this paper. For
convenience, we write πi for the i-th projection instead of using the selectors fst
and rst. For example, π2 M corresponds to the term fst (rst M ).
   The closure conversion algorithm given in Fig. 10 translates a well-typed source
term M using the map ρ. To translate a source variable, we look up its binding in
the map ρ. To translate tuples and projections, we translate the subterms before
reassembling the result using target language constructs. () is directly translated
to its target equivalent. Translating the let-expression let x = M in N involves
translating M using the mapping ρ and translating N with the extended map
ρ, x 7→ y, therefore guaranteeing that the map provides instantiations for all the
free variables in N , before reassembling the converted terms using the target let-
construct. The interesting cases of closure conversion arise for λ-abstraction and
application.
   When translating a λ-abstraction lam x. M , we first compute the set {x1 , ..., xn }
of free variables occurring in lam x. M . We then form a closure consisting of two
parts:
(1) A term P , obtained by converting M with the new map ρ0 which maps variables
    x1 , ..., xn to their corresponding projection of the environment yenv and x to

Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
     Programming type-safe transformations using higher-order abstract syntax         ·     65

    itself, thereby eliminating all free variables in M .
(2) An environment tuple Penv , obtained by applying ρ to each variable in (x1 , ..., xn ).
   When translating an application M N , we first translate M and N to target
terms P and Q respectively. Since the source term M denotes a function, the
target term P will denote a closure and we extract the two parts of the closure
using a let-pack construct where the variable yf describes the function and yenv
stands for the environment. We then apply the extended environment (Q, yenv ) to
the function described by the variable yf .
   Following our earlier ideas, we implement the described algorithm in Beluga as
a recursive program which manipulates intrinsically well-typed source terms. Re-
call that intrinsically typed terms represent typing derivations and hence, our pro-
gram can be viewed as an executable transformation over typing derivations. To
understand better the general idea behind our implementation and appreciate its
correctness, we again discuss first how to prove that given a well-typed source term
M we can produce a well-typed target term which is the result of converting M .
The proof relies on several straightforward lemmas which we discuss below. We
then use this proof as a guide to explain our type-preserving implementation of
closure conversion. As we will see the lemmas necessary in the type preservation
proof correspond exactly to auxiliary functions needed in our implementation.
   Most of the lemmas arise from proving that translating λ-abstractions preserves
typing. For example when translating a λ-abstraction, we compute the set of free
variables that in fact occur in the body of the abstraction. This set of free variables
and their associated types form a subset of the overall typing context. To argue
that types are preserved we need a strengthening lemma for source terms (see
Lemma 4.1) which justifies that the body remains well-typed in the smaller context
which only tracks the free variables occurring in it.
   Lemma 4.1. Term Strengthening
If Γ ` M : T and Γ0 = F V (M ) then Γ0 ⊆ Γ and Γ0 ` M : T .
  Proof. Proof using an auxiliary lemma: if Γ1 , Γ2 ` M : T and Γ01 = F V (M )\Γ2
then Γ01 ⊆ Γ1 and Γ01 , Γ2 ` M : T which is proven by induction on Γ1 .
  Term Strengthening (Lemma 4.1) says that the set of typing assumption Γ0 as
computed by FV is sufficient to type any term M provided that this term M is
well-typed in the context Γ.
  The result of translating the body of the abstraction is a target term P ; for it to
be meaningful again in the original typing context, we will need to use weakening
(see Lemma 4.2). As we will see in the implementation of our algorithm in Beluga,
this form of weakening is obtained for free while the strengthening properties must
be established separately. In the type preservation proof itself, we also rely on
weakening source terms which allows us to weaken the tuple describing the free
source variables in the body of the λ-abstraction to its original context. Hence we
state two weakening lemmas.
  Lemma 4.2. Term Weakening
(1 ) If Γ0 ` M : T and Γ0 ⊆ Γ then Γ ` M : T .
(2 ) If ∆, ∆0 ` P : T then ∆, x : S, ∆0 ` P : T .
                                           Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
66      ·    Olivier Savary Belanger et al.

  Proof. Proof (1) using an auxiliary lemma: if Γ01 , Γ2 ` P : T and Γ01 ⊆ Γ1 then
Γ1 , Γ2 ` P : T which is proven by induction on Γ01 .
Proof of (2) is the standard lemma for weakening target terms.
   Term Weakening (Lemma 4.2) says that a source term M stays well-typed at
type T if we weaken its typing context Γ to a context Γ0 containing all of the
assumptions in Γ. It is stated dual to the previous strengthening lemma such that
first strengthening a term and then weakening it again, results in the same original
source term. To prove term weakening for source terms, we need to generalize. The
weakening lemma for target terms is stated in the standard way.
   Since our algorithm abstracts over the free variables x1 , . . . , xn and creates an
environment as an n-ary tuple, we also need to argue that the type of the environ-
ment can always be inferred and exists. Intuitively, given the set of free variables
and their types, i.e. x1 :T1 , . . . , xn :Tn , we can form the type T1 × . . . × Tn together
with a well-typed map which associates each xi with the i-th projection. This is
justified by the following context reification lemma.
  Lemma 4.3. Context Reification
Given a context Γ = x1 : T1 , . . . , xn : Tn , there exists a type TΓ = (T1 ×. . .×Tn ) and
there is a ρ = x1 7→ π1 yenv , . . . , xn 7→ πn yenv such that yenv : T1 × . . . × Tn ` ρ : Γ
and Γ ` (x1 , . . . , xn ) : T1 × . . . × Tn .
     Proof. By induction on Γ.
Context Reification (Lemma 4.3) says that it is possible to represent a context Γ
of typing assumptions as a single typing assumption yenv by creating a product
type which consists of all the typing assumptions in Γ. The substitution ρ acts as
a witness and transports any term meaningful in Γ to one solely referring to yenv .
  Finally, we establish some basic lemmas about looking up an element in our
mapping ρ between source variables and their corresponding target terms and about
extending the mapping (see lemma 4.4 and 4.5).
   Lemma 4.4. Map Extension
If ∆ ` ρ : Γ then ∆, y : T ` ρ, x 7→ y : Γ, x : T .
     Proof. Induction on the definition of ∆ ` ρ : Γ.
The Map Extension Lemma 4.4 says that we can extend any substitution ρ by the
identity, mapping a source variable x to a new target variable of the same type. This
does not follow directly from the definition of the map. Instead, it is necessary to
weaken all judgments of the form ∆ ` P : S contained in ρ by the formation rule
m dot to judgments of the form ∆, x : T ` P : S.
   Lemma 4.5. Map Lookup
If x : T ∈ Γ and ∆ ` ρ : Γ, then ∆ ` ρ(x) : T .
     Proof. Induction on the definition of ∆ ` ρ : Γ.
   Map Lookup (Lemma 4.5) states, intuitively, that substitutions as encoded by
our mapping judgment work as intended: ρ associates any variable in Γ to a term
of the same type in the target context ∆.

Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
      Programming type-safe transformations using higher-order abstract syntax              ·     67

   Lemma 4.6. Map Lookup (Tuple)
If Γ ` (x1 , . . . , xn ) : T and ∆ ` ρ : Γ then ∆ ` (ρ(x1 ), . . . , ρ(xn )) : T .
  Proof. By Lemma 4.5 and inversion on the typing rules.
Map Lookup (Tuple) (Lemma 4.6) says that applying a substitution ρ to each
component of a variable tuple will transport the tuple from the domain of the
substitution Γ to its codomain ∆ while preserving the type of the tuple.
  We now are ready to show that our closure conversion algorithm preserves types.
The proof is mostly straightforward except for the λ-abstraction case which is the
most difficult.
   Theorem 4.1. Type Preservation
If Γ ` M : T and ∆ ` ρ : Γ then ∆ ` JM Kρ : T .
   Proof. By induction on the typing derivation D0 :: Γ ` M : T . We only show
a few key cases. The other cases are similar.
                D
              x:T ∈Γ
Case D0 =                  t var
              Γ`x:T

where M = x and ∆ ` ρ : Γ.
∆ ` ρ(x) : T                                                                     by Map Lookup
∆ ` JxKρ : T                                                                        by definition
                         D
                 Γ, x : T ` M 0 : S
Case D0 =                                t lam
              Γ ` lam x. M 0 : T → S

where M = lam x. M 0 and ∆ ` ρ : Γ.
Γ0 ` lam x. M 0 : T → S and Γ0 ⊆ Γ where Γ0 = F V (lam x. M 0 )                       by Term Str

Γ0 ` (x1 , . . . , xn ) : TΓ0 and yenv : TΓ0 ` ρ0 : Γ0              by Context Reification
Γ ` (x1 , . . . , xn ) : TΓ0                                       by Term Weakening (1)
∆`ρ:Γ                                                                       by assumption
let (ρ(x1 ), . . . , ρ(xn )) = Penv
∆ ` Penv : TΓ0                                                     by Map Lookup (tuple)
yenv : TΓ0 , y : T ` ρ0 , x 7→ y : Γ0 , x : T                            By Map Extension
yenv : TΓ0 , y : T ` P : S where P = JM 0 Kρ0 ,x7→y                            by i.h. on D
yc : T × TΓ0 , yenv : TΓ0 , y : T ` P : S                          by Term Weakening (2)
yc : T × TΓ0 , y : T, yenv : TΓ0 ` P : S                                      by Exchange
yc : T × TΓ0 , y : T ` let yenv = rst yc in P : S                             by rule t clet
yc : T × TΓ0 ` let y = fst yc in let yenv = rst yc in P : S                   by rule t clet
· ` lam yc . let y = fst yc in let yenv = rst yc in P : code (T × TΓ0 ) S    by rule t clam
∆ ` hlam yc . let y = fst yc in let yenv = rst yc in P , Penv i : T → S by rule t cpack
∆ ` Jlam x. M 0 Kρ : T → S                                                    by definition


                                                 Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
68     ·      Olivier Savary Belanger et al.


        LF target: tp → type =
        |   clam    : (target T → target S) → target (code T S)
        |   capp    : target (code T S) → target T → target S
        |   cpack   : target (code (cross T L) S) → target L → target (arr T S)
        |   cletpack: target (arr T S)
                   → ({l:tp} target (code (cross T l) S) → target l → target S)
                   → target S
        |   cfst : target (cross T S) → target T
        |   crst : target (cross T S) → target S
        |   ccons: target T → target S → target (cross T S)
        |   cnil : target unit
        |   clet : target T → (target T → target S) → target S;


             Fig. 11.   Encoding of the Target Language of Closure Conversion in LF

                    D1                        D2
               Γ ` M0 : S → T               Γ`N :S
Case D0 =                                              t app
                           Γ ` M0 N : T

where M = M 0 N and ∆ ` ρ : Γ.
∆ ` JM 0 Kρ : S → T                                                           by i.h. on D1
∆ ` JN Kρ : S                                                                 by i.h. on D2
∆, yenv : l ` JN Kρ : S                                             by Term Weakening (2)
∆, yenv : l ` yenv : l                                                        by rule t cvar
∆, yenv : l ` (JN Kρ , yenv ) : (S × l)                                     by rule t ccons
∆, yf : code (S × l) T, yenv : l ` (JN Kρ , yenv ) : (S × l)        by Term Weakening (2)
∆, yf : code (S × l) T ` yf : code (S × l) T                                  by rule t cvar
∆, yf : code (S × l) T, yenv : l ` yf : code (S × l) T              by Term Weakening (2)
∆, yf : code (S × l) T, yenv : l ` yf (JN Kρ , yenv ) : T                    by rule t capp
∆ ` let hyf , yenv i = JM 0 Kρ in yf (JN Kρ , yenv ) : T                  by rule t cletpack
∆ ` JM 0 N Kρ : T                                                         by definition
4.3   Representing the Target Language in LF
Our implementation of type-preserving closure conversion in Beluga translates an
intrinsically well-typed source term to an intrinsically well-typed target term. For
source terms we will reuse the data type definition given earlier (see Fig. 3).
   Target terms are defined in LF (see Fig. 11) following the typing rules from Fig. 9
using the type family target which is indexed by types. This allows us to only
consider well-typed target terms. Note that our target terms for closure conversion
differ from the target terms used in CPS. We are taking advantage of HOAS and
model the binding structure in abstractions and let-expressions by piggybacking on
LF’s function space. Our data-type definition directly reflects the typing rules with
one exception: our typing rule t pack enforced that P was closed. This cannot be
achieved in the LF encoding, since the context of assumptions is ambient. As a
consequence, hoisting, which relies on the fact that the closure converted functions
are closed, cannot be implemented as a separate phase after closure conversion. We
will come back to this issue in Section 5.



Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
      Programming type-safe transformations using higher-order abstract syntax         ·     69

4.4   Type Preserving Closure Conversion in Beluga: an Overview
We now implement the closure conversion algorithm as a transformation of intrin-
sically typed source terms to intrinsically typed target terms. Our main function cc
corresponds closely to the type preservation proof. Its type is a direct encoding of
the type-preservation theorem and can be read as follows: given well-typed source
terms in a source context Γ and a map of the source context Γ to the target context
∆, it returns a well-typed target term in the target context ∆. We again ensure
that the type T is closed by associating it with a weakening substitution.
       cc: Map [∆] [Γ] → [Γ ` source T[]] → [∆ ` target T[]]

  Here Map [∆] [Γ] refers to an indexed recursive data-type which encodes the
context relation between the target context ∆ and the source context Γ (see page
63 for the formal description given earlier). Before we give its definition, we define
the type of a context using a schema declaration. The schema for source and target
contexts can be defined as follows:
       schema tctx = target T;
       schema sctx = source T;

   The schema tctx describes contexts where each declaration is an instance of type
target T  and encodes the structure of target contexts as defined by the grammar;
similarly the schema sctx describes contexts where each declaration is an instance
of type source T. In the remainder of this section and in Section 5, we will use
the convention of writing Γ to name contexts characterized by the schema sctx,
and ∆ for contexts of schema tctx. We note that our typing rule for t letpack also
introduces type variables. This might suggest that we must include them in our
schema definition for the target context. However, type variables only occur locally
and are always bound before the term is returned by our closure conversion function.
Therefore well-typed terms never depend on these type variables. As we remarked
earlier, a schema declaration simply declares an invariant that the context satisfies
when we translate well-typed source terms to well-typed target terms. The schema
declaration does not enforce that in general we can only build terms that have
this form. In fact, our data type for target terms allows it – however the schema
declaration defines a context invariant that is more restrictive and is satisfied in
the type preservation proof and also in our implementation of cc.
   We now define Map [∆] [Γ] as an indexed recursive type [Cave and Pientka, 2012]
in Beluga to relate the target context ∆ and source context Γ following the defi-
nition given earlier on page 63. Each of the constructors given directly corresponds
to one of the inference rules defining the relationship between the target and source
context.
       inductive Map:{∆:tctx}{Γ:sctx} ctype =
       | M_id : {∆:tctx} Map [∆] []
       | M_dot: Map [∆] [Γ] → [∆ ` target S[]] → Map [∆] [Γ, x:source S[]];

  In Beluga’s concrete syntax, the kind ctype and the keyword inductive indicate
that we are not defining an LF datatype, but an inductive type on the level of
computations. → is overloaded to mean computation-level functions rather than
the LF function space. Map is defined recursively on the source context Γ directly
encoding our definition ∆ ` ρ : Γ given earlier (see page 63). Note that we can
only embed contextual LF into computation-level (inductive) types not the other
                                            Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
70     ·     Olivier Savary Belanger et al.

way. Once we encounter a box-type or box-object enclosed with [ and ] we leave
the computation-level and descend to contextual LF.
   Beluga reconstructs the type of free variables ∆, Γ, and S and implicitly ab-
stracts over them. In the constructor M_id, we choose to make ∆ an explicit argu-
ment to M_id, since we often need to refer to ∆ explicitly in the recursive programs
we are writing about Map.
4.5   Implementation of Auxiliary Lemmas
Before giving the implementation of the closure conversion function cc, we present
several auxiliary functions which closely correspond to the auxiliary lemmas needed
in the type preservation proof.
  Term strengthening. Our previous strengthening lemma on page 65 stated: if
the source term M is well-typed in the context Γ, then M is also well-typed in
Γ0 = F V (M ) which is a sub-context of Γ. Here we give an algorithmic interpretation
mirroring the proof. We again rely on intrinsic typing here, and hence use a single
function to implement both the F V computation and the strengthening proof.
  Our strengthening function takes as input a well-typed source term M in the
context Γ and returns a strengthened term M’ which is well-typed in some context
Γ0 where Γ0 is a sub-context of Γ, written as Γ0 ⊆ Γ. By construction, Γ0 will
contain all the free variables occurring in M.
  The subset relation between the context Γ and the context Γ0 is defined using
the following indexed recursive computation-level data-type.
        inductive SubCtx: {Γ0 :sctx} {Γ:sctx} ctype =
        | WInit: SubCtx [] []
        | WDrop: SubCtx [Γ0 ] [Γ] → SubCtx [Γ0 ] [Γ, x:source T[]]
        | WKeep: SubCtx [Γ0 ] [Γ] → SubCtx [Γ0 , x:source T[]] [Γ, x:source T[]];

  In the type preservation proof, we strengthen a term lam x. M 0 and compute
Γ = F V (lam x. M 0 ). Then we recursively translate the term M 0 which is well-typed
 0

in Γ0 , x : S. Here, we implicitly rely on the fact that strengthening lam x. M 0 does
not change the shape of the overall term. We might even use the same variable
names. However, because variables can be understood as referring to a specific
position in the contexts (for example as a de Bruijn index), strengthening changes
what position a variable refers to. This is subtle and in fact difficult to obtain
for free in an implementation. Our implementation strengthens a source term M
in Γ, x:source S[] and returns a strengthened version of M, which is well-typed in
the source context Γ0 , x:source S[] together with the proof SubCtx [Γ0 ] [Γ]. By
construction, Γ0 characterizes the free variables in the expression lam λx.M. Since
Beluga does not directly support existential types, we encode this result using the
indexed recursive type StrTerm.
      inductive StrTerm: {Γ:sctx} [ ` tp] → ctype =
      | STm’: [Γ0 ` source T[]] → SubCtx [Γ0 ] [Γ] → StrTerm [Γ] [ ` T];

      rec strengthen:[Γ, x:source S[] ` source T[]] → StrTerm [Γ,x:source S[]] [ ` T]

  Just as in the proof of the term strengthening lemma, we cannot implement the
function strengthen directly. When performing induction on Γ, we cannot appeal to
the induction hypothesis while maintaining a well-scoped source term. Instead, we
implement str, which intuitively implements the lemma
Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
     Programming type-safe transformations using higher-order abstract syntax          ·     71


    LF wrap: tp → nat → type =
    | init: (source T) → wrap T z
    | abs : (source S → wrap T N) → wrap (arr S T) (suc N);

    inductive StrTerm’: {Γ:sctx} [ ` tp] → [ ` nat] → ctype =
    | STm’: [Γ0 ` wrap T[] N[]] → SubCtx [Γ0 ] [Γ] → StrTerm’ [Γ] [ ` T] [ ` N];


    rec str: {Γ:ctx} [Γ ` wrap T[] K[]] → StrTerm’ [Γ] [ ` T] [ ` K]=
    λ2 Γ ⇒ fn e ⇒ case [Γ] of
    | [] ⇒ let [ ` M] = e in STm’ [ ` M] WInit
    | [Γ, x:source _ ] ⇒
      case e of
      | [Γ0 ,x:source _ ` M [...]] ⇒
        let STm’ [h ` M’] rel = str [Γ0 ] [Γ0 ` M] in
           STm’ [h ` M’] (WDrop rel)
      | [Γ0 ,x:source _ ` M] ⇒
        let STm’ [h ` abs λx.M’] rel = str [Γ0 ] [Γ0 ` abs λx. M] in
           STm’ [h,x:source _ ` M’] (WKeep rel)
    ;


    rec strengthen:[Γ,x:source S[] ` source T[]]→ StrTerm [Γ, x:source S[]] [ ` T] =
    fn m ⇒
    let [Γ,x:source _ ` M] = m in
    let STm’ [Γ0 ` abs λx.init M’] wk = str [Γ] [Γ ` abs λx.init M] in
      STm [Γ0 ,x:source _ ` M’] wk;


                      Fig. 12.   Implementation of the Function str

        If Γ1 , Γ2 ` M : T and Γ01 = F V (M ) \ Γ2
        then Γ01 , Γ2 ` M : T and Γ01 ⊆ Γ1 .
  In Beluga, contextual objects can only refer to one context variable, such that
we cannot simply write [Γ1 ,Γ2 ` source T[]]. Instead we define a type family wrap
which abstracts over all the variables in Γ2 . The type family wrap is indexed by the
type T of the source term and the size of Γ2 described by N. The function str then
recursively analyses Γ1 , adding variables occurring in the input term to Γ2 . The
type of str carries with it the index N the size of Γ2 which is preserved. This is
only needed to verify coverage; in the case where we call str, this ensures that the
returned wrapped term will be of the same form.
  The function str, given in Fig. 12, is implemented recursively on the structure
of Γ and exploits higher-order pattern matching to test whether a given variable
x occurs in a term M. As a consequence, we can avoid the implementation of a
function which recursively analyzes M to test whether x occurs in it.
In the function body, λ2 -abstraction introduces the explicitly quantified context
and fn-abstraction introduces a computation-level function. In order to observe the
contextual dependencies of M, we first pattern match on its context Γ. The first
case, Γ = · implies that [ ` M] and hence FV(M ) = ·. As a witness we return the
subcontext relation with the WInit constructor.
In the second case where Γ = (Γ0 , x:source _ ) we pattern match on e to see, if x
occurs. If e matches the pattern [Γ0 , x:source _ ` M[...]], then we are guaranteed
that x, the rightmost variable in the context, does not appear in M. Recall that
associating M with the weakening substitution [...] means that M may only refer to

                                            Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
72     ·     Olivier Savary Belanger et al.

Γ0 . The type of M will be [Γ0 ` source _ ]. We can hence strengthen M to the context
Γ0 by recursively calling str on the subcontext Γ0 , and use the subcontext relation
constructor WDrop to relate Γ and Γ0 ,x:source _ .
Otherwise [Γ0 , x:source _ ` M] matches, meaning that x may occur in M. Recall
that M is implicitly associated with the identity substitution and hence may refer
to Γ0 and x. As the term did not match the first pattern, we know that x must
occur in M; hence we must keep it as part of FV(M ). We use the abs constructor
of the wrap type to add x to the accumulator representing Γ2 , and recursively call
str on the Γ subcontext. As the type index in the recursive call is now suc N, we
are guaranteed that the wrapped term in the output will be of the form abs λx.M’.
Finally we use the WKeep subcontext relation constructor to keep x as part of FV(M).
   The function strengthen then simply calls str. This helps to keep the code modu-
lar. Because str implicitly reasons about the size of Γ2 , we are guaranteed that the
term returned by the function str must be of the form [Γ’` abs λx.M’]. However,
this does not guarantee that the actual size of the term M’ is equal to the size of
M. We will return to this issue when we discuss totality of the closure conversion
function.
   Term weakening. In the formal development, we relied on two weakening lemmas:
in the first we weaken a source term with respect to a given context relation: Given
a well-typed term M in the context Γ0 and Γ0 ⊆ Γ, the term M remains well-typed
in Γ. This form of weakening cannot be obtained for free, since it relies on the
context relation Γ0 ⊆ Γ. It is a general form of weakening. In our implementation,
we incorporated this form of weakening directly into the variable lookup function
discussed below.
   The second form of weakening allows us to weaken a target term, i.e. if a target
term is well-typed in a context ∆, it remains well-typed if we add an additional
assumption. In Beluga, we obtain this kind of weakening for free since contextual
type theory incorporates weakening by individual declarations.
  Map Variable lookup. The function lookup takes as input a Map [∆] [Γ] together
with a source variable of type T in the source context Γ and returns the corresponding
target expression of the same type.
     rec lookup: Map [∆] [Γ] → {#q:[Γ ` source T[]]} [∆ ` target T[]] =
     fn ρ ⇒ λ2 #q ⇒ case ρ of
     | M_dot ρ0 [∆ ` M] ⇒
      let (ρ : Map [∆] [Γ0 ,x:source _) = ρ in
      (case [Γ0 , x:source _ ` #q] of
      | [Γ0 , x:source _ ` x       ] ⇒ [∆ ` M]
      | [Γ0 , x:source _ ` #p[...]] ⇒ lookup ρ’ [Γ0 ` #p] )
     | M_id [∆] ⇒ impossible [ ` #q]

   We quantify explicitly over all variables in the context Γ by {#q:[Γ ` source T[]]}
where #q denotes a variable of type source T[] in the context Γ. The function lookup
is implemented by pattern matching on the map ρ. This makes establishing the
totality of this function straightforward. If ρ is of type Map [∆] [ ], i.e. Γ is empty,
there is no possible variable #q. We can disprove a case by impossible [ ` #q] which
tries to split on the variable #q.
   If ρ is of type Map [∆] [Γ0 , x:source _ ], then there is a ρ0 of type Map [∆] [Γ0 ]
and some target term [∆ ` M] of target type [∆ ` target _ ] corresponding to the
Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
     Programming type-safe transformations using higher-order abstract syntax         ·     73

source variable x. We now check whether x is the variable we are looking for by
pattern matching on [Γ0 , x:source _ ` #q]. There are two cases: either #q stands for
x, in which case we choose the branch with the pattern [Γ0 , x:source _ ` x] and
simply return [∆ ` M], or it stands for another variable from Γ and we choose the
branch with the pattern [Γ0 , x:source _ ` #p [...]] and search the remaining context
Γ0 .
   For the closure conversion algorithm, it is important to know that an n-ary tuple
is composed solely of source variables from the context Γ, in the same order. We
therefore define VarTup as a computational datatype which guarantees that the tuple
only contains variables in the order they occur in Γ.
    inductive VarTup: (Γ:sctx) {T:[ ` tp]} [Γ ` source T[]] → ctype =
    | Empty : VarTup [ ` unit] [ ` nil]
    | Next : VarTup [ ` L] [Γ ` R]
         → VarTup [ ` cross T L] [Γ,x:source _ ` cons x R[...]]
    ;

  The constructor Empty stands for an empty tuple. Given a variable tuple [Γ ` R],
we can form a variable tuple [Γ, x:source _ ` cons x R[...]] using the constructor
Next. Note that we must weaken R to guarantee it is meaningful in the extended
context.
  Next, we translate the tuple VarTup [ ` L] [Γ0 ` R] where SubCtx [Γ0 ] [Γ] to a cor-
responding target term using a mapping ρ between source and target context. In
the type preservation proof, we first weaken the tuple VarTup [ ` L] [Γ0 ` R] to be
meaningful in the context Γ, and then lookup for each xi the corresponding target
term in the mapping ρ. Here, we give a direct implementation which incorporates
weakening directly. The function is defined recursively on SubCtx [Γ0 ] [Γ].
    rec lookupVars: SubCtx [Γ0 ] [Γ] → VarTup [Γ0 ] [ ` L] → Map [∆] [Γ]
                   → [∆ ` target L] =
    fn r ⇒ fn vt ⇒ fn σ ⇒ let (σ : Map [∆] [Γ]) = σ in case r of
    | WInit ⇒
      let Empty = vt in [∆ ` cnil]
    | WDrop r’ ⇒
      let M_dot σ 0 [∆ ` P] = σ in lookupVars r’ vt σ 0
    | WKeep r’ ⇒
      let Next vt’ = vt in
      let M_dot σ 0 [∆ ` P] = σ in
      let [∆ ` M] = lookupVars r’ vt’ σ 0 in
         [∆ ` ccons P M]
    ;

   In the first case, we learn that Γ0 = Γ = · and the variable tuple must be empty;
the corresponding target tuple hence can be represented with cnil in context ∆.
In the second case, the first variable of Γ does not appear in Γ0 , we can thus disregard
it in the tuple construction and we recursively call lookupVars after removing x 7→ P
from σ.
In the third case, the top variable of Γ appears on top of Γ0 as well, and we have
x 7→ P in σ. We recursively construct the tuple representing the rest of Γ0 , before
adding P in front.
  Map Extension. In the type preservation proof, we relied on being able to ex-
tend our map between source Γ and target context ∆. First, we implement the
function weaken which allows us to simply weaken the target context; given a map ρ
between source context Γ and target context ∆, it is straightforward to construct
                                           Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
74        ·   Olivier Savary Belanger et al.

a map between Γ and ∆, x:target S[]. Since our map ρ is only required to provide
mappings for all the source variables in Γ, we recursively analyze the given map ρ
and weaken each element to be meaningful in the extended target context.
   We then use this function to extend a map ρ between the source context Γ and
target context ∆ with an identity mapping, i.e. a new source variable is mapped to
its corresponding target variable. We first retrieve a name for the target context
by re-binding ρ to (ρ : Map [∆] [Γ]). We then weaken ρ using the function weaken
and extend the result with [∆, x:target _ ` x].
      rec weaken: Map [∆] [Γ] → Map [∆, x:target S[]] [Γ] =
      fn ρ ⇒ case ρ of
      | IdMap [∆]         ⇒ IdMap [∆, x:target _]
      | DotMap ρ0 [∆ ` M] ⇒ DotMap (weaken ρ0 ) [∆, x:target _ ` M]
      ;

      rec extend: Map [∆] [Γ] → Map [∆, x:target S[]] [Γ, x:source S[]] =
      fn ρ ⇒ let (ρ : Map [∆] [Γ]) = ρ in
          M_dot (weakenMap ρ) [∆,x:target _ ` x]
      ;

   Context Reification. The context reification lemma is proven by induction on Γ
and our function reify directly implements the proof by pattern matching on the
context Γ. Given a context Γ, the function reify produces a tuple containing vari-
ables of Γ together with Map [xenv :target TΓ ] [Γ], the mapping between those target
variables and their corresponding projections. We call the result an environment
closure, written as EnvClo vt ρ, since we package the variable tuple vt with the en-
vironment ρ. The type of reify enforces that the returned Map contains, for each
of the variables in Γ, a target term of the same type referring solely to a variable
xenv of type TΓ . In particular, we replace a source variable with the corresponding
projection on the target variable xenv . This replacement is elegantly accomplished
by relying on the meta-level substitution. In the function extendEnv, we recursively
analyze the given map ρ which provides mappings from the source context Γ to the
target xenv : target S; for each element in the map ρ we replace any occurrence of
xenv with crst xenv where xenv has now the extended type target (cross T S).
     inductive CtxAsTup: {Γ:sctx} ctype =
     | EnvClo: VarTup [ ` TΓ ] [Γ ` M] → Map [xenv :target TΓ ] [Γ] → CtxAsTup [Γ];

     rec extendEnv: Map [xenv :target S] [Γ] → Map [xenv :target (cross T S)] [Γ] =
     fn ρ ⇒ case ρ of
     | M_id [xenv :target S] ⇒ M_id [xenv :target _]
     | M_dot ρ0 [xenv :target S ` M] ⇒
         M_dot (extendEnv ρ0 ) [xenv :target _ ` M[crst xenv ]]
     ;

     rec reify: {Γ:sctx} CtxAsTup [Γ] =
     λ2 Γ ⇒ case [Γ] of
     | [ ] ⇒ EnvClo Emp (IdMap [x:target unit])
     | [Γ, x:source S[]] ⇒
       let EnvClo vt ρ = reify [Γ] in
       let ρ0 = DotMap (extendEnv ρ) [xenv :target (cross S[] _) ` cfst xenv ] in
          EnvClo (Next vt) ρ0
     ;




Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
      Programming type-safe transformations using higher-order abstract syntax           ·     75


      rec cc: [Γ ` source T[]] → Map [∆] [Γ] → [∆ ` target T[]] =
      fn m ⇒ fn ρ ⇒ case m of

      | [Γ ` #p] ⇒ lookup ρ [Γ ` #p]

      | [Γ ` app M N] ⇒
        let [∆ ` P] = cc [Γ ` M] ρ in
        let [∆ ` Q] = cc [Γ ` N] ρ in
             [∆ ` cletpack P λl.λxf .λxenv . capp xf (ccons (Q [...]) xenv )]

      | [Γ ` lam λx.M] ⇒
        let STm [Γ0 ,x:source _ ` M’] wk = strengthen [Γ, x:source _ ` M] in
        let EnvClo env ρ0 = reify [Γ0 ] in
        let [∆ ` Penv ] = lookupVars wk env ρ in
        let [xenv :target _,x:target _ ` P] = cc [Γ0 ,x:source _ ` M’] (extend ρ0 )
        in [∆ ` cpack (clam λc.clet (cfst c)
                                          (λx.clet (crst c) (λxenv .P [xenv , x])))
                           Penv ]
      ;


                  Fig. 13.   Implementation of Closure Conversion in Beluga

4.6   Type-preserving Closure Conversion Implementation
We now describe the implementation of the type-preserving closure conversion al-
gorithm using the type-preservation proof (Thm. 4.1) as a guide. The top-level
function cc takes as input a well-typed source term, [Γ ` source T[]], together with
a map ρ between the source context Γ and the target context ∆, and returns
a well-typed target term, [∆ ` target T[]]. The function recursively analyzes a
given source term, [Γ ` source T[]]. We concentrate here on the cases for vari-
ables, λ-abstractions and applications. When we encounter a variable, written as
[Γ ` #p], we simply lookup its corresponding binding in ρ. When we encounter an
application, [Γ ` app M N], we recursively translate [Γ ` M] and [Γ ` N] and package
together their results.
   The most interesting case is the one for λ-abstraction, [Γ ` lam λx.M]. We first
strengthen the term to a term [Γ0 ,x:source _ ` M’] where Γ0 describes the free vari-
ables occurring in lam λx.M and wk is a witness for SubCtx [Γ0 ] [Γ], i.e. the fact that
Γ0 is a sub-context of Γ. Next, we reify the context Γ0 into a tuple env describing
the environment and a mapping ρ0 between the source context Γ0 and the target
variable xenv . Recall that ρ0 associates each variable in Γ0 with the corresponding
projection of xenv . Moreover, if Γ0 = xk :source Tk , ..., x1 :source T1 , then xenv has
type target (cross T1 (cross ... (cross Tk unit))) and env is a tuple consisting of
variables x1 , ..., xk .
   Using lookupVars wk env ρ we build a corresponding tuple in the target language,
called [∆ ` Penv ]. By recursively translating [Γ0 ,x:source _ ` M’] with the map ρ0
extended with the identity, we obtain [xenv :target _, x:target _ ` P]. Finally, we
build our result: clam λc.clet (cfst c) (λx. clet (crst c) (λxenv . P [xenv , x])) to-
gether with its environment Penv . Our underlying dependent types guarantee that
our implementation is well-typed.




                                              Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
76     ·     Olivier Savary Belanger et al.

4.7   Discussion
Our implementation of closure conversion, including all definitions and auxiliary
functions, consists of approximately 200 lines of code and follows closely the type-
preservation proof. By taking advantage of the built-in substitution to replace vari-
ables in the source term with their respective projections in the target language,
our implementation remains compact avoiding the need to build and manage in-
frastructure regarding variable bindings and contexts. There is only one instance
where we wish Beluga would support richer abstractions: it is the function for
strengthening. We come back to this point shortly.
   All our auxiliary functions and the main closure conversion function pass the
coverage checker [Dunfield and Pientka, 2009]. All the auxiliary functions also are
accepted by the totality checker [Pientka and Abel, 2015; Pientka and Cave, 2015]
certifying that they are terminating. Certifying that the closure conversion func-
tion is terminating fails. The reason is subtle: in the case for lambda-abstraction
we strengthen [Γ, x:source _ ` M] and obtain [Γ’, x:source _ ` M’]. We then recur-
sively translate [Γ’, x:source _ ` M’]. However, there is no obvious reason why it
is structurally smaller than the original term. Therefore, the totality checker flags
this recursive call as (possibly) not decreasing.
   Note that this is not as dramatic as it seems: while our Beluga code looks very
much like a proof, the actual proof of type preservation is not directly given by our
code but by the meta-theoretical properties of Beluga, which do not depend on
the totality of our code. Instead, type preservation is only guaranteed under the
condition that the code terminates. So the failure of the totality checker means that
we cannot guarantee that the closure conversion will always terminate, but when
it does terminate, we still know that it returns a term of the right type. In this
context, a proof of termination is not terribly important, especially if we consider
that a total function may still fail to terminate within our lifetime.
   How could one guarantee that M’ is indeed equivalent to M up to possibly some
variable renaming? – Intuitively, when we strengthen a term [Γ ` lam λx.M], we
would like to return a strengthened term [Γ0 ` lam λx.M’] together with a strength-
ening substitution Γ ` σ : Γ0 . Since σ is a strengthening substitution and only maps
variables to variables, we then know that [Γ ` lam λx.M’[σ x]] has the same size
as [Γ ` lam λx.M]. Therefore, [Γ0 ,x:source _ ` M’] can be considered smaller than
[Γ,x:source _ ` M] and we can safely convert [Γ0 ,x:source _ ` M’].
   While Beluga supports substitution variables [Cave and Pientka, 2013], it does
not allow us to express and guarantee that these substitutions only map variables
to variables. Hence, we cannot exploit and take advantage of substitution vari-
ables directly. In the same way that Beluga distinguishes between general meta-
variables, written with upper-case letters, and parameter variables, written as lower
case letters prefixed with #, distinguishing between general substitution variables
and variable substitutions is desirable. It would not only allow us to express the
strengthening function more abstractly, but also would simplify reasoning about
the size of strengthened terms. However, in balance, the current implementation is
likely more efficient. Hence, this seems a trade-off between efficiency and guaran-
teeing correctness properties statically.
   Closely related to our work is Guillemette and Monnier [2007], which describes

Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
      Programming type-safe transformations using higher-order abstract syntax           ·     77

the implementation of a type-preserving closure conversion algorithm over STLC
in Haskell. While HOAS is used in the CPS translation, the languages from closure
conversion onwards use de Bruijn indices. They then compute the free-variables of
a term as a list, and use this list to create a map from the variable to its projection
when variable occurs in the term, and to ⊥ otherwise. Guillemette and Monnier
[2008] extend the closure conversion implementation to System F.
   Chlipala [2008] presents a certified compiler for STLC in Coq using parametric
higher-order abstract syntax (PHOAS), a variant of weak HOAS. He however an-
notates his binders with de Bruijn level before the closure conversion pass, thus
degenerating to a first-order representation. His closure conversion is hence similar
to that of Guillemette and Monnier [2007].
   In both implementations, infrastructural lemmas dealing with binders constitute
a large part of the development. Moreover, additional information in types is
necessary to ensure the program type-checks, but is irrelevant at a computational
level. In contrast, we rely on the rich type system and abstraction mechanisms of
Beluga to avoid all infrastructural lemmas.

5.   HOISTING
The last program transformation we consider is hoisting. It lifts λ-abstractions,
closed by closure conversion, to the top level of the program. Function declarations
in the program’s body are replaced by references to a global function environment.
   As alluded to in Sec. 4.3, our encoding of the target language of closure con-
version does not guarantee that functions in a closure converted term are indeed
closed. While this information is available during closure conversion, it cannot
easily be captured in our meta-language, LF. We therefore extend our closure con-
version algorithm to perform hoisting at the same time. Hoisting can however be
understood by itself; we present here a standalone type-preserving hoisting algo-
rithm. As before, we revisit the type preservation proof to guide us in explaining
the implementation.
   When hoisting all functions from a program, each function may depend on func-
tions nested in them. One way of performing hoisting (see Guillemette and Monnier
[2008]) consists of binding the functions at the top level individually. We instead
merge all the functions in a single tuple, representing the function environment,
and bind it as a single variable from which we project individual functions, which
ends up being less cumbersome when using Beluga’s notion of context variables.
   For example, performing hoisting on the closure-converted program presented in
Sec. 4.2
     let hf1 , c1 i =
         let hf2 , c2 i =
             h lam e2 . let x = fst e2 in let xenv = rst e2
                         in h lam e1 . let y = fst e1 in let yenv = rst e1 in fst yenv + y
                            , (x, ()) i
             , () i
         in f2 (5 , c2 )
     in f1 (2, c1 )


                                              Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
78     ·       Olivier Savary Belanger et al.

will result in
           let l = (lam l2 . lam e2 . let x = fst e2 in let xenv = rst e2
                                        in h (fst l2 ) (rst l2 ) , (x, ()) i
                    , lam l1 . lam e1 . let y = fst e1 in let yenv = rst e1 in fst yenv + y
                    , ())
           in let hf1 , c1 i =
                  let hf2 , c2 i = h(fst l) (rst l), ()i
                  in f2 (5, c2 )
              in f1 (2, c1 )
5.1   The Target Language Revisited
We define hoisting on the target language of closure conversion and keep the same
typing rules (see Fig. 9) with one exception: the typing rule for t cpack is replaced
by the following one:

                 l : Tf ` P : code (T × Tx ) S ∆, l : Tf ` Q : Tx
                                                                  t cpack’
                             ∆, l : Tf ` hP, Qi : T → S
   When hoisting is performed at the same time as closure conversion, P is not
completely closed anymore, as it refers to the function environment l. Only at top-
level, where we bind the collected tuple as l, will we recover a closed term. This is
only problematic for t cpack, as we request the code portion to be closed; t cpack’
specifically allows the code portion to depend on the function environment.
   The distinction between t cpack and t cpack’ is irrelevant in our implementation,
as in our representation of the typing rules in LF the context is ambient.
5.2   Hoisting Algorithm
We now define the hoisting algorithm in Fig. 14 using JP Kl = Q ./ E , where
P , Q and E are target terms and l is a variable name which does not occur in
P . Hoisting takes as input a target term P and returns a hoisted target term Q
together with its function environment E, represented as a n-ary tuple of product
type L. We write E1 ◦ E2 for appending tuple E2 to E1 and L1 ◦ L2 for appending
the product type L2 to L1 . Renaming and adjustment of references to the function
environment are performed implicitly in the presentation, and binding l is taken to
uniquely name function references.
   While the presented hoisting algorithm is simple to implement in an untyped
setting, its extension to a typed language demands more care with respect to the
form and type of the function environment. As ◦ is only defined on n-ary tuples and
product types and not on general terms and types, we enforce that the returned
environment E and its type L are of the right form. We define separately ∆ `l E : L
restricting ∆ ` E : L to a n-ary tuple E of product type L.

           ∆ `l E : L      E is a well-formed tuple of type L in target context ∆

                                                ∆ ` P : T ∆ `l E : L
                                  env nil                            env cons
                 ∆ `l () : unit                  ∆ `l (P, E) : T × L

Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
        Programming type-safe transformations using higher-order abstract syntax          ·     79


JxKl                      = x ./ ()
JhP1 , P2 iKl             = h(fst l) (rst l), Q2 i ./ E       where JP1 Kl = Q1 ./ E1
                                                                and JP2 Kl = Q2 ./ E2
s                      {                                        and E = (lam l. Q1 , E1 ◦ E2 )
 let hxf , xenv i = P1       let hxf , xenv i = Q1
                           =                       ./ E       where JP1 Kl = Q1 ./ E1
 in P2                   l
                             in Q2
                                                               and    JP2 Kl = Q2 ./    E2
                                                               and    E = E1 ◦ E2
Jlam x. P Kl              = lam x. Q ./ E                     where   JP Kl = Q ./      E
JP1 P2 Kl                 = Q1 Q2 ./ E1 ◦ E2                  where   JP1 Kl = Q1 ./    E1
                                                               and    JP2 Kl = Q2 ./    E2
Jlet x = P1 in P2 Kl      = let x = Q1 in Q2 ./ E1 ◦ E2       where   JP1 Kl = Q1 ./    E1
                                                               and    JP2 Kl = Q2 ./    E2
J(P1 , P2 )Kl             = (Q1 , Q2 ) ./ E1 ◦ E2             where   JP1 Kl = Q1 ./    E1
                                                               and    JP2 Kl = Q2 ./    E2
Jfst P Kl                 = fst Q ./ E                        where   JP Kl = Q ./      E
Jrst P Kl                 = rst Q ./ E                        where   JP Kl = Q ./      E

J()Kl                     = () ./ ()


                                 Fig. 14.   Hoisting Algorithm

  The type correctness of hoisting depends on a number of lemmas. In particular,
we rely on a number of properties about those environments represented as n-ary
tuples containing target terms; for example, weakening states that given a target
term P which depends on an environment l : Lf , it remains well-typed given an
extended environment l : L where either L = Lf ◦L0 or L = L0 ◦Lf ; also, appending
two well-typed environments yields a well-typed environment.
   Lemma 5.1. Append Function Environments
If ∆ `l E1 : L1 and ∆ `l E2 : L2 , then ∆ `l E1 ◦ E2 : L1 ◦ L2 .
  Proof. By induction on the derivation ∆ `l E1 : L1 .
  Append Function Environments (Lemma 5.1) states that appending two environ-
ments remains well-typed. Thus, appending two tuples E1 and E2 of type L1 and
L2 respectively will result in a tuple of type L1 ◦ L2 . We overload here the append
operator written as ◦ using it on the one hand to append terms and on the other
to append types.
   Lemma 5.2. Function Environment Weakening (1)
If ∆, l2 : Lf2 ` P : T and Lf1 ◦ Lf2 = Lf , then ∆, l : Lf ` [l2 7→ πn+1 l]P : T where
n = |Lf1 |.
  Proof. By induction on the relation Lf1 ◦ Lf2 = Lf .
   Lemma 5.3. Function Environment Weakening (2)
If ∆, l : Lf1 ` P : T and Lf1 ◦ Lf2 = Lf , then ∆, l : Lf ` P : T .
  Proof. By induction on the relation Lf1 ◦ Lf2 = Lf .

                                               Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
80     ·     Olivier Savary Belanger et al.

Function Environment Weakening (1) (Lemma 5.2) and (2) (Lemma 5.3) say that
we can replace a variable of a product type by a product type which is larger, i.e. it
has more elements. Lemma 5.2 proves this property when we extend the product
type Lf2 by appending the product type Lf1 to the left, i.e. we compute Lf1 ◦Lf2 . If
Lf1 denotes a product type T1 × (T2 × (. . . (Tn × unit) . . .)), then Lf1 ◦ Lf2 essentially
results in replacing unit with the product type Lf2 . Hence, any occurrence of l2
in the term P must be replaced by πn+1 l in the statement of Lemma 5.2. When
we append Lf2 to Lf1 in the statement of Lemma 5.3 however, we do not need to
renumber the projections in P .
   Theorem 5.1. Type Preservation
If ∆ ` P : T and JP Kl = Q ./ E then · `l E : Lf and ∆, l : Lf ` Q : T for some
Lf .
  Proof. By induction on the typing derivation D0 :: ∆ ` P : T . We only show a
few cases in detail. The other cases are similar.
                D
              x:T ∈∆
Case D0 =                   t cvar
               ∆`x:T

where JxKl = x ./ () .
· `l () : unit                                                                        by env nil
∆, lf : unit ` x : T                                                                   by t cvar
                          D1                               D2
              · ` P1 : code (T × Lx ) S                ∆ ` P2 : Lx
Case D0 =                                                            t cpack
                            ∆ ` hP1 , P2 i : T → S

where JhP1 , P2 iKl = h(fst l) (rst l), Q2 i ./ (lam l. Q1 , E)
and JP1 Kl = Q1 ./ E1 , JP2 Kl = Q2 ./ E2 and E = E1 ◦ E2 .
l : L1 ` Q1 : code (T × Lx ) S and · `l E1 : L1                           by i.h. on D1
∆, l : L2 ` Q2 : Lx and · `l E2 : L2                                      by i.h. on D2
· `l E1 ◦ E2 : L1 ◦ L2 and L1 ◦ L2 = Lf                by Append f. env. (Lemma 5.1)
l : Lf ` Q1 : code (T × Lx ) S                      by F. env. weaken.(1)(Lemma 5.2)
∆, l : Lf ` Q2 : Lx                                 by F. env. weaken.(2)(Lemma 5.3)
· ` lam l. Q1 : code Lf (code (T × Lx ) S)                                    by t clam
· `l (lam l. Q1 , E1 ◦ E2 ) : (code Lf (code (T × Lx ) S)) × Lf            by env cons
l : (code Lf (code (T × Lx ) S)) × Lf ` fst l : code Lf (code (T × Lx ) S) by t cfst
l : (code Lf (code (T × Lx ) S)) × Lf ` rst l : Lf                            by t csnd
l : (code Lf (code (T × Lx ) S)) × Lf ` (fst l) (rst l) : code (T × Lx ) S by t capp
∆, l : (code Lf (code (T × E) S)) × Lf ` h(fst l) (rst l), Q2 i : T → S by t cpack’
                   D1                                    D2
              ∆ ` P1 : S → T          ∆, xf : code (S × l0 ) S, xenv : l0 ` P2 : T
Case D0 =                                                                            t cletpackl0
                               ∆ ` let hxf , xenv i = P1 in P2 : T


Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
      Programming type-safe transformations using higher-order abstract syntax          ·     81

where Jlet hxf , xenv i = P1 in P2 Kl = let hxf , xenv i = Q1 in Q2 ./ E
where JP1 Kl = Q1 ./ E1 , JP2 Kl = Q2 ./ E2 and E = E1 ◦ E2 .
∆, l : L1 ` Q1 : S → T and · `l E1 : L1                                    by i.h. on D1
∆, xf : code (S × l0 ) T, xenv : l0 , l : L1 ` Q2 : T and · `l E2 : L2     by i.h. on D2
· `l E1 ◦ E2 : L1 ◦ L2 and L1 ◦ L2 = Lf                   by Append f. env.(Lemma 5.1)
∆, l : Lf ` Q1 : S → T                                by F. env. weaken.(1)(Lemma 5.2)
∆, xf : code (S × l0 ) T, xenv : l0 , l : Lf ` Q2 : T by F. env. weaken.(2)(Lemma 5.3)
∆, l : Lf , xf : code (S × L) T, xenv : l0 ` Q2 : T                         by exchange
∆, l : Lf ` let hxf , xenv i = Q1 in Q2 : T                                by t cletpack
                        D
                ∆, x : S ` P : T
Case D0 =                              t clam
            ∆ ` lam x. P : code S T

where Jlam x. P Kl = lam x. Q ./ E where JP Kl = Q ./ E .
∆, x : S, l : Lf ` Q : T and · `l E : Lf                                         by i.h. on D
∆, l : Lf , x : S ` Q : T                                                        by exchange
∆, l : Lf ` lam x. Q : code S T                                                     by t clam
                    D1                        D2
             ∆ ` P1 : code S T             ∆ ` P2 : S
Case D0 =                                               t capp
                         ∆ ` P1 P2 : T

where JP1 P2 Kl = Q1 Q2 ./ E
where JP1 Kl = Q1 ./ E1 , JP2 Kl = Q1 ./ E2             and E = E1 ◦ E2 .
∆, l : L1 ` Q1 : code S T and · ` E1 : L1                                       by i.h. on D1
∆, l : L2 ` Q2 : S and · ` E2 : L2                                              by i.h. on D2
· `l E1 ◦ E2 : L1 ◦ L2 and L1 ◦ L2 = Lf                   by Append f. env.(Lemma 5.1)
∆, l : Lf ` Q1 : code S T                           by F. env. weaken. (1) (Lemma 5.2)
∆, l : Lf ` Q2 : S                                  by F. env. weaken. (2) (Lemma 5.3)
∆, l : Lf ` Q1 Q2 : T                                                         by t capp


   While we have so far concentrated on describing hoisting as a separate transfor-
mation on the result of closure conversion, our Beluga implementation of hoisting
is incorporated into closure conversion. Certain cases had to be adapted to this end.
For example, as the closure case hP1 , P2 i corresponds in the implementation to the
translation of a source lambda-abstraction lam x. M , the need to merge function
environments is eliminated due to applying the induction hypothesis to a single
subterm.
5.3   Implementation of Auxiliary Lemmas
   Defining function environments. The function environment represents the collec-
tion of functions hoisted out of a program. Since our context keeps track both of
variables which represent functions bound at the top-level and of those representing

                                             Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
82     ·     Olivier Savary Belanger et al.

local arguments, extra machinery would be required to separate them. For this rea-
son, we represent the function environment as a single term in the target language
rather than multiple terms with individual binders, maintaining as an additional
proposition its form as a tuple of product type.
  As mentioned in our description of the hoisting algorithm, operations such as ◦
are only defined on n-ary tuples and on product types. To guarantee coverage, we
hence define a data-type env which guarantees that a given target term P is a tuple
of type Lf encoding the judgement · `l P : Lf given earlier. To put it differently,
env Lf P guarantees that the tuple P is a well-formed environment of type Lf and
stands for the derivation · `l P : Lf .
     LF env: {Lf :tp} target Lf → type =
     | env_nil: env unit cnil
     | env_cons: {P:target T} env Lf E → env (cross T Lf ) (ccons P E)
     ;

  The constructor env_nil describes an empty tuple of type unit. The constructor
env_consallows us to build a well-formed environment given a target P of type T and
an environment consisting of the tuple E together with its type Lf .
   Appending function environments. When hoisting terms with more than one sub-
term, each recursive call on those subterms results in a different function environ-
ment; they need to be merged before combining the subterms again. In our hoisting
algorithm we rely on the operation ◦ which allows us to append environments to-
gether with several auxiliary lemmas regarding environments.
   To append two environments, we first define in Beluga the function append which
when given two environments Env1 and Env2 returns as a result a new environment
Env3 together with the proof of Append [ ` Env1] [ ` Env2] [ ` Env3]. Knowing the re-
lationship between Env1, Env2 and Env3 is important, since we exploit it later to prove
two weakening lemmas about environments. Our append corresponds to Lemma 5.1
about appending function environments.
     inductive Append: [ ` env L1 E1 ] → [ ` env L2 E2 ] → [ ` env L3 E3 ] → ctype =
     | App_nil : Append [ ` env_nil] [ ` E] [ ` E]
     | App_cons: Append [ ` E1 ] [ ` E2 ] [ ` E3 ]
               → Append [ ` env_cons P E1 ] [ ` E2 ] [ ` env_cons P E3 ]
     ;

     inductive ExAppend: [ ` env L1 E1 ] → [ ` env L2 E2 ] → ctype =
     | ExEnv: Append [ ` Env1 ] [ ` Env2 ] [ ` Env3 ] → ExAppend [ ` Env1 ] [ ` Env2 ]
     ;

     rec append: {Env1 :[ ` env L1 E1 ]}{Env2:[ ` env L2 E2 ]}
                  ExAppend [ ` Env1 ] [ ` Env2 ] =
     λ2 Env1 , Env2 ⇒ case [ ` Env1] of
     | [ ` env_nil] ⇒ ExEnv App_nil
     | [ ` env_cons P Env’1 ] ⇒
       let ExEnv a = append [ ` Env’1 ] [ ` Env2 ] in   ExEnv (App_cons a)
     ;

  Let us look at our implementation more closely. The data-type definition of Append
as an indexed recursive type is straightforward. The constructor App_nil describes
the fact that appending the empty environment to an environment E returns E. The
constructor App_cons states given that appending E1 to E2 returns E3 , we know that
appending (env_cons P E1 ) to E2 returns (env_cons P E3 ).

Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
     Programming type-safe transformations using higher-order abstract syntax          ·     83

   As mentioned earlier, the function append states that given two well-typed envi-
ronments Env1 and Env2 there exists a well-typed environment Env3 together with
the witness that Append [ ` Env1 ] [ ` Env2 ] [ ` Env3 ]. As Beluga does not directly
support existential types, we define a recursive type ExAppend [ ` Env1 ] [ ` Env2 ] to
describe the result.
   The implementation of the function append is then straightforward by recursion
on the first environment Env1 .
   Next, we consider the implementation of the two weakening lemmas for function
environment (Lemma 5.2 and 5.3). The lemmas do in fact not talk about appending
environments, but only about appending their types. Since in our implementation
environments are intrinsically typed, we re-formulate these lemmas slightly. The
first can be read as:
  Let Env1 , Env1 and Env3 be well-typed environments describing · `l E1 : L1 ,
  · `l E2 : L2 , and · `l E3 : L3 respectively. If Append [ ` Env1 ] [ ` Env2 ] [ ` Env3 ]
  and [∆, l:target L2 [] ` target T[]] then [∆, l:target L3 [] ` target T[]]
It is translated directly into the following function:
 rec weakenEnv1:(∆:tctx)
                  {Env1 :[ ` env L1 E1 ]}{Env2:[ ` env L2 E2 ]}{Env3 :[ ` env L3 E3 ]}
                  Append [ ` Env1 ] [ ` Env2 ] [ ` Env3 ] → [∆, l:target L2 [] ` target T[]]
                  → [∆, l:target L3 [] ` target T[]] =
 λ2 Env1 , Env2 , Env3 ⇒ fn a ⇒ fn m ⇒ case prf of
 | App_nil       ⇒ m
 | App_cons a’ ⇒
   let [∆,l: target _ ` P] = weakenEnv1 [ ` _ ] [ ` _ ] [ ` _ ] a’ m in
      [∆,l:target _ ` P[...,(crst l)] ]
 ;

   We made the environment variables Env1 , Env2 , Env3 explicit, since the property we
state crucially depends on the type of the environments. The function weakenEnv1 is
implemented by recursion over the proof that Append [ ` Env1 ] [ ` Env2 ] [ ` Env3 ].
We could have also implemented this function recursively over Env1 . There are only
two cases. If Env1 describes the empty environment and a stands for App_nil, then
we know that L2 and L3 are the same and hence we simply return target term m
given as input. If Env1 is a well-typed non-empty tuple and a stands for App_cons
a’, we recursively translate a’ leaving it up to type reconstruction to fill in the
concrete instantiations for the corresponding environments. As a result, we obtain
[∆, l:target L[] ` M’]. We need to however return a target term in the context
∆, l:target (cross T[] L[]). We therefore replace l in M’ with (crst l). We again
exploit the built-in substitution for LF objects in Beluga to model it.
   The second weakening lemma states that we can weaken the type standing for
an environment by adding additional elements to the right. More precisely it says:
  For all well-typed environments Env1 describing · `l E1 : L1 , Env2 describing
  · `l E2 : L2 , and and Env3 describing · `l E3 : L3 ,
  if Append [ ` Env1 ] [ ` Env2 ] [ ` Env3 ] and [∆, l:target L1 [] ` target T[]]
  then [∆, l:target L3 [] ` target T[]]
  To prove this lemma, we in fact rely on another simple lemma which states that
appending an environment Env to an empty environment returns the environment
Env.

                                            Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
84     ·     Olivier Savary Belanger et al.

 rec append_nil: Append [ ` Env1 ] [ ` env_nil] [ ` Env3 ] → [ ` eq Env1 Env3 ] =
 fn a ⇒ case a of
 | App_nil       ⇒ [ ` refl]
 | App_cons a’ ⇒
   let [ ` refl] = append_nil a’ in        [ ` refl]
 ;

 rec weakenEnv2:(∆:tctx)
                  {Env1 :[ ` env L1 E1 ]}{Env2 :[ ` env L2 E2 ]}{Env3 :[ ` env L3 E3 ]}
                  Append [ ` Env1 ] [ ` Env2 ] [ ` Env3 ] →
                  [∆, l:target L1 [] ` target T[]] → [∆, l:target L3 [] ` target T[]] =
 λ2 Env1 , Env2 , Env3 ⇒ fn a ⇒ fn n ⇒ case a of
 | App_nil ⇒
   let ExEnv a = append [ ` Env3 ] [ ` env_nil] in
   let [ ` refl] = append_nil a in weakenEnv1 [ ` _ ] [ ` _ ] [ ` _ ] a n
 | App_cons p ⇒
   let [∆,l:target (cross S[] L01 []) ` N] = n in
   let [∆,x:target S[], l:target L03 [] ` N’] =
      weakenEnv2 [ ` _ ] [ ` _ ][ ` _ ] p [Γ,x:target S[],l:target L01 [] ` N[..., ccons x l]]
   in [∆,l:target (cross S[] L03 []) ` N’[..., cfst l, crst l]]
 ;

   While the implementation of weakEnv1 is directly using the definition of Append, the
function weakEnv2, which corresponds to proof of Lemma 5.3 is a bit more involved.
The reason is that Append is defined recursively on the first environment. When we
recursively analyze a: Append [ ` Env1 ] [ ` Env2 ] [ ` Env3 ] we learn in the base case
that Env1 is the empty environment. Therefore, its type is unit and we need to build
a target term in the context ∆, l:target L3 [] given a target term in the context
∆, l:target unit. We also know that Env2 and Env3 are the same. We first show that
there exists an environment Env’ s.t. Append [ ` Env3 ] [ ` env_nil] [ ` Env’]. Then
we show that Env’ is uniquely determined, i.e. it is in fact Env3 . Finally, we use
weakenEnv1 (Lemma 5.2), to show that given Append [ ` Env3 ] [ ` env_nil] [ ` Env3 ]
and a target term in the context ∆, l:target unit there exists a target term in the
context ∆, l:target L3 [].
   In the recursive case, the environment Env1 stands for a tuple (env_cons P Env01 ) of
type (cross S L01 ) and Env3 stands for a tuple (env_cons P Env03 ) of type (cross S L03 ).
Hence, we need to construct a target term in the context ∆,l:target (cross S[] L03 [])
given a target term n in the context ∆,l:target (cross S[] L01 []). By the assump-
tion, we know that a:Append [ ` Env01 ] [ ` Env2 ] [ ` Env03 ] and we want to recursively
weaken n which stands for [∆,l:target (cross S[] L01 []) ` N]. The problem however
is that Env01 is an environment tuple of type L01 [], not (cross S[] L01 []).
   We therefore employ a clever trick: we replace any occurrence of l in N where
l stood for an environment of type (cross S[] L01 []) with ccons x l in the context
∆,x:target S[],l:target L01 [] and then recursively weaken the term N[..., ccons x l].
As a result we obtain a term N’ in the context ∆, x:target S[], l:target L03 []. Note
that the type of the function guarantees the shape of the context. We now must
translate the term N’ back to the context ∆, l:target (cross S[] L03 []). Again we
rely on substitution and replace any occurrence of x with the first projection and
any occurrence of l with the second projection. As is apparent being able to silently
substitute for variables in a term plays a crucial role in our implementation and we
benefit substantially from the built-in support provided by Beluga.



Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
       Programming type-safe transformations using higher-order abstract syntax          ·     85


inductive Result:{∆:tctx} [ ` tp] → ctype =
| Result : [∆,l:target Lf [] ` target T[]] → [ ` env Lf E]
         → Result [∆] [ ` T]
;

rec hcc: [Γ ` source T[]] → Map [∆] [Γ] → Result [∆] [ ` T] =
fn m ⇒ fn ρ ⇒ case m of
| [Γ ` #p] ⇒
  let [∆ ` Q] = lookup ρ [Γ ` #p] in
     Result [∆, l:target unit ` Q [...]] [ ` env_nil]

| [Γ ` app M N] ⇒
  let Result r1 [ ` Env1 ] = hcc [Γ ` M] ρ in
  let Result r2 [ ` Env2 ] = hcc [Γ ` N] ρ in
  let ExEnv (a : Append [ ` _ ] [ ` _ ] [ ` Env3 ]) = append      [ ` Env1 ] [ ` Env2 ] in
  let [∆, l:target L[] ` P] = weakenEnv2 [ ` _ ] [ ` _ ] [ `      _ ] a r1 in
  let [∆, l:target L[] ` Q] = weakenEnv1 [ ` _ ] [ ` _ ] [ `      _ ] a r2 in
   Result [∆,l:target L[] ` cletpack P λe.λxf .λxenv .capp        xf (ccons Q[...,l] xenv )]
           [ ` Env3 ]

| [Γ ` lam λx.M] ⇒
  let STm [Γ0 ,x:source S[] ` M’] wk = strengthen [Γ, x:source _ ` M] in
  let EnvClo env ρ0                      = reify [Γ0 ] in
  let Result r1 [ ` Env1 ]                = hcc [Γ0 ,x:source _ ` M’] (extend ρ0 ) in
  let [∆ ` Penv ]                           = lookupVars wk env ρ in
  let [xenv :target LΓ0 [],x:target T[],l:target L[] ` P] = r1 in
     Result [∆,l:target (cross (code L[] (code (cross T[] LΓ0 []) _ )) L[])
                                   ` cpack (capp (cfst l) (crst l)) Penv [...]]
             [ ` env_cons (clam λl.
                              clam (λc.clet (cfst c) λx.clet (crst c)
                                                               λxenv .P[xenv , x, l]))
                            Env1 ]

...
;

rec hoist_cc: [ ` source T] → [ ` target T] =
fn m ⇒
 let Result [l:target _ ` M] (e : [ ` env _ E]) = hcc m        (M_id []) in
      [ ` clet E (λl. M)]
;


            Fig. 15.   Implementation of Closure Conversion and Hoisting in Beluga

5.4    Implementation of the Main Theorem
We now generalize the closure conversion function such that it not only closure
converts a source term but also hoists all converted and closed code to the top
level. The top-level function hoist_cc performs hoisting at the same time as closure
conversion on closed terms. It relies on the generalized function hcc (see Fig. 15)
for the main work. It takes in a map between the source context Γ and target
context ∆ in addition to a source term of type T in context Γ. Compared to our
previous implementation of type-preserving closure conversion, only small changes
are necessary to integrate hoisting. The first obvious change is that we return
not only the closure converted term, [∆, l:target Lf [] ` target T[]], but also the
corresponding function environment, [ ` env Lf E]. This result is encapsulated in a
compile time data-type of type Result [∆] [ ` T]. How we build the closure con-
verted term remains essentially unchanged. The main change is apparent in the

                                              Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
86     ·     Olivier Savary Belanger et al.

case for application app M N. Here, we first translate M obtaining the closure con-
verted term r1 together with an environment Env1 . Similarly, translating N returns
the closure converted term r2 together with an environment Env2 . We now append
the environments Env1 and Env2 obtaining a joint environment Env3 . Finally, we
weaken both, the closure converted terms r1 and r2 , to be meaningful with respect
to the environment Env3 and build our final closure converted term.
  The top-level function hoist_cc calls hcc with the initial map and the source term
m of type T, producing a Result [ ] [ ` T] pairing a function environment and a
target term depending solely on a function environment variable l. It then binds,
with clet, the function environment as l in the hoisted term, resulting in a closed
target term of the same type.
5.5   Discussion
Our implementation of hoisting adds in the order of 100 lines to the development
of closure conversion (for a total of approximately 300 lines of code) and retains its
main structure.
   An alternative to the presented algorithm would be to thread through the func-
tion environment as an additional argument to hcc. This avoids the need to append
function environments and obviates the need for certain auxiliary functions such as
weakenEnv1. Other properties around Append would however have to be proven, some
of which require multiple nested inductions; therefore, the complexity and length
of the resulting implementation is similar.
   As in our work, hoisting in Chlipala [2008] is performed at the same time as
closure conversion, as a consequence of the target language not capturing that
functions are closed.
   In Guillemette and Monnier [2008], the authors include hoisting as part of their
transformation pipeline, after closure conversion. Since the language targeted by
their closure conversion syntactically enforces that functions are closed, it would
have been possible for them to perform hoisting in a separate phase. In Beluga,
we could perform partial hoisting on the target language of closure conversion,
only lifting provably closed functions to the top level. To do so, we would use two
patterns for the closure case, [Γ ` cpack M[] N] where the function part, M, is closed
and can thus be hoisted out, and [Γ ` cpack M N], where M may still depend on the
context Γ, and as such cannot be hoisted out.

6.    RELATED WORK
While HOAS holds the promise of dramatically reducing the overhead related to
manipulating abstract syntax trees with binders, the implementation of a certified
compiler, in particular the phases of closure conversion and hoisting, using HOAS
has been elusive.
  One of the earliest studies of using HOAS in implementing compilers was pre-
sented in Hannan [1995], where the author describes the implementation of a type-
directed closure conversion in Elf [Pfenning, 1989], leaving open several implemen-
tation details, such as how to reason about variable equality.
  In more recent work, the closure conversion algorithm together with separate
typing rules has been specified in Abella [Gacek, 2008], an interactive theorem
prover which supports HOAS specifications, but not dependent types at the spec-
Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
      Programming type-safe transformations using higher-order abstract syntax         ·     87

ification level. Specifying the closure conversion algorithm using HOAS requires
extra book-keeping infrastructure for tracking variables, computing the free vari-
ables in a term, and describing the mapping ρ. Moreover, when we reason about
the algorithm and prove that types are preserved, we need to establish invariants
about variable contexts separately, since first-class support for contexts is missing.
While this demonstrates, implementing and reasoning about closure conversion us-
ing HOAS is feasible, our development is unique as we develop the algorithm and
proof at the same time. In fact, our algorithm itself is the proof.
   A number of typed transformations to CPS [Harper and Lillibridge, 1993; Barthe
et al., 1999, 2001] have been implemented in such a way as to obtain type safety
as a direct consequence of type checking the implementation in the host language’s
type system. This is the case of Chen and Xi [2003], who show an implementation
statically guaranteed to be type safe of the CPS transform, using GADTs and over
a decidedly first-order representation of terms using de Bruijn indices. Guillemette
and Monnier [2006]; Chlipala [2008] achieve similar results in Haskell and Coq
respectively, with term representations based on HOAS.
   The closure conversion algorithm has also served as a key benchmark for sys-
tems supporting first-class nominal abstraction such as FreshML [Pottier, 2007]
and αProlog [Cheney and Urban, 2004]. Both languages provide facilities for gen-
erating names and reasoning about their freshness, which proves very useful when
computing the free variables in a term. However, capture-avoiding substitution still
needs to be implemented separately. Since these languages lack dependent types,
implementing a certified compiler is out of their reach.
6.1   Design Options
Beluga’s provision of dependent types along with datatypes both at the compu-
tation level and the LF level gives a lot of flexibility in terms of implementation
choices. Throughout the development, design choices have been made for the pur-
pose of simplifying the implementation while still obtaining a realistic compilation
pipeline.
   All our object languages are encoded in LF. Alternatively, we could have encoded
them as indexed datatypes. This would have allowed us, among other things, to
syntactically enforce that the function part of closures is closed. It would how-
ever have made it necessary to manually implement capture-avoiding substitution
functions for each language. Moreover, as indexed datatypes may not be indexed
with other indexed datatypes, closure conversion and hoisting would have required
additional facilities and functions to work around this limitation, for example by
duplicating the encoding of terms at the LF level. Another alternative would be
to construct a datatype indexed by LF terms, effectively duplicating the encod-
ing, witnessing the closedness of the function part of closures. This could be used
to characterize the output of closure conversion, in which case hoisting could be
performed separately.
   The CPS algorithm could have been encoded as an indexed datatype relating
the source and target languages. This would have made it possible to prove full
semantics preservation of the algorithm in Beluga. However, doing so, we would
not obtain an executable code transformation. Closure conversion would have been
difficult to encode as an indexed datatype as it depends on pattern matching, which
                                            Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
88     ·     Olivier Savary Belanger et al.

is only available within Beluga functions, to maximally strengthen the variable
environment (see Fig. 12). A naive closure conversion algorithm can be encoded
in LF, using explicit tags to track variables, after which other properties such as
semantics preservation could be proven in Beluga.
   With the transformations encoded as Beluga functions, we have the option of
relating contexts of the source and target languages using a joint context, as we did
for CPS, or using a context relation, as we did for closure conversion and hoisting.
Differences between these two approaches are discussed thoroughly in Felty and
Pientka [2010] and Felty et al. [2015]. We could have used a context relation for
CPS with no changes to the length or complexity of the code. It would have been
complicated to use a joint context for closure conversion, as many source variables
are represented by the same target variable, namely the environment, in the target
context.

7.   CONCLUSION
Using a representation based on HOAS, we have implemented not only a translation
to continuation-passing style but also a closure conversion and hoisting, where those
implementations also constitute a proof of their type-preservation.
   Although HOAS is one of the most sophisticated encoding techniques for struc-
tures with binders and offers significant benefits, problems such as closure con-
version, where reasoning about the identity of free variables is needed, have been
difficult to implement using an HOAS encoding. In Beluga, contexts are first-
class; we can manipulate them, and indeed recover the identity of free variables
by observing the context of the term. This is unlike other systems supporting
HOAS such as Twelf [Pfenning and Schürmann, 1999] or Delphin [Poswolsky and
Schürmann, 2008]; in Abella [Gacek, 2008], we can test variables for identity, but
users need to represent and reason about contexts explicitly. More importantly,
we cannot develop the program and proof hand-in-hand. In our development, the
actual program is the proof.
   In addition, Beluga’s computation-level recursive datatypes provide us with
an elegant tool to encode properties about contexts and contextual object. Our
case study clearly demonstrates the elegance of developing certified programs in
Beluga. We rely on built-in substitutions to replace bound variables with their
corresponding projections in the environment; we rely on the first-class context and
recursive datatypes to define a mapping of source and target variables as well as
computing a strengthened context only containing the relevant free variables in a
given term.
   Developing this case study has already lead to a number of improvements for
programmers wanting to use Beluga for certified programming. In particular, the
support to write programs with holes and printing the typing information of the
hole has been tremendously beneficial in practice. Support for automatic splitting
on variables is also useful. This case study also has highlighted other areas: for
example, support for variable substitutions in addition to substitution variables
[Cave and Pientka, 2013], would allow us to express and guarantee that these sub-
stitutions only map variables to variables and do not change the size of the overal
term. This seems an elegant way of justifying why recursing on the strengthened
term during closure conversion will terminate.
Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
     Programming type-safe transformations using higher-order abstract syntax         ·     89

   In the future, we plan to extend our compiler to System F. While the algorithms
seldom change from STLC to System F, open types pose a significant challenge.
This will provide further insights into what tools and abstractions are needed to
make certified programming accessible to the every day programmer.
   Acknowledgements.. We thank Mathieu Boespflug for his feedback and work on
the implementation of Beluga. An abridged version of this paper appeared in the
proceeding of the International Conference on Certified Programs and Proofs in De-
cember 2013 under the name “Programming type-safe transformations using higher-
order abstract syntax” [Savary B. et al., 2013]. We also thank all the reviewers for
this article for their careful reading and detailed feedback which helped improve the
paper. This research was supported through the Natural Sciences and Engineer-
ing Research Council of Canada (NSERC-298311, NSERC-206263 and NSERC-
RGPAS 234341), the Ministère du Dèveloppement économique, de l’Innovation et
de l’Exportation du Quebec (MDEIE PSR-SIIRI-734), and a graduate scholarship
from the Fonds de recherche Nature et Technologies Quebec.

8.   BIBLIOGRAPHY
G. Barthe, J. Hatcliff, and M. H. Sørensen. CPS Translations and Applications:
  The Cube and Beyond. Higher-Order and Symbolic Computation, 12(2):125–170,
  1999.
G. Barthe, J. Hatcliff, and M. H. Sørensen. Weak Normalization Implies Strong
  Normalization in a Class of Non-Dependent Pure Type Systems. Theor. Comput.
  Sci., 269(1-2):317–361, 2001.
N. Benton, A. Kennedy, and G. Russell. Compiling Standard ML to Java Bytecodes.
  In International Conference on Functional Programming, ICFP’98, pages 129–
  140. ACM, 1998.
POPL Tutorial: Mechanizing Meta-Theory with LF and Twelf. Carnegie Mellon
  University, 2009. URL http://twelf.org/wiki/POPL_Tutorial.
A. Cave and B. Pientka. Programming with Binders and Indexed Data-Types. In
  Symposium on Principles of Programming Languages, POPL’12, pages 413–424.
  ACM, 2012.
A. Cave and B. Pientka. First-Class Substitutions in Contextual Type Theory.
  In International Workshop on Logical Frameworks and Meta-Languages: Theory
  and Practice, LFMTP’13, pages 15–24. ACM, 2013.
C. Chen and H. Xi. Implementing Typeful Program Transformations. In Workshop
  on Partial Evaluation and Semantics-based Program Manipulation, pages 20–28,
  ACM, 2003.
J. Cheney and C. Urban. Alpha-Prolog: A Logic Programming Language with
  Names, Binding and Alpha-Equivalence. In International Conference on Logic
  Programming, ICLP’04, pages 269–283, 2004.
A. J. Chlipala. Parametric Higher-Order Abstract Syntax for Mechanized Seman-
  tics. In International Conference on Functional Programming, pages 143–156.
  ACM, 2008.
O. Danvy and A. Filinski. Representing Control: A Study of the CPS Transforma-
  tion. Mathematical Structures in Computer Science, 2(4):361–391, 1992.
                                           Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
90     ·     Olivier Savary Belanger et al.

J. Dunfield and B. Pientka. Case Analysis of Higher-Order Data. In International
   Workshop on Logical Frameworks and Meta-Languages: Theory and Practice,
   LFMTP’08, Electronic Notes in Theoretical Computer Science (ENTCS), pages
   69–84. Elsevier, 2009.
A. P. Felty and B. Pientka. Reasoning with Higher-Order Abstract Syntax and
   Contexts: A Comparison. In International Conference on Interactive Theorem
   Proving, ITP’10, pages 227–242. Springer, 2010.
A. P. Felty, A. Momigliano, and B. Pientka. The Next 700 Challenge Problems
   for Reasoning with Higher-Order Abstract Syntax Representations: Part 2 - a
   Survey. Journal of Automated Reasoning, 55(4):307–372, 2015.
F. Ferreira and B. Pientka. Bidirectional Elaboration of Dependently Typed Lan-
   guages. In International Symposium on Principles and Practice of Declarative
   Programming, PPDP’14, pages 161–174. ACM, 2014.
A. Gacek. The Abella Interactive Theorem Prover (System Description). In In-
   ternational Joint Conference on Automated Reasoning, pages 154–161. Springer,
   2008.
L.-J. Guillemette and S. Monnier. Statically Verified Type-preserving Code Trans-
   formations in Haskell. In Programming Languages meets Program Verification,
   PLPV’06, Electronic Notes in Theoretical Computer Science (ENTCS), pages
   23–39. Elsevier, 2006.
L.-J. Guillemette and S. Monnier. A Type-Preserving Closure Conversion in
   Haskell. In Workshop on Haskell, pages 83–92. ACM, 2007.
L.-J. Guillemette and S. Monnier. A Type-Preserving Compiler in Haskell. In
   International Conference on Functional Programming, ICFP’08, pages 75–86.
   ACM, 2008.
J. Hannan. Type Systems for Closure Conversions. In Workshop on Types for
   Program Analysis, pages 48–62, 1995.
R. Harper and D. R. Licata. Mechanizing Metatheory in a Logical Framework.
   Journal of Functional Programming, 17(4-5):613–673, 2007.
R. Harper and M. Lillibridge. Explicit Polymorphism and CPS Conversion. In
   Symposium on Principles of programming Languages, POPL ’93, pages 206–219,
   ACM, 1993.
R. Harper, F. Honsell, and G. Plotkin. A Framework for Defining Logics. Journal
   of the ACM, 40(1):143–184, January 1993.
A. Nanevski, F. Pfenning, and B. Pientka. Contextual Modal Type Theory. Trans-
   actions on Computational Logic, 9(3):1–49, 2008.
F. Pfenning. Elf: A Language for Logic Definition and Verified Meta-Programming.
   In Symposium on Logic in Computer Science, LICS’89, pages 313–322. IEEE,
   1989.
F. Pfenning and C. Schürmann. System description: Twelf — a Meta-Logical
   Framework for Deductive Systems. In International Conference on Automated
   Deduction, CADE’99, pages 202–206. Springer, 1999.
B. Pientka. A Type-theoretic Foundation for Programming with Higher-Order
   Abstract Syntax and First-Class Substitutions. In Symposium on Principles of
   Programming Languages, POPL’08, pages 371–382. ACM, 2008.
Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
     Programming type-safe transformations using higher-order abstract syntax         ·     91

B. Pientka. An Insider’s Look at LF Type Reconstruction: Everything You (N)ever
  Wanted to Know. Journal of Functional Programming, 1(1–37), 2013.
B. Pientka and A. Abel. Structural Recursion over Contextual Objects. In 13th
  International Conference on Typed Lambda Calculi and Applications, TLCA’15,
  pages 273–287. LIPIcs-Leibniz International Proceedings in Informatics, 2015.
B. Pientka and A. Cave. Inductive Beluga: Programming Proofs (System Descrip-
  tion). In 25th International Conference on Automated Deduction, CADE-25,
  pages 272–281. Springer, 2015.
B. Pientka and J. Dunfield. Beluga: A Framework for Programming and Reasoning
  with Deductive Systems (System Description). In International Joint Conference
  on Automated Reasoning, IJCAR’10, pages 15–21. Springer, 2010.
A. B. Poswolsky and C. Schürmann. Practical Programming with Higher-Order
  Encodings and Dependent Types. In European Symposium on Programming,
  ESOP’08, pages 93–107. Springer, 2008.
F. Pottier. Static Name Control for FreshML. In Symposium on Logic in Computer
  Science, LICS’07, pages 356–365. IEEE, 2007.
O. Savary B., S. Monnier, and B. Pientka. Programming Type-Safe Transformations
  using Higher-order Abstract Syntax. In Certified Programs and Proofs, CPP’13.
  Springer, 2013.
Z. Shao and A. W. Appel. A Type-Based Compiler for Standard ML. In Conference
  on Programming Language Design and Implementation, PLDI’95, pages 116–129,
  1995. ACM.
Z. Shao, C. League, and S. Monnier. Implementing Typed Intermediate Languages.
  In International Conference on Functional Programming, ICFP’98, pages 313–
  323. ACM, 1998.
D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P. Lee. TIL: A Type-
  Directed Optimizing Compiler for ML. In Conference on Programming Languages
  Design and Implementation, PLDI’96, pages 181–192, ACM, 1996.
R. Virga. Higher-Order Rewriting with Dependent Types. PhD thesis, Department
  of Mathematical Sciences, Carnegie Mellon University, 1999. CMU-CS-99-167.




                                           Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
