System FR as Foundations for Stainless

TL;DR

This paper introduces System FR, a formal foundation and verifier for higher-order functional programs with generics and recursive types, ensuring safety and termination through formal proofs and practical implementation.

Contribution

It formalizes System FR, a calculus supporting polymorphism, dependent types, and recursion, and implements a verifier integrated with Stainless for verifying complex Scala programs.

Findings

Verified 14,000 lines of Scala code including algorithms and data structures.

Proved soundness and safety of the verifier using Coq.

Demonstrated efficiency on real-world functional programs.

Abstract

We present the design, implementation, and foundation of a verifier for higher-order functional programs with generics and recursive data types. Our system supports proving safety and termination using preconditions, postconditions and assertions. It supports writing proof hints using assertions and recursive calls. To formalize the soundness of the system we introduce System FR, a calculus supporting System F polymorphism, dependent refinement types, and recursive types (including recursion through contravariant positions of function types). Through the use of sized types, System FR supports reasoning about termination of lazy data structures such as streams. We formalize a reducibility argument using the Coq proof assistant and prove the soundness of a type-checker with respect to call-by-value semantics, ensuring type safety and normalization for typeable programs. Our program verifier is implemented as an alternative verification-condition generator for the Stainless tool, which relies on existing SMT-based solver backend for automation. We demonstrate the efficiency of our approach by verifying a collection of higher-order functional programs comprising around 14000 lines of polymorphic higher-order Scala code, including graph search algorithms, basic number theory, monad laws, functional data structures, and assignments from popular Functional Programming MOOCs.

Equations

$$\displaystyle t\Coloneqq\$$

$$\displaystyle{\tt left}({t})\ |\ {\tt right}({t})\ |\ {\tt either\_match}({t},{x\Rightarrow t},{x\Rightarrow t})\hskip 10.00002pt|\hskip 10.00002pt{\tt true}\ |\ {\tt false}\ |\ {\tt if}\ {t}\ {\tt then}\ {t}\ {\tt else}\ {t}\ |\$$

$$\mathtt{zero}|\mathtt{succ}(t)|\mathtt{rec}(t,t,(n,y)\Rightarrow t)|\mathtt{fix}(y\Rightarrow t)|\mathtt{match}(t,t,n\Rightarrow t)$$

$$\mathtt{fold}(t)|\mathtt{unfold}t\mathtt{in}x\Rightarrow t|\Lambda t|t[]|\mathtt{err}|\mathtt{let}x=t\mathtt{in}t|\mathtt{size}(t)$$

$$\begin{array}[]{rcl@{\hspace*{1cm}}rcl}{\tt size\_sem}({{\tt succ}({v})})&=&1+{\tt size\_sem}({v})\hfil\hskip 28.45274pt&{\tt size\_sem}({{\tt fold}({v})})&=&1+{\tt size\_sem}({v})\\ {\tt size\_sem}({{\tt right}({v})})&=&1+{\tt size\_sem}({v})\hfil\hskip 28.45274pt&{\tt size\_sem}({{\tt left}({v})})&=&1+{\tt size\_sem}({v})\\ {\tt size\_sem}({(v_{1},v_{2})})&=&{\tt size\_sem}({v_{1}})+{\tt size\_sem}({v_{2}})\hfil\hskip 28.45274pt&\lx@intercol\hfil{\tt size\_sem}({v})=0,\mbox{\it in all other cases}\hfil\lx@intercol\\ \end{array}$$

$$\mathcal{H}|\mathcal{E}e|v\mathcal{E}|(\mathcal{E},e)|(v,\mathcal{E})|{\pi }_1\mathcal{E}|{\pi }_2\mathcal{E}|\mathtt{succ}(\mathcal{E})|$$

$$\mathtt{rec}(\mathcal{E},\_,\_)|\mathtt{match}(\mathcal{E},\_,\_)|\mathtt{if}\mathcal{E}\mathtt{then}t\mathtt{else}t|\mathtt{let}x=\mathcal{E}\mathtt{in}t|\mathtt{size}(\mathcal{E})|$$

$$\mathtt{fold}(\mathcal{E})|\mathtt{unfold}\mathcal{E}\mathtt{in}\_|\mathcal{E}[]|\mathtt{left}(\mathcal{E})|\mathtt{right}(\mathcal{E})|either\_match(\mathcal{E},\_,\_)$$

$$\displaystyle\tau\Coloneqq\$$

$$\mathtt{Rec}(n)(\alpha \Rightarrow \tau )|\{x:\tau |t\}|t\equiv t$$

$$\mathtt{Rec}(\alpha \Rightarrow \tau )\triangleq \forall n:\mathsf{Nat}.\mathtt{Rec}(n)(\alpha \Rightarrow \tau )$$

$$[[\alpha {]]}_{\text{v}}^{\theta }\triangleq \theta (\alpha )$$

$$[[\top {]]}_{\text{v}}^{\theta }\triangleq \mathsf{Val}$$

$$[[\mathsf{Unit}{]]}_{\text{v}}^{\theta }\triangleq \{()\}$$

$$[[\mathsf{Bool}{]]}_{\text{v}}^{\theta }\triangleq \{\mathtt{true},\mathtt{false}\}$$

$$[[\mathsf{Nat}{]]}_{\text{v}}^{\theta }\triangleq \{\mathtt{zero},\mathtt{succ}(\mathtt{zero}),\mathtt{succ}(\mathtt{succ}(\mathtt{zero})),\dots \}$$

$$[[\Pi x:{\tau }_1.{\tau }_2{]]}_{\text{v}}^{\theta }\triangleq \{f\in \mathsf{Val}|\forall a\in [[{\tau }_1{]]}_{\text{v}}^{\theta }.fa\in [[{\tau }_2[x\mapsto a]{]]}_{\text{t}}^{\theta }\}$$

$$[[\forall x:{\tau }_1.{\tau }_2{]]}_{\text{v}}^{\theta }\triangleq \{b\in \mathsf{Val}|\forall a\in [[{\tau }_1{]]}_{\text{v}}^{\theta }.b\in [[{\tau }_2[x\mapsto a]{]]}_{\text{v}}^{\theta }\}$$

$$[[\Sigma x:{\tau }_1.{\tau }_2{]]}_{\text{v}}^{\theta }\triangleq \{(a,b)|a\in [[{\tau }_1{]]}_{\text{v}}^{\theta }\wedge b\in [[{\tau }_2[x\mapsto a]{]]}_{\text{v}}^{\theta }\}$$

$$[[\{x:\tau |b\}{]]}_{\text{v}}^{\theta }\triangleq \{a\in [[\tau {]]}_{\text{v}}^{\theta }|b[x\mapsto a]{\hookrightarrow }^{\ast }\mathtt{true}\}$$

$$[[{\tau }_1+{\tau }_2{]]}_{\text{v}}^{\theta }\triangleq \{\mathtt{left}(v)|v\in [[{\tau }_1{]]}_{\text{v}}^{\theta }\}\cup \{\mathtt{right}(v)|v\in [[{\tau }_2{]]}_{\text{v}}^{\theta }\}$$

$$[[t_1\equiv t_2{]]}_{\text{v}}^{\theta }\triangleq \{()\}\text{ if t1≈t2, and ∅ otherwise, where}$$

$$\displaystyle\qquad\qquad\qquad({t_{1}}\approx{t_{2}})\triangleq\big{(}\forall v\in{\sf Val}.\ (t_{1}\hookrightarrow^{*}v\mit{~{}iff~{}}t_{2}\hookrightarrow^{*}v)\big{)}$$

$$[[\forall \alpha :\mathtt{Type}.\tau {]]}_{\text{v}}^{\theta }\triangleq \{v\in \mathsf{Val}|\forall \mathsf{C}\in \mathsf{Candidates}.v[]\in [[\tau {]]}_{\text{t}}^{\theta [\alpha \mapsto \mathsf{C}]}\}$$

$$\displaystyle\llbracket{\tt Rec}({t})({\alpha}\Rightarrow{\tau})\rrbracket_{\textsf{v}}^{\theta}\triangleq\big{\{}{\tt fold}({v})\ \big{|}\ (t\hookrightarrow^{*}{\tt zero}\land v\in\llbracket{\sf basetype}_{\alpha}({\tau})\rrbracket_{\textsf{v}}^{\theta})\ \lor$$

$$\displaystyle\qquad\qquad\qquad\qquad\qquad\qquad\quad\exists n\in\llbracket{\sf Nat}\rrbracket_{\textsf{v}}.\ t\hookrightarrow^{*}{\tt succ}({n})\land v\in\llbracket\tau\rrbracket_{\textsf{v}}^{{\theta}[{\alpha}~{}\mapsto~{}{\llbracket{\tt Rec}({n})({\alpha}\Rightarrow{\tau})\rrbracket_{\textsf{v}}^{\theta}}]}\ \big{\}}$$

$$[[\tau {]]}_{\text{t}}^{\theta }\triangleq \{t|\exists v\in [[\tau {]]}_{\text{v}}^{\theta }.t{\hookrightarrow }^{\ast }v\}$$

$${\mathsf{basetype}}_{\alpha }(\Sigma x:{\tau }_1.{\tau }_2)\triangleq \Sigma x:{\mathsf{basetype}}_{\alpha }({\tau }_1).{\mathsf{basetype}}_{\alpha }({\tau }_2)$$

$${\mathsf{basetype}}_{\alpha }({\tau }_1+{\tau }_2)\triangleq {\mathsf{basetype}}_{\alpha }({\tau }_1)+{\mathsf{basetype}}_{\alpha }({\tau }_2)$$

$${\mathsf{basetype}}_{\alpha }(\tau )\triangleq \text{ if α∈fv(τ)}\text{ then }\top \text{ else }\tau$$

$$[[{\tau }_1{]]}_{\text{v}}^{\theta [\alpha \mapsto [[{\tau }_2{]]}_{\text{v}}^{\theta }]}=[[{\tau }_1[\alpha \mapsto {\tau }_2]{]]}_{\text{v}}^{\theta }$$

$$\forall \theta ,\gamma \in [[\Theta ;\Gamma {]]}_{\text{v}}.\gamma (t)\in [[\gamma (\tau ){]]}_{\text{t}}^{\theta }$$

$$\mathtt{List}[\mathtt{X}]\triangleq \forall n:\mathsf{Nat}.{\mathtt{List}}_n[\mathtt{X}].$$

$$t$$

$$\mathtt{left}[\tau +\tau ](t)|\mathtt{right}[\tau +\tau ](t)|either\_match(t,x\Rightarrow t,x\Rightarrow t)|$$

$$\displaystyle{\tt true}\ |\ {\tt false}\ |\ {\tt if}\ {t}\ {\tt then}\ {t}\ {\tt else}\ {t}\ |\$$

$$\displaystyle{\tt zero}\ |\ {\tt succ}({t})\ |\ {\tt rec}[{x\Rightarrow\tau}]({t},{t},{(n,y)\Rightarrow t})\ |\ {\tt fix}[{n\Rightarrow\tau}]({(n,y)\Rightarrow t})\ |\ {\tt match}({t},{t},{n\Rightarrow t})\ |\$$

$$\displaystyle{\tt fold}[\tau]({t})\ |\ {\tt unfold}\ {t}\ {\tt in}\ {x\Rightarrow t}\ |\ {\tt unfold\_pos}\ {t}\ {\tt in}\ {x\Rightarrow t}\ |\$$

$$\Lambda \alpha .t|t[\tau ]|\mathtt{err}[\tau ]|\mathtt{refl}[t,t]|\mathtt{let}x=t\mathtt{in}t|\mathtt{size}(t)$$

$$\forall m:\{m:\mathsf{Nat}|m<n\}.\mathsf{Unit}\to \Pi x:\{x:\{x:{\tau }_1|pre\}|measure\le m\}.\{res:{\tau }_2|post\}$$

$$\forall n:\mathsf{Nat}.\Pi x:\{x:\{x:{\tau }_1|pre\}|m\le n\}.\{res:{\tau }_2|post\}$$

$$\begin{array}[]{l@{}c@{}c@{}c@{}rcl}{{\tt unify}(E,}&{\sf Unit}&,&{\sf Unit}&)&\triangleq&{\sf Unit}\\ {{\tt unify}(E,}&{\sf Bool}&,&{\sf Bool}&)&\triangleq&{\sf Bool}\\ {{\tt unify}(E,}&{\sf Nat}&,&{\sf Nat}&)&\triangleq&{\sf Nat}\\ {{\tt unify}(E,}&\top&,&\top&)&\triangleq&\top\\ {{\tt unify}(E,}&\alpha&,&\alpha&)&\triangleq&\alpha\\ {{\tt unify}(E,}&\Pi{x}:{A_{1}}.\ {B_{1}}&,&\Pi{x}:{A_{2}}.\ {B_{2}}&)&\triangleq&\Pi{x}:{{\tt unify}(E,A_{1},A_{2})}.\ {{\tt unify}(E,B_{1},B_{2})}\\ {{\tt unify}(E,}&\forall{x}:{A_{1}}.\ {B_{1}}&,&\forall{x}:{A_{2}}.\ {B_{2}}&)&\triangleq&\forall{x}:{{\tt unify}(E,A_{1},A_{2})}.\ {{\tt unify}(E,B_{1},B_{2})}\\ {{\tt unify}(E,}&\Sigma{x}:{A_{1}}.\ {B_{1}}&,&\Sigma{x}:{A_{2}}.\ {B_{2}}&)&\triangleq&\Sigma{x}:{{\tt unify}(E,A_{1},A_{2})}.\ {{\tt unify}(E,B_{1},B_{2})}\\ {{\tt unify}(E,}&{\tt Rec}({n_{1}})({\alpha}\Rightarrow{\tau_{1}})&,&{\tt Rec}({n_{2}})({\alpha}\Rightarrow{\tau_{2}})&)&\triangleq&{\tt Rec}({E[n_{1},n_{2}]})({\alpha}\Rightarrow{{\tt unify}(E,\tau_{1},\tau_{2})})\\ {{\tt unify}(E,}&\{{x}:~{}{A_{1}}~{}|~{}{p_{1}}\}&,{}&\{{x}:~{}{A_{2}}~{}|~{}{p_{2}}\}&)&\triangleq&\{{x}:~{}{{\tt unify}(E,A_{1},A_{2})}~{}|~{}{E[p_{1},p_{2}]}\}\\ {{\tt unify}(E,}&{t_{1,1}}\equiv{t_{1,2}}&,&{t_{2,1}}\equiv{t_{2,2}}&)&\triangleq&{E[t_{1,1},t_{2,1}]}\equiv{E[t_{1,2},t_{2,2}]}\\ \end{array}$$

$$\mathtt{If}{t}_1\mathtt{Then}{\tau }_2\mathtt{Else}{\tau }_3$$

$$\mathtt{Let}x=t\mathtt{in}\tau$$

$$Either\_Match(t,x\Rightarrow {\tau }_1,x\Rightarrow {\tau }_2)$$

Full text

††journalvolume: ††article: ††publicationmonth: 10††copyright: none

1. Introduction

Automatically verifying the correctness of higher-order programs is a long-standing problem that arises in most programming languages and proof assistants. Despite extensive research in program verifiers and proof assistants (Nipkow et al., 2002a; Bertot and Castéran, 2004a; Gordon and Melham, 1993; Harrison, 2009, 2017; Abel, 2010; Norell, 2007; Brady, 2013; Vazou et al., 2014; Swamy et al., 2013; Leino, 2010) there remain significant challenges and trade-offs in checking safety and termination. A motivation for our work are implementations that verify polymorphic functional programs using SMT solvers (Suter et al., 2011; Vazou et al., 2014). To focus on foundations, we look at simpler verifiers that do not perform invariant inference and are mostly based on unfolding recursive definitions and encoding of higher-order functions into SMT theories (Suter et al., 2011; Voirol et al., 2015; Blanc and Kuncak, 2015). A recent implementation of such a verifier is the Stainless system (LARA, 2019), which handles a subset of Scala (Odersky et al., 2008). The goal of Stainless is to verify that function contracts hold and that all functions terminate. It was shown (Hupel and Kuncak, 2016) how to map certain patterns of specified Scala programs into Isabelle/HOL. Whereas this approach ensures soundness, it does not reuse the reasoning of Stainless and it can verify only some of the programs that Stainless verifier can prove. The present paper seeks to provide direct foundations for verification and termination checking of functional programs with a rich set of features for purely functional programming including non-monotonic data types. On the other hand, our calculus does not aspire to directly support effects for which there exist excellent other systems (Swamy et al., 2013).

The subtleties of ensuring function termination have been an initial impetus for the calculus we present. Termination is desirable for many executable functions in programs and is even more important in formal specifications. A non-terminating function definition such as $f(x)=1+f(x)$ could be easily mapped to a contradiction and violate the conservative extension principle for definitions. Yet termination in the presence of higher-order functions and data types is challenging to ensure. For example, when using non-monotonic recursive types, terms can diverge even without the explicit use of recursive functions, as illustrated by the following snippet of Scala code:

⬇

case class D(f: D $\Rightarrow$ Unit) // non-monotonic recursive type

def g(d: D): Unit = d.f(d) // non-recursive function definition

g(D(g)) // diverging term, reduces to D(g).f(D(g)) and then again to g(D(g))

Furthermore, even though the concept of termination for all function inputs is an intuitively clear property, its modular definition is subtle: a higher order function $g$ taking another function $f$ as an argument should terminate when given any terminating function $f$, which, in turn, can be applied to expressions involving further calls to $g$. The quest for solid foundations for termination led us to type theoretic techniques, where reducibility method has long been used to show strong normalization of expressive calculi (Tait, 1967), (Girard, 1990, Chapter 6), (Harper, 2016). As a natural framework for analyzing support for first-class functions with preconditions and post-conditions we embraced the ideas of refinement dependent types similar to those in Liquid Haskell (Vazou et al., 2014) with refinement-based notion of subtyping. To explain proof obligation generation in the higher-order case (including the question of which assumptions should be visible when checking a given assertion), we resorted to well-known dependent ($\Pi$) function types. To support parametric polymorphism we incorporated type quantifiers, as in System F (Girard, 1971, 1990). We found that the presence of refinement types allowed us to explain soundness of well-founded recursion based on user-defined measures. The recursion in programs is thus not syntactically restricted as in, e.g., System F. To provide expressive support for iterative unfolding of recursive functions, we introduced rules to make function bodies available while type checking of recursive functions. For recursive type definitions, many existing systems introduce separate notions of inductive and co-inductive definitions. We found this distinction less natural for developers and chose to support expressive recursive types (without a necessary restriction to positive recursion) using sized types (Abel, 2010). We draw inspiration from a number of existing systems, yet our solution is a new sound combination of features that work nicely together.

We combined these features into a new type system, System FR, which we present as a bidirectional type checking algorithm. The algorithm generates type checking and type inference goals by traversing terms and types, until it reaches a point where it has to check that a given term evaluates to true. This typically arises when we want to check that a term $t$ has a refinement type $\{{x}:~{}{T}~{}|~{}{b}\}$, which is the case when $t$ has type $T$, and when the term $b$ evaluates to true in the context where $x$ equals $t$. Following the tradition of SMT-based verifiers (Detlefs et al., 1998; Barnett et al., 2004), we use the term verification condition (VC) to refer to a term that should evaluate to true.

We prove the soundness of our type system using a reducibility interpretation of types. The goal of our verification system is to ensure that a given term belongs to the semantic denotation of a given type. For simple types such as natural numbers, this denotation is the set of untyped lambda calculus terms that evaluate, in a finite number of steps, to a non-negative integer. For function types the denotation are, as is typical in reducibility approaches, terms that, when applied to terms in denotation of argument type, evaluate to terms in the denotation of the result type. Such denotation gives us a unified framework for function contracts expressed as refinement types. The approach ensures termination of programs because the semantics of types only contain terms that are terminating in call-by-value semantics.

We have formally proven using the Coq proof assistant (Bertot and Castéran, 2004a) the soundness of our typing algorithm, implying that when verification conditions generated for checking that a term $t$ belongs to a type $T$ are semantically valid, the term $t$ belongs to the semantic denotation of the type $T$. The bidirectional typing algorithm handles the expressive types in a deterministic and predictable way, which enables good and localized error reporting to the user. To solve generated verification conditions, we use existing implementation invoking the Inox solver111https://github.com/epfl-lara/inox that reduces higher-order queries to the first-order language of SMT solvers (Voirol et al., 2015). Our semantics of types provides a definition of soundness for such solvers; any solver that respects the semantics can be used with our verification condition generator. Our bidirectional type checking algorithm thus becomes a new, trustworthy verification condition generator for Stainless. We were successful in verifying many existing Stainless benchmarks using the new approach.

We summarize our contributions as follows:

• •

We present a rich type system, called System FR, that combines System F with dependent types, refinements, equality types, and recursive types (Sections 3 and 4).

• •

We define a bidirectional type-checking algorithm for System FR (Section 5). Our algorithm generates verification conditions that are solved by the (existing) SMT-based solver Inox.

• •

We prove222https://github.com/epfl-lara/SystemFR/tree/oopsla2019 soundness of our bidirectional type-checking algorithm that reduces program correctness to proving that certain formulas always evaluate to true (Section 6). Our formalization also supports additional expressive notions, such as infinite intersections and unions as well as refinement conditions given by non-emptiness of an arbitrary type.

• •

We built a verification condition generator based on these foundations333https://github.com/jad-hamza/stainless/tree/type-inference and evaluated it on around $14$k lines of benchmarks (Section 7), showing that generating proof obligations using type checking is effective in practice.

2. Examples of Program Verification and Termination Checking

Our goal is to verify correctness and termination of pure Scala functions written as in Figure 1. $pre$[x] is the precondition of the function f, and is written by the user in the same language as the body of f. The precondition may contain arbitrary expressions and calls to other functions. Similarly, the user specifies in $post$ the property that the results of the function should satisfy. To ensure termination of f (which might call itself recursively), the user may also provide a measure using the decreases keyword, which is also an expression (of type ${\sf Nat}$, the type of natural numbers) written in the same language. $\tau_{1}$ and $\tau_{2}$ may be arbitrary types, including function types or algebraic data types. Informally, the function is terminating and correct, if, for every value v of type $\tau_{1}$ such that $pre$[v] evaluates to ${\tt true}$, f(v) returns (in a finite number of steps) a value res of type $\tau_{2}$ such that $post$[v,res] evaluates to ${\tt true}$. By using dependent and refinement types, this can be summarized by saying that the function f has type: $\Pi{x}:{\{{x}:~{}{\tau_{1}}~{}|~{}{pre[x]}\}}.\ {\{{res}:~{}{\tau_{2}}~{}|~{}{post[x,res]}\}}.$

As an example, consider the list type as defined in Figure 3. We use $\mathbb{Z}$ to denote the type of integers (corresponding to Scala’s BigInt in actual source code). The function filter filters elements from a list, while count counts the number of occurrences of an integer in the list. These two functions have no pre- or postconditions. The decreases clauses specify that the functions terminate because the size of the list decreases at each recursive call.

Using these functions we define partition in Figure 3, which takes a list l of integers and partitions it according to a predicate p: $\mathbb{Z}\Rightarrow{\sf Bool}$. We prove in the postcondition that partitioning coincides with applying filter to the list with p and its negation.

Figure 4 shows a theorem that partition also preserves the multiplicity of each element. We use here count to state the property, but we could have used multisets instead (a type which is natively supported in Stainless). The holds keyword is a shorthand for ensuring { res => res }. The @induct annotation instructs the system to add a recursive call to partitionMultiplicity on the tail of l when l is not empty. This gives us access to the multiplicity property for the tail of l, which the system can then use automatically to prove that the property holds for l itself. This corresponds to a proof by induction on l.

Figure 5 shows a function isSorted that checks whether a list is sorted, and a function merge that combines two sorted lists in a sorted list. When given the above input, the system proves the termination of all functions, establishes that postconditions of functions hold, and shows that the theorem holds, without any user interaction or additional annotations. For the merge function, the postcondition might seem too weak to establish that e.g. Cons(x, merge(xs, l2)) is sorted just based on the fact that merge(xs, l2) is sorted. However, since we put the definition of merge while type-checking the body of merge in the context, it is possible to establish that x is smaller than the head of merge(xs, l2). We give more details on this feature of our system, called body-visible recursion, in Section 5.3.

2.1. Reasoning about Streams

Our system also supports reasoning about infinite data structures, including streams that are computed on demand. These data structures are challenging to deal with because even defining termination of an infinite stream is non-obvious, especially in absence of a concrete operation that uses the stream. Given some type X, ${\tt Stream}[{\tt X}]$ represents the type of infinite streams containing elements in X. In a mainstream call-by-value language such as Scala, this type can be defined as:

⬇

case class Stream[X](head: X, tail: ${()}{\Rightarrow}$ Stream[X])

For the sake of concise syntax, we typeset a function taking unit, (u:Unit)=>e, using Scala’s syntax ${()}{\Rightarrow}$e for a function of zero parameters. Given a stream s: ${\tt Stream}[{\tt X}]$, we can call s.head to get the head of the stream (which is of type X), or s.tail to get the tail of the stream (which is of type ${()}{\Rightarrow}{\tt Stream}[{\tt X}]$). We can use recursion to define streams, as shown in figures 8, 8, 8. The @erasable annotation is used to mark the erasable parameters n of these functions. These parameters are used as annotations to guide our type-checker, but they do not influence the computation and can be erased at runtime. For instance, an erased version of constant (without erasable code and without type annotation) looks like:

⬇

def constant(x) = Stream(x, ${()}{\Rightarrow}$ constant(x))

Informally, we can say that the constant stream is terminating. Indeed, it has the interesting property that, despite the recursion, for every $n\in\mathbb{N}$, we can take the first $n$ elements in finite time (no divergence in the computation). We say that constant(x) is an $n$-non-diverging stream. Moreover, when a stream is $n$-non-diverging for every $n\in\mathbb{N}$, we simply say that it is non-diverging, which means that we can take as many elements as we want without diverging, which is the case for constant(x). Note that non-divergence of constant cannot be shown by defining a measure on its argument x that strictly decreases on each recursive call, because constant is called recursively on the exact same argument x. Instead, we define a measure on the erasable argument n of the annotated version. This corresponds to using type-based termination (Abel, 2008, 2007; Barthe et al., 2008), where the type of the function for the recursive call is smaller than the type of the caller. We expand on that technique in Section 5.2.

In the annotated version of constant from Figure 8, the notation ${\tt Stream}[{\tt X}](n)$ stands for streams of elements in X which are n-non-diverging. The type of constant then states that constant can be called with any (erasable) parameter n to build an n-non-diverging stream. Since parameter n is computationally irrelevant, this proves that the erased version of constant returns a non-diverging stream.

We now give a variant of constant which is diverging:

⬇

def badConstant(x) = Stream(x, ${()}{\Rightarrow}$ badConstant(x).tail())

Indeed, given some x, a call to badConstant(x).tail() ends up evaluating badConstant(x).tail() again, and would diverge.

The zipWith function in Figure 8 takes two streams and a function f. It creates a new stream by applying f to pairs of elements taken from each stream. For zipWith, we can verify that as long as f terminates on every input, and s1 and s2 are non-diverging streams, then zipWith returns a non-diverging stream. We can then use zipWith to define the well-known Fibonacci stream (Figure 8), an infinite stream containing the Fibonacci sequence: 0, 1, 1, 2, 3, 5, 8, 13, etc. We make use of a function plus:$\mathbb{Z}\Rightarrow\mathbb{Z}\Rightarrow\mathbb{Z}$ that computes the sum of two integers. Just like the constant streams, fib is a non-diverging stream. For instance, calling fib.tail().tail().tail().head returns (in finite time) the number $2$ from the Fibonacci sequence.

The important property that the type signature of zipWith ensures is that, for every $n\in{\sf Nat}$, if s1 and s2 are $n$-non-diverging streams, then zipWith f s1 s2 is $n$-non-diverging as well. Our type system can check this property and then use it to make sure that the definition of fib type-checks. We can also prove further properties of interest, e.g., that zipping two streams s1 and s2 with the function (x:${\sf Nat}$)$\Rightarrow$(y:${\sf Nat}$)$\Rightarrow$x returns a stream that behaves as the stream s1.

3. Syntax and Operational Semantics

We now give a formal syntax for terms and show call-by-value operational semantics. This untyped lambda calculus with pairs, tagged unions, integers, booleans, and error values models programs that our verification system supports. It is Turing complete and rather conventional.

3.1. Terms of an Untyped Calculus

Let $\mathcal{V}$ be a set of variables. We let ${\sf Terms}$ be the set of all (untyped) terms (see Figure 9) which includes the unit term ${\tt()}$, pairs, booleans, natural numbers, a recursor rec for iterating over natural numbers, a pattern matching operator match for natural numbers, a recursion operator fix, an error term ${\tt err}$ to represent crashes. The recursor rec can be simulated using fix and match but we keep it in the paper for presenting examples.

The terms ${\tt fold}({t})$ and ${\tt unfold}\ {t_{1}}\ {\tt in}\ {x\Rightarrow t_{2}}$ are used to represent data structures (such as lists or streams), where ‘${\tt fold}({}){}$’ plays the role of a constructor, and ‘${\tt unfold}\ {}\ {\tt in}\ {}$’ the role of a deconstructor. The terms $\Lambda{t}$ and ${t}[{}]$ are used to represent the erasure of type abstractions and type instantiation terms (for polymorphism) of the form $\Lambda{\alpha}.\ {t}$ and ${t}[{\tau}]$, where $\alpha$ is a type variable and $\tau$ is a type. These annotated terms will be introduced in a further section.

The term ${\tt size}({t})$ is a special term to internalize the sizes of syntax trees of values (ignoring lambdas) of our language. It is used for measure of recursive functions such as the map examples on lists shown in Section 2.

Given a term $t$ we denote ${\sf fv}({t})$ the set of all free variables of $t$. Terms are considered up to renaming of locally bound variables (alpha-renaming).

3.2. Call-by-Value Operational Semantics

The set ${\sf Val}$ of values of our language is defined (inductively) to be ${\tt zero}$, ${\tt()}$, ${\tt true}$, ${\tt false}$, every variable $x$, every lambda term $\lambda{x}.\ {t}$ or $\Lambda{t}$, the terms of the form ${\tt succ}({v})$ or ${\tt fold}({v})$ where ${v}\in{\sf Val}$, and the terms of the form $(v_{1},v_{2})$ where $v_{1},v_{2}\in~{\sf Val}$.

The call-by-value small-step relation between two terms $t_{1},t_{2}\in{\sf Terms}$, written $t_{1}\hookrightarrow t_{2}$, is standard for the most part and given in Figure 10. Given a term $t$ and a value $v$, ${t}[{x}~{}\mapsto~{}{v}]$ denotes the term $t$ where every free occurrence of $x$ has been replaced by $v$.

To evaluate the fixpoint operator fix, we use the rule ${\tt fix}({y\Rightarrow t})\hookrightarrow t[y\mapsto\lambda{()}.\ {{\tt fix}({y\Rightarrow t})}]$, which substitutes the fix under a lambda with unit argument. We do this wrapping of fix in a lambda term because we wanted all substitutions to be values for our call-by-value semantics, and fix is not. This also means that, to make a recursive call within $t$, one has to use y() instead of y.

To define the semantics of ${\tt size}({})$, we use a (mathematical) function ${\tt size\_sem}({})$ that returns the size of a value, ignoring lambdas for which it returns [math]. The precise definition is given in Figure 11.

We make use in the operational semantics of an evaluation context $\mathcal{E}$, which specifies through a hole $\mathcal{H}$ the next place where reduction can occur in a term. Inductively, an evaluation context $\mathcal{E}$ must be of one of the following forms:

[TABLE]

Given a term $t$, we denote by $\mathcal{E}[{t}]$ the context $\mathcal{E}$ where the hole $\mathcal{H}$ has been replaced by $t$.

We denote by $\hookrightarrow^{*}$ the reflexive and transitive closure of $\hookrightarrow$. A term $t$ is normalizing if there exists a value $v$ such that $t\hookrightarrow^{*}v$.

4. Types, Semantics and Reducibility

We give in Figure 12 the grammar for the types $\tau$ that our verification system supports. Given two types $\tau_{1}$ and $\tau_{2}$, we use the notation $\tau_{1}\rightarrow\tau_{2}$ for $\Pi{x}:{\tau_{1}}.\ {\tau_{2}}$ when $x$ is not a free variable of $\tau_{2}$. Similarly, we use the notation $\tau_{1}\times\tau_{2}$ for $\Sigma{x}:{\tau_{1}}.\ {\tau_{2}}$ when $x$ is not a free variable of $\tau_{2}$.

For recursive types, we introduce the notation:

[TABLE]

Then, the type of (non-diverging) streams informally introduced in Section 2 can be understood as a notation, when X is a type, for: ${\tt Stream}[{\tt X}]\triangleq{\tt Rec}({\alpha}\Rightarrow{{\tt X}\times({\sf Unit}\rightarrow\alpha)})$. Similarly, for a natural number $n$, the type of $n$-non-diverging streams ${\tt Stream}_{n}[{\tt X}]$ is a notation for ${\tt Rec}({n})({\alpha}\Rightarrow{{\tt X}\times({\sf Unit}\rightarrow\alpha)})$. Using this notation, we can also define finite data structures such as lists of elements from X, as follows: ${\tt List}[{\tt X}]\triangleq{\tt Rec}({\alpha}\Rightarrow{{{\sf Unit}}+{{\tt X}\times\alpha}})$.

We show in Section 4.3 that these types indeed correspond to streams and lists respectively.

Let ${\sf Type}$ be the set of all types. We define a (unary) logical relation on types to describe terms that do not get stuck (e.g. due to the error term ${\sf err}$, or due to an ill-formed application such as ‘${\tt true}\ {\tt zero}$’) and that terminate to a value of the given type. Our definition is inspired by the notion of reducibility or hereditary termination (see e.g. (Tait, 1967; Girard, 1990; Harper, 2016)), which we use as a guiding principle for designing the type system and its extensions.

4.1. Reduciblity for Closed Terms

For each type $\tau$, we define in Figure 13 mutually recursively the sets of reducible values $\llbracket\tau\rrbracket_{\textsf{v}}^{\theta}$ and reducible terms $\llbracket\tau\rrbracket_{\textsf{t}}^{\theta}$. In that sense, a type $\tau$ can be understood as a specification that some terms satisfy (and some do not).

These definitions require an environment $\theta$, called an interpretation, to give meaning to type variables. Concretely, an interpretation is a partial map from type variables to sets of terms. An interpretation $\theta$ has the constraint that for every type variable $\alpha\in{\sf dom}(\theta)$, $\theta(\alpha)$ is a reducibility candidate ${\sf C}$, which, in our setting, means that all terms in $\theta(\alpha)$ are (erased) values. The set of all reducibility candidates is denoted by ${\sf Candidates}\subseteq 2^{{\sf Terms}}$, and an interpretation $\theta$ is therefore a partial map in $\mathcal{V}\mapsto{\sf Candidates}$.

When the interpretation has no influence on the definition, we may omit it. For instance, for every $\theta\in(\mathcal{V}\mapsto{\sf Candidates})$, we have $\llbracket{\sf Nat}\rrbracket_{\textsf{v}}^{\theta}=\{{\tt zero},{\tt succ}({{\tt zero}}),{\tt succ}({{\tt succ}({{\tt zero}})}),\dots\}$, so we can just denote this set by $\llbracket{\sf Nat}\rrbracket_{\textsf{v}}$.

By construction, $\llbracket\tau\rrbracket_{\textsf{v}}^{\theta}$ only contains (erased) values (of type $\tau$), while $\llbracket\tau\rrbracket_{\textsf{t}}^{\theta}$ contains (erased) terms that reduce to a value in $\llbracket\tau\rrbracket_{\textsf{v}}^{\theta}$. For example, a term in $\llbracket{\sf Nat}\rightarrow{\sf Nat}\rrbracket_{\textsf{t}}^{\theta}$ is not only normalizing as a term of its own, but also normalizes whenever applied to a value in $\llbracket{\sf Nat}\rrbracket_{\textsf{v}}^{\theta}$.

The type $\{{x}:~{}{\tau}~{}|~{}{b}\}$ represents the values $v$ of type $\tau$ for which ${b}[{x}~{}\mapsto~{}{v}]$ evaluates to ${\tt true}$. We use this type as a building block for writing specifications (pre and postconditions).

The type $\forall{x}:{\tau_{1}}.\ {\tau_{2}}$ represents the values that are in the intersection of the types ${\tau_{2}}[{x}~{}\mapsto~{}{a}]$ when $a$ ranges over values of type $\tau_{1}$. This type differs from $\Pi{x}:{\tau_{1}}.\ {\tau_{2}}$ in the sense that a value in $\forall{x}:{\tau_{1}}.\ {\tau_{2}}$ belongs to every ${\tau_{2}}[{x}~{}\mapsto~{}{a}]$ for $a$ in $\tau_{1}$, while a value in $\Pi{x}:{\tau_{1}}.\ {\tau_{2}}$ is a function that, when applied to some $a$ in $\tau_{1}$, produces a value in ${\tau_{2}}[{x}~{}\mapsto~{}{a}]$. From a value $b$ in $\forall{x}:{\tau_{1}}.\ {\tau_{2}}$, we can build a value in $\Pi{x}:{\tau_{1}}.\ {\tau_{2}}$ (namely, $\lambda{x}.\ {b}$), while the other way around is not always possible.

The sum type ${\tau_{1}}+{\tau_{2}}$ represents values that are either of the form ${\tt left}({v})$ where $v$ is a reducible value of $\tau_{1}$, or of the form ${\tt right}({v})$ where $v$ is a reducible value of $\tau_{2}$.

The set of reducible values for the equality type $\llbracket{t_{1}}\equiv{t_{2}}\rrbracket_{\textsf{v}}^{\theta}$ makes use of a notion of equivalence on terms which is based on operational semantics. More specifically, we say that $t_{1}$ and $t_{2}$ are equivalent, denoted ${t_{1}}\approx{t_{2}}$, if for every value $v$, we have $t_{1}\hookrightarrow^{*}v\mit{~{}iff~{}}t_{2}\hookrightarrow^{*}v$. Note that this equivalence relation is defined even if we do not know anything about the types of terms $t_{1}$ and $t_{2}$, and it ensures that if one of the terms reduces to a value, then so does the other.

The type $\forall{\alpha}:{\tt Type}.\,{\tau}$ is the polymorphic type from System F. The set $\llbracket\forall{\alpha}:{\tt Type}.\,{\tau}\rrbracket_{\textsf{v}}^{\theta}$ is defined by using the environment $\theta$ to bind the type variable $\alpha$ to an arbitrary reducibility candidate.

We use the recursive type ${\tt Rec}({n})({\alpha}\Rightarrow{\tau})$ as a building block for representing data structures such as lists of streams. The definition of reducibility for the recursive type makes use of an auxiliary function ${\sf basetype}({})$ that can be seen as an (upper) approximation of the recursive type. Note that ${\sf basetype}_{\alpha}({\tau})$ (defined at the bottom of Figure 13) removes the type variable $\alpha$ from $\tau$.

Our reducibility definition respects typical lemmas that are needed to prove the soundness of typing rules, such as the following substitution lemma (see (Girard, 1971) for the lemma on System F), which we have formally proven (see also Section 6 below).

Lemma 4.1.

Let $\tau_{1}$ and $\tau_{2}$ be two types, and let $\alpha$ be a type variable that may appear in $\tau_{1}$ but not in $\tau_{2}$. Let $\theta$ be a type interpretation. Then, we have:

[TABLE]

4.1.1. Well-Foundedness of the Reduciblity Definition

We can show that the definition given Figure 13 is well-founded by defining a lexicographic measure $({\tt typeNodes}(\tau),{\tt index}(\tau))\in\mathbb{N}\times{\sf Terms}$ on types $\tau$. The function ${\tt typeNodes}(\tau)$ returns the size of the syntactic tree of type $\tau$, ignoring the terms that appear inside. This size roughly corresponds to the number of (top-level) type constructors in the tree of $\tau$. For example, ${\tt typeNodes}(\{{x}:~{}{\tau}~{}|~{}{p}\})=1+{\tt typeNodes}(\tau)$ (ignoring $p$), ${\tt typeNodes}({\tau_{1}}+{\tau_{2}})=1+{\tt typeNodes}(\tau_{1})+{\tt typeNodes}(\tau_{2})$, and ${\tt typeNodes}({t_{1}}\equiv{t_{2}})=0$. Ignoring the size of terms inside types ensures that given a type $\tau$, a term variable $x$, and a term $a$, we have: ${\tt typeNodes}({\tau}[{x}~{}\mapsto~{}{a}])={\tt typeNodes}(\tau)$. As a result, the measure ${\tt typeNodes}(\tau)$ in the definition of reducibility decreases for indexed types such as $\Sigma{x}:{\tau_{1}}.\ {\tau_{2}}$ or $\Pi{x}:{\tau_{1}}.\ {\tau_{2}}$.

The number ${\tt typeNodes}(\tau)$ decreases in every case of Figure 13, except for recursive types ${\tt Rec}({t})({\alpha}\Rightarrow{\tau})$ where the measure stays the same in the recursive call to the denotation on ${\tt Rec}({n})({\alpha}\Rightarrow{\tau})$ with $t\hookrightarrow^{*}{\tt succ}({n})$. This is where we use the second component of the lexicographic measure, ${\tt index}(\tau)$. We define ${\tt index}({\tt Rec}({t})({\alpha}\Rightarrow{\tau}))=t$ and ${\tt index}(\tau)={\tt err}$ for every other type. Then, given $t_{1},~{}t_{2}~{}\in~{}{\sf Terms}$, we consider $t_{1}$ to be (strictly) smaller than $t_{2}$ if there exist $v_{1},v_{2}\in\llbracket{\sf Nat}\rrbracket_{\textsf{v}}$, such that $t_{1}\hookrightarrow^{*}v_{1}$, $t_{2}\hookrightarrow^{*}v_{2}$, and $v_{1}$ is strictly smaller than $v_{2}$ when seen as a natural number. Therefore, the second component ${\tt index}({\tt Rec}({n})({\alpha}\Rightarrow{\tau}))=n$ is strictly smaller than ${\tt index}({\tt Rec}({t})({\alpha}\Rightarrow{\tau}))=t$ in the definition (because $t\hookrightarrow^{*}{\tt succ}({n})$), which ensures that the overall lexicographic measure decreases.

4.2. Reduciblity for Open Terms

Having defined reducibility for closed terms, we now define what it means for a term $t$ with free term and type variables to be reducible for a type $\tau$. Informally, we want to ensure that for every interpretation of the type variables, and for every substitution of values for the term variables, the term $t$ reduces in a finite number of steps to a value in type $\tau$. This is formalized by a (semantic) typing relation ${\Theta;\Gamma}\models_{\sf Red}{t}:{\tau}$ which is defined as follows.

First, a context $\Theta;\Gamma$ is made of a finite set $\Theta\subseteq\mathcal{V}$ of type variables and of a sequence $\Gamma$ of pairs in $\mathcal{V}\times{\sf Type}$. The domain of $\Gamma$, denoted ${\sf dom}(\Gamma)$ is the list of variables (in $\mathcal{V}$) appearing in the left-hand-sides of the pairs. We implicitly assume throughout the paper that all variables appearing in the domains are distinct. This enables us to use $\Gamma$ as a partial map from $\mathcal{V}$ to ${\sf Type}$. We use a sequence to represent $\Gamma$ as the order of variables is important, since a variable may have a (dependent) type which refers to previous variables in the context.

Given a partial map $\gamma\in\mathcal{V}\mapsto{\sf Terms}$, we write $\gamma(t)$ for the term $t$ where every variable $x$ is replaced by $\gamma(x)$. We use the same notation $\gamma(\tau)$ for applying a substitution to a type $\tau$.

Given a context $\Theta;\Gamma$, a reducible substitution for $\Theta;\Gamma$ is a pair of partial maps $\theta\in\mathcal{V}\mapsto{\sf Candidates}$ and $\gamma\in\mathcal{V}\mapsto{\sf Terms}$ where: ${\sf dom}(\theta)=\Theta$, ${\sf dom}(\gamma)={\sf dom}(\Gamma)$, and $\forall x\in{\sf dom}(\Gamma).\ \gamma(x)\in\llbracket\gamma(\Gamma(x))\rrbracket_{\textsf{v}}^{\theta}$.

Note that the substitution $\gamma$ is also applied to the type $\Gamma(x)$, since $\Gamma(x)$ may be a dependent type with free term variables. The set of all pairs of reducible substitutions for $\Theta;\Gamma$ is denoted $\llbracket\Theta;\Gamma\rrbracket_{\textsf{v}}$.

Finally, given a context $\Theta;\Gamma$, a term $t$ and a type $\tau$, we say that ${\Theta;\Gamma}\models_{\sf Red}{t}:{\tau}$ holds when for every pair of substitutions $\theta,\gamma$ for the context $\Theta;\Gamma$, $\gamma(t)$ belongs the reducible values at type $\gamma(\tau)$. Formally, ${\Theta;\Gamma}\models_{\sf Red}{t}:{\tau}$ is defined to hold when:

[TABLE]

Our bidirectional type checking and inference algorithm in Section 5 is a sound (even if incomplete) procedure to check ${\Theta;\Gamma}\models_{\sf Red}{t}:{\tau}$.

4.3. Recursive Types

We explain in this section how to interpret the type ${\tt Rec}({n})({\alpha}\Rightarrow{\tau})$ (see reducibility definition in Figure 13) and how the ${\tt Stream}[{\tt X}]$ and ${\tt List}[{\tt X}]$ types represent streams and lists.

4.3.1. Infinite Streams

For a natural number $n$, consider the type $S_{n}\triangleq{\tt Stream}_{n}[{{\sf Nat}}]\triangleq{\tt Rec}({n})({\alpha}\Rightarrow{{\sf Nat}\times({\sf Unit}\rightarrow\alpha)})$. Let us first see what $S_{n}$ represents for small values of $n$. As a shortcut, we use the notations [math], $1$, $2$, $\dots$ for ${\tt zero}$, ${\tt succ}({{\tt zero}})$, ${\tt succ}({{\tt succ}({{\tt zero}})})$, $\dots$

The definition $\llbracket S_{0}\rrbracket_{\textsf{v}}$ refers to ${\sf basetype}_{\alpha}({{\sf Nat}\times({\sf Unit}\rightarrow\alpha)})$, which is ${\sf Nat}\times\top$ by definition. This means that $\llbracket S_{0}\rrbracket_{\textsf{v}}$ is the set of values of the form ${\tt fold}({(a,v)})$, where $a\in\llbracket{\sf Nat}\rrbracket_{\textsf{v}}$, and $v\in{\sf Val}$.

By unrolling the definition, we get that $\llbracket S_{1}\rrbracket_{\textsf{v}}$ is the set of values of the form ${\tt fold}({v})$ where $v$ is in $\llbracket{\sf Nat}\times({\sf Unit}\rightarrow\alpha)\rrbracket_{\textsf{v}}^{{}[{\alpha}~{}\mapsto~{}{\llbracket S_{0}\rrbracket_{\textsf{v}}}]}$, which is the same (by Lemma 4.1) as $\llbracket{\sf Nat}\times({\sf Unit}\rightarrow S_{0})\rrbracket_{\textsf{v}}$. Therefore, $\llbracket S_{1}\rrbracket_{\textsf{v}}$ is the set of values of the form ${\tt fold}({a,f})$ where $a\in\llbracket{\sf Nat}\rrbracket_{\textsf{v}}$ and $f\in\llbracket{\sf Unit}\rightarrow S_{0}\rrbracket_{\textsf{v}}$. This means that when it is applied to ${\tt()}$, $f$ terminates and returns a value in $\llbracket S_{0}\rrbracket_{\textsf{v}}^{\theta}$. Similarly, $\llbracket S_{2}\rrbracket_{\textsf{v}}$ is the set of values of the form ${\tt fold}({a,f})$ where $n\in\llbracket{\sf Nat}\rrbracket_{\textsf{v}}$ and $f\in\llbracket{\sf Unit}\rightarrow S_{1}\rrbracket_{\textsf{v}}$.

To summarize, we can say that for every $n\in\llbracket{\sf Nat}\rrbracket_{\textsf{v}}$, $S_{n}$ represents values of the language that behave as streams of natural numbers, as long as they are unfolded at most $n+1$ times. This matches the property we mentioned in Section 2, as $S_{n}$ represents the streams that are $n+1$-non-diverging. We can show that as $n$ grows, $S_{n}$ gets more and more constraints: $\llbracket S_{0}\rrbracket_{\textsf{v}}\supseteq\llbracket S_{1}\rrbracket_{\textsf{v}}\supseteq\llbracket S_{2}\rrbracket_{\textsf{v}}\supseteq\dots$ In the limit, a value $v\in\llbracket\forall{n}:{{\sf Nat}}.\ {S_{n}}\rrbracket_{\textsf{v}}$ (which is in every $S_{n}$ for $n\in\llbracket{\sf Nat}\rrbracket_{\textsf{v}}$), represents a stream of natural numbers, that, regardless of the number of times it is unfolded, does not diverge, i.e. a non-diverging stream. Equivalently, we have $v\in\llbracket{\tt Stream}[{{\sf Nat}}]\rrbracket_{\textsf{v}}$.

4.3.2. Finite Lists

Types of the form ${\tt Rec}({\alpha}\Rightarrow{\tau})$ can also be used to represent finite data structures such as lists. We let ${\tt List}_{n}[{\tt X}]$ be a notation for ${\tt Rec}({n})({\alpha}\Rightarrow{{{\sf Unit}}+{{\tt X}\times\alpha}})$, so that:

[TABLE]

Here are some examples to show how lists are encoded:

• •

The empty list is ${\tt fold}({{\tt left}({})})$,

• •

A list with one element $n$ is ${\tt fold}({{\tt right}({n,{\tt fold}({{\tt left}({})})})})$,

• •

Given an element $n$ and a list $l$, we can construct the list $n::l$ by writing: ${\tt fold}({{\tt right}({n,l})})$.

Let us now see why ${\tt List}[{\tt X}]$ represents the type of all finite lists of elements in ${\tt X}$. The first thing to note is that given $n~\in~\llbracket{\sf Nat}\rrbracket_{\textsf{v}}$, ${\tt List}_{n}[{\tt X}]$ does not represent the lists of size $n$. For instance, we know that $\llbracket{\tt List}_{0}[{\tt X}]\rrbracket_{\textsf{v}}$ is the set of values of the form ${\tt fold}({v})$ where $v\in\llbracket{\sf basetype}_{\alpha}({{{\sf Unit}}+{{\tt X}\times\alpha}})\rrbracket_{\textsf{v}}$, i.e. $v\in\llbracket\top\rrbracket_{\textsf{v}}={\sf Val}$. Therefore, ${\tt List}_{0}[{\tt X}]$ contains lists of all sizes (and also all values that do not represent lists, such as ${\tt fold}({{\tt zero}})$ or ${\tt fold}({\lambda{x}.\ {({\tt()}}})$).

Instead, ${\tt List}_{n}[{\tt X}]$ can be understood as the values that, as long as they are unfolded no more than $n$ times, behave as lists. As for streams, we have: $\llbracket{\tt List}_{0}[{\tt X}]\rrbracket_{\textsf{v}}\supseteq\llbracket{\tt List}_{1}[{\tt X}]\rrbracket_{\textsf{v}}\supseteq\llbracket{\tt List}_{2}[{\tt X}]\rrbracket_{\textsf{v}}\supseteq\dots$ where the monotonicity follows because $\alpha$ only appears in positive positions in the definitions of the recursive types for streams and lists. In the limit, we can show that ${\tt List}[{\tt X}]$ contains all finite lists, and nothing more.

Lemma 4.2.

Let $v\in~{\sf Val}$ be a value and ${\tt X}$ be some type. Then, $v\in\llbracket{\tt List}[{\tt X}]\rrbracket_{\textsf{v}}$ if and only if there exists $k\geq 0$ and $a_{1},\dots,a_{k}\in\llbracket\tt X\rrbracket_{\textsf{v}}$ such that $v={\tt fold}({{\tt right}({a_{1},\dots\tt fold({{\tt right}({a_{k},{\tt fold}({{\tt left}({})})})})\dots})})$.

It may seem surprising that the type of streams ${\tt Rec}({\alpha}\Rightarrow{{\tt X}\times({\sf Unit}\rightarrow\alpha)})$ contains infinite streams while the type of lists ${\tt Rec}({\alpha}\Rightarrow{{{\sf Unit}}+{{\tt X}\times\alpha}})$ only contains finite lists. The reason is that, in a call-by-value language, a value representing an infinite list would need to have an infinite syntax tree, with infinitely many ${\tt fold}({})$’s (which is not possible). On the other hand, we can represent infinite streams by hiding recursion underneath a lambda term as shown in Section 2.

5. A Bidirectional Type-Checking Algorithm

In this section, we give procedures for inferring a type $\tau$ for a term $t$ in a context $\Theta;\Gamma$, denoted ${\Theta;\Gamma}\vdash{t}\Uparrow{\tau}$, as well as for checking that the type of a term $t$ is $\tau$, denoted ${\Theta;\Gamma}\vdash{t}\Downarrow{\tau}$. We introduce rules of our procedures throughout this section; the full set of rules is given in figures 14 and  15.

Our inference and checking rules give rise to conditions of the form ${\Theta;\Gamma}\vdash{t_{1}}\equiv{t_{2}}$. We call such checks verification conditions (in the rules, they are boxed and appear in blue color). The $\equiv$ sign is part of the judgment form, and does not describe a formula. We rely on an external solver to perform these checks, and assume that when the verification condition is considered valid by the solver, then: $\forall\theta,\gamma\in\llbracket\Theta;\Gamma\rrbracket_{\textsf{v}}.{\gamma({\sf erase}({t_{1}}))}\approx{\gamma({\sf erase}({t_{2}}))}$. This is an equivalent way of saying that $\llbracket{\gamma({\sf erase}({t_{1}}))}\equiv{\gamma({\sf erase}({t_{2}}))}\rrbracket_{\textsf{v}}^{\theta}$ is non-empty. Under these conditions, we have the following theorem.

Theorem 5.1 (Soundness of the Bidirectional Type-Checker).

If ${\Theta;\Gamma}\vdash{t}\Uparrow{\tau}$ holds or if ${\Theta;\Gamma}\vdash{t}\Downarrow{\tau}$ holds, then ${\Theta;{\sf erase}({\Gamma})}\models_{\sf Red}{{\sf erase}({t})}:{{\sf erase}({\tau})}$ holds.

5.1. Annotated Terms

In order to guide our type-checking algorithm, we require terms to be annotated. We give in Figure 16 the grammar for annotated terms. The term ${\tt inst}({t_{1}},{t_{2}})$ is used to instantiate a term $t_{1}$ which has a type of the form $\forall{x}:{\tau_{2}}.\ {\tau}$ to a particular term $t_{2}$ of type $\tau_{2}$, in the (Infer Forall Instantiation) type inference rule of Figure 14. The term ${\tt unfold\_pos}\ {t_{1}}\ {\tt in}\ {t_{2}}$ is an annotated variant of ${\tt unfold}\ {t_{1}}\ {\tt in}\ {t_{2}}$ (see rules (Infer Unfold) and (Infer Unfold Positive) in Figure 14). We discuss the difference between these rules in Section 5.6.

The type ${\tt Let}~{}{x}~{}=~{}{t_{2}}~{}{\tt in}~{}{\tau}$ represents the type $\tau$ where the variable $x$ is bound to $t_{2}$ by using let’s in each term that appears in $\tau$. The formal definition is given in Section 5.

Annotations such as $\lambda{x}:{\tau}.\ {t}$ or ${\tt inst}({t_{1}},{t_{2}})$ have no runtime influence and are erased (respectively to $\lambda{x}.\ {t}$ and $t_{1}$). We write ${\sf erase}({t})$ to refer to the erasure of $t$, where every annotation has been erased. The full definition is given in Appendix C, Figure 28.

When a type $\tau$ has annotated terms inside, we write ${\sf erase}({\tau})$ to erase their annotations. For instance ${\sf erase}({\{{x}:~{}{\tau}~{}|~{}{b}\}})$ refers to $\{{x}:~{}{\tau}~{}|~{}{{\sf erase}({b})}\}$. Moreover, for a context $\Gamma$, we write ${\sf erase}({\Gamma})$ to refer to the context $\Gamma$ where each type $\tau$ has been replaced by ${\sf erase}({\tau})$.

5.2. Contracts and Measures

The syntax we support in our verification tool translates into our core calculus presented above. In our tool we support named functions with contracts and measures which are desugared into fix terms. To compare natural numbers and express the fact that measures decrease, we use functions ‘<’, ‘<=’ and ‘==’ on natural numbers. These functions can be defined using the recursor rec (see Appendix E for definitions).

Figure 17 shows how, thanks to refinement types, the fix term can encode recursive functions (such as the one given in Section 2) that feature user-defined pre- and post-conditions and whose termination arguments relies on a user-defined measure function. The fix term shown on the right corresponds to the desugaring of the recursive function on the left whose contracts are given by the require and ensuring keywords, and whose measure is given by the decreases keyword. The contract terms $pre$ and $post$ are such that ${{\tt x}:\tau_{1}}\vdash{pre}:{{\sf Bool}}$ and ${{\tt x}:\tau_{1},{\tt res}:\tau_{2}}\vdash{post}:{{\sf Bool}}$, and the measure function $measure$ satisfies ${{\tt x}:\tau_{1}}\vdash{measure}:{{\sf Nat}}$. The term ${\tt pred}$ is a function of type $\{{n}:~{}{{\sf Nat}}~{}|~{}{{\tt zero}<n}\}\rightarrow{\sf Nat}$ that returns the predecessor of numbers greater than ${\tt zero}$.

We now explain how our type-checking algorithm ensures termination of such a function. Our type inference rule for fix is (Infer Fix). The side condition $n\notin{\sf fv}({{\sf erase}({t})})$ ensures that $n$ only appears in type annotations in $t$, and is not part of the computation. The other check corresponds to a proof by strong induction (over $n$) that the fix term has type $\forall{n}:{{\sf Nat}}.\ {\tau}$. Indeed, we have to check that $t$, the body of the fix term, has type $\tau$ (for some $n:{\sf Nat}$), under the assumption that $y$ (which is the variable representing the recursion) has type ${\tau}[{n}~{}\mapsto~{}{m}]$ for all $m<n$. The ‘${\sf Unit}\rightarrow$’ part of the type of $y$ corresponds to the fact that the operational semantics of fix replaces variable $y$ by the fix term under a lambda (as explained in Section 3).

The variable $p$ is a witness that the variable $y$ is equal to the fix term (under a lambda). This feature is useful for body-visible recursion, and is explained in Section 5.3.

Back to the encoding presented in Figure 17, we explain how the (Infer Fix) rule ensures that $measure$ decreases at each recursive call of function f. Assume that the premise of the (Infer Fix) rule holds, and that f is called with some value $v$ of type $\tau_{1}$, such that $measure[v]$ evaluates to some (term representing a) natural number $n$. By instantiating the premise of the (Infer Fix) rule for that particular $n$, we get that $E[x,{\tt inst}({f},{{\tt pred}({n})}){\tt()}]$ is well-typed under the condition that $f$ has type:

[TABLE]

First, in order for ${\tt pred}$ to be applied to $n$, we have to check that $n$ is non-zero, meaning that the measure of $v$ is strictly positive in the places where the recursive calls happen. This is ensured by the (Check Refinement) rule for checking refinement types (see Figure 15), which generates a verification condition.

Second, the rule (Infer Forall Instantiation) ensures that ${\tt inst}({f},{{\tt pred}({n})}){\tt()}$ takes arguments of type $\{{x}:~{}{\{{x}:~{}{\tau_{1}}~{}|~{}{pre}\}}~{}|~{}{measure\leq{\tt pred}({n})}\}$. Therefore, if $f$ is applied recursively to an argument $v^{\prime}$, the rule (Check Refinement) ensures that $measure[v^{\prime}]\leq{\tt pred}({n})$ holds. Overall, we get $measure[v^{\prime}]\leq{\tt pred}({n})<n=measure[v]$, which ensures that the measures of arguments always decrease on recursive calls to f.

In our implementation, we do not go through the encoding with fix and forall types, but instead directly generate the verification conditions that correspond to the measure decreasing by using the left-hand-side form of Figure 17. Our system also supports mutually recursive functions (by requiring that the measure decreases for each call to a mutually recursive function), which can be encoded in the usual way by defining a fix term that returns a tuple of functions.

In the end, if the body of the function is well-typed, the (Infer Fix) rule infers the type:

[TABLE]

One should note that this encoding imposes a scoping restriction on the original program, namely precondition, postcondition, and measure of a function $f$ cannot contain calls to $f$. This restriction has not proved limiting in our experience with benchmarks.

5.2.1. Lexicographic Orderings

Functions whose termination arguments require lexicographic orderings can be encoded by using two levels of recursions, which is a known technique that shows expressive power of System T (Girard, 1990, Section 7.3.2). We review how this encoding works in our system in Appendix A and show an example of Ackerman’s function and its simple lexicographic measure. In our implementation, we support lexicographic measures directly.

5.3. Body-Visible Recursion

In this section, we give more details about the (Infer Fix) and (Infer Rec) typing rules for recursion. They allow body-visible recursion which gives the type-checker access to the definition of a recursive function while type-checking the body of the recursive function itself.

The first thing to note is that we introduce an equality type containing the definition (in the type of $p$) in the context, while we do not know yet whether the body of the recursion is well-typed. Since our equality type is defined (in Section 4) for all terms, regardless of whether they are well-typed, this is perfectly legal. We show in the merge example of Figure 5 how body-visible recursion relieves the user from writing excessive specification annotations.

Assume we want to prove, on paper, that merge indeed returns a sorted list when given two sorted lists l1 and l2, by induction over size(l1) + size(l2). Consider the first branch of the if  then  else  statement, where we return Cons(x, merge(xs,l2)). By the induction hypothesis, we know that the recursive call merge(xs,l2) is sorted, but this mere fact is not enough to conclude that Cons(x, merge(xs,l2)) is sorted. By unfolding the definition of isSorted, we see that we need in addition to know that x is smaller than the head of the result merge(xs,l2).

Therefore, the property we prove by induction needs to be strengthened by saying that the head of the result, if non-empty, is equal to the (smallest) head of one the input lists. From that, we will know by the induction hypothesis that the head $h$ of merge(xs,l2) (if non-empty) is either the head of xs or the head of l2. In the first case, we can deduce that x is smaller than $h$ by using the fact that l1 = Cons(x,xs) is sorted. In the second case, we have $h={\tt y}$, and we know from the condition of the if  then  else  statement that x $\leq$ y. In both cases, we can conclude that the whole list Cons(x, merge(xs,l2)) is sorted.

If we are to type-check the program above, and if we only know the return type of merge(xs,l2), that is { l: List| isSorted(l) }, we will run into the same problem, and will not be able to conclude that Cons(x, merge(xs,l2)) is sorted. In our type system, we get in addition access to the definition of merge while type-checking it, thanks to the $p$ variable of equality type in the (Infer Fix) rule. By unfolding the definition of merge(xs,l2), we conclude by case analysis that the head $h$ of merge(xs,l2) (if non-empty) is either the head of xs or the head of l2 (which is y).

Without body-visible recursion, the developer would need to strengthen the postcondition to:

[TABLE]

In Inox, the external solver we use for verification conditions, definitions of recursive functions are unfolded automatically. Inox does incremental queries to SMT solvers. It first sends a query without unfolding at all, then a new query after unfolding once, and so on until a query succeeds or a timeout. Thanks to this approach, Inox does not rely on universal quantifiers to encode recursive functions. This feature is crucial to have such examples be verified without user intervention, and is here required to get the bodies of the calls to merge and isSorted when verifying the postcondition of merge.

5.4. Unification in Type Inference

In order to perform type inference, we expect a certain structure on the inferred types. For example, given term ${t_{1}}\ {t_{2}}$, we expect term $t_{1}$ to have a function type when inferring the type of an application. Furthermore, type inference must perform least upper bound computation for if, match and either_match terms, which adds more complexity to the system. We handle these considerations in a generalized manner by performing type unifications, defined in Figure 18 by using the type-level notations If Then Else, Let, Either_Match, and Match.

We draw attention here to the fact that our type checking and inference procedures are syntax directed and predictable, which enables a natural verification process through term-level hints. The algorithmic nature of our type checking precludes the verification of certain well-typed programs. However, our experience has shown that this limitation is largely inconsequential in practice and is outweighed by the predictable nature of the algorithm.

5.5. Hiding Recursive Type Indices

Beyond general rules of Figure 14, in Figure 19 we show two additional rules for ‘fold’ and ‘unfold in’ that ignore the indices hidden under the Rec type for strictly positive recursive types (which is the case for the List and Stream types). We write ${\tt spos}({\alpha},{\tau})$ when a type variable appears only strictly positively in type $\tau$, meaning only to the right of $\Pi$ and $\forall$ types (see Appendix B for the precise definition). This enables us, under some conditions, to fold and unfold a strictly positive recursive type without worrying about indices.

Practically, given an element $l$ of type ${\tt List}[{\tt X}]$ (resp. ${\tt Stream}[{\tt X}]$), we can unfold it (with the (Infer Unfold Gen) rule) to get its head and its tail of type ${\tt List}[{\tt X}]$ (resp. $Unit\rightarrow{\tt Stream}[{\tt X}]$). Conversely, we use the rule (Infer Fold Gen) to build a list or a stream from an element and a tail.

Strict positivity gives us the following key lemma that ensures the soundness of our rules with respect to our reducibility definition. This lemma states that when a type variable $\alpha$ appears only strictly positively in $\tau$, then quantifying with a forall type outside $\tau$ or inside a substitution for $\alpha$ is the same (as long as we are quantifying over a non-empty type $\tau_{1}$). This property is similar to the notions lim sup-pushable and lim inf-pullable (Abel, 2008) and implies the soundness of our rules.

Lemma 5.2.

Let $\tau$ and $\forall{x}:{\tau_{1}}.\ {\tau_{2}}$ be two types. Let $\alpha$ be a type variable that appears strictly positively in $\tau$. Let $\theta$ be a type interpretation such that $\llbracket\tau_{1}\rrbracket_{\textsf{v}}^{\theta}$ is not empty. We have:

[TABLE]

5.6. Type-Checking Algorithm Examples: Streams

5.6.1. Constant Stream

The fix term and associated typing rules can also be used to express the kind of recursion used to define the streams in Section 2. We start by revisiting the constant stream, which in our notations can be written as an untyped term:

[TABLE]

Assume we want to prove, on paper, that for any value $x$, $\tt{{\tt constant}}[{}](x)$ produces a non-diverging stream, i.e. a stream which is $n$-non-diverging for every $n\in\mathbb{N}$. A natural proof could be done by induction on $n$, as follows:

• •

$(n=0)$ $\tt{{\tt constant}}[{}](x)$ is [math]-non-diverging, meaning that it reduces to a value of the form ${\tt fold}({x,v})$ where $x$ and $v$ are values. This is clear from the code of constant, as this expression evaluates in a few steps to ${\tt fold}({x,\ \lambda{u}.\ {{(\lambda u^{\prime}.{\tt constant})()}[{}](x)}})$.

• •

$(n=n^{\prime}+1)$ Assume by induction that $\tt{{\tt constant}}[{}](x)$ is $n^{\prime}$-non-diverging. By definition of $n$-non-diverging, we get that ${\tt fold}({x,\ \lambda{u}:{{\sf Unit}}.\ {{{\tt constant}}[{}](x)}})$ is $n$-non-diverging. Since this term is equivalent to the term to which $\tt{{\tt constant}}[{}](x)$ evaluates, we conclude that $\tt{{\tt constant}}[{}](x)$ is $n$-non-diverging as well.

Our type system and type-checking algorithm can be used to simulate this proof by using an annotated version of constant:

[TABLE]

where ${\tt body(n,constant)}$ is a shorthand for

[TABLE]

By applying the (Infer Fix) rule presented above, we get the type

[TABLE]

The (Infer Fix) rule of our algorithm generates a check that corresponds to a (strong) induction that shows that for every $n\in\llbracket{\sf Nat}\rrbracket_{\textsf{v}}$, ${\tt constant}[X](x)$ in $\llbracket{\tt Stream}_{n}[{X}]\rrbracket_{\textsf{v}}$ assuming that it is in $\llbracket{\tt Stream}_{m}[{X}]\rrbracket_{\textsf{v}}$ for all $m<n$:

[TABLE]

After applying standard rules related to $\lambda$ and $\Lambda$, our algorithm will attempt to infer, using the (Infer Fold) rule, a type for the term:

[TABLE]

In addition to the type-check that $n$ has type ${\sf Nat}$, this rule generates two checks to cover the cases where $n$ is zero or non-zero. These correspond to the informal proof by induction given above for the non-divergence of constant. The first check reduces (after applying some straightforward rules) to checking that $\lambda{u}:{{\sf Unit}}.\ {{{\tt inst}({\tt constant},{{\tt pred}({n})}){\tt()}}[{X}](x)}$ has type $\top$ (remember that ${\sf basetype}_{\alpha}({X\times({\sf Unit}\rightarrow\alpha)})=X\times\top$), which goes through easily thanks to the rule (Check Top 1).

The second check amounts to checking that ${\tt inst}({\tt constant},{{\tt pred}({n})}){\tt()}{\tt[X](x)}$ has type ${\tt Stream}_{n^{\prime}}[{X}]$ under the assumption that ${n}\equiv{{\tt succ}({n^{\prime}})}$. By the context we know that ${\tt inst}({\tt constant},{{\tt pred}({n})}){\tt()}{\tt[X](x)}$ has type ${\tt Stream}_{{\tt pred}({n})}[{X}]$. Since $n^{\prime}$ and ${\tt pred}({n})$ are equivalent, we can use the rule (Check Recursive) (given in Figure 15) to convert between the two types.

Attempting to type-check the badConstant example from Section 2:

[TABLE]

where ${\tt badBody(n,badConstant)}$ stands for:

[TABLE]

will lead to an error in the second check (corresponding to the inductive case), since the extra call to tail() decreases the index of the stream by one.

5.6.2. ZipWith Function on Streams

We now revisit the zipWith function from Figure 8. We said in Section 2 that for every $n\in\mathbb{N}$, when s1 and s2 are $n$-non-diverging streams, then so is zipWith(f,s1,s2). On paper, we can check by induction over $n\in\mathbb{N}$ that when s1 and s2 are $n$-non-diverging streams and $f$ is terminating, then zipWith(f,s1,s2) (as written in Figure 8, and ignoring type annotations and the erasable parameter for the moment) is also an $n$-non-diverging stream.

• •

$(n=0)$ It is indeed the case that we can access the head of zipWith(f,s1,s2) as long as we can access the heads s1 and s2 (and as long as $f$ terminates).

• •

$(n=n^{\prime}+1)$ Let s1 and s2 be two $n$-non-diverging streams. By definition of non-diverging, we know that s1.tail() and s2.tail() are $n^{\prime}$-non-diverging. By induction hypothesis,

zipWith(f,s1.tail(),s2.tail()) is $n^{\prime}$-non-diverging as well. This means that zipWith(f,s1,s2) is $n$-non-diverging, which concludes the proof.

Accordingly, our type-checking algorithm is able to infer the type

[TABLE]

for the annotated zipWith term given in Figure 20. We use the term ‘unfold in’ to access the heads (with ${\pi_{1}}\ {}$). For the tails, we use instead ‘unfold_pos in’. To understand the difference, we must first look at the (Infer Fold) rule for the fold term, which will generate two subgoals, one with $n=0$ and one with $n>0$. In the subgoal with $n=0$, we must check that the lambda term ‘$\lambda u:Unit.[...]$’ has type $\top$, which goes through directly thanks to (Check Top 1). Therefore, when we are type-checking the body of the lambda, we know that $n>0$. We can thus access the tails using (Infer Unfold Positive), a variant of (Infer Unfold) that discards a subgoal with $n=0$ but requires proving $n>0$ instead.

5.6.3. Fibonacci Stream

We now consider the Fibonacci stream function from Figure 8. We can prove by induction that for all $n\in\mathbb{N}$, fib is an $n$-non-diverging stream. In our view, this corresponds to writing fib as in Figure 21.

When type-checking fib, we use the type of zipWith and instantiate it to pred(pred(n)), and get that: inst(zipWith,pred(pred(n))) has type:

[TABLE]

This is where we use the fact that zipWith returns an $n$-non-diverging stream when given $n$-non-diverging streams.

5.7. Verification of Properties

Finally, we show how to verify the property mentioned in Section 2: that zipping two streams s1 and s2 with the function $\lambda{x}.\ {\lambda{y}.\ {x}}$ returns a stream equivalent to s1.

We define a function zipWith_fst with the following type:

[TABLE]

For short, we denote this type as $\Pi{n}:{{\sf Nat}}.\ {\tau}$. The code of zipWith_fst is given in Figure 22 and makes use of the recursor rec. Our (Infer Rec) rule for inferring the type of rec is similar to fix. The difference is that rec allows references to $n$ in the code, so the computation is allowed to depend on $n$. Moreover, rec does not use $\forall$ types. Finally, rec is analogous to a simple induction, while fix is analogous to a strong induction.

In the zipWith_fst example, applying this rule corresponds to a proof by induction over $n$, that for any two streams s1 and s2, the $n$th element of s1 is equal to the nth element of $zipWith(\lambda{x}.\ {\lambda{y}.\ {x}},\tt s1,s2)$.

In the base case, to type-check the term ${{\tt refl}[{{\tt nth}\ 0\ {\tt s1}},{{\tt nth}\ 0\ (zipWith(\lambda{x}.\ {\lambda{y}.\ {x}},\tt s1,s2))}]}$, we must make sure that the following equality holds: ${{\tt nth}\ 0\ {\tt s1}}\equiv{{\tt nth}\ 0\ (zipWith(\lambda{x}.\ {\lambda{y}.\ {x}},\tt s1,s2))}.$

The corresponding type inference rule is (Infer Refl), which generates a verification condition.

In the inductive case, we explicitly instantiate our inductive hypothesis on the tails of s1 and s2 by using the let binding on variable pr. The equality given by the type of pr is then sufficient to prove what we wanted: ${{\tt nth}\ ({\tt succ}({n}))\ {\tt s1}}\equiv{{\tt nth}\ ({\tt succ}({n}))\ (zipWith(\lambda{x}.\ {\lambda{y}.\ {x}},\tt s1,s2))}.$

This example also illustrates that developers can express the desired versions of what others might call extensional equality (here: same results when calling nth) using $\Pi$ types and equi-reducibility $\equiv$; our type system does not impose any preferred form of extensional equality.

6. Formalization in the Coq Proof Assistant

We here give more details about our formalization of Theorem 5.1 in Coq 8.9.1 (including the rules from Section 5.5). Our proofs are available from

https://github.com/epfl-lara/SystemFR/tree/oopsla2019

We represent terms and types using a locally nameless representation (Charguéraud, 2012), where free variables are named, and where local variables are bound using De Bruijn indices. Using this representation, lambdas and other binders can be seen as terms with holes, which can be filled with other terms (typically values). We use the Coq Equations library (Sozeau, 2010) to define the reducibility logical relation $\llbracket\rrbracket_{\textsf{v}}$. This library facilitates the use of functions which are defined recursively based on a well-founded measure.

We give an overview of our files (containing around $20$k lines of code):

• •

Trees.v contains the definitions of types and terms,

• •

Typing.v gives all typing rules (containing rules from the paper and more),

• •

SmallStep.v contains the operational semantics of the language,

• •

ReducibilityDefinition.v contains the definition of reducibility,

• •

The Reducibility*.v files contain lemmas for the soundness of the rules from Typing.v,

• •

Reducibility.v contains the proof that all typing rules from Typing.v are sound with respect to the reducibility definition (which implies that Theorem 5.1 holds).

6.1. Extensions of Formalization

Our approach to formalization proved flexible and allowed us to extend the system with additional types. In addition to formalizing the types and rules for our type checking algorithm (figures 15 and 15), our Coq formalization also defines (Figure 23) reducibility for the bottom type, singleton types, union and intersection types, and an existential type more abstract than dependent pair (and dual to $\forall{x}:{\tau_{1}}.\ {\tau_{2}}$). We also formalized refinement by type ${\{}{\{}{x}:~{}{\tau_{1}}~{}|~{}{\tau_{2}}{\}}{\}}$, which generalizes refinements from computable terminating terms of our language to the condition of non-emptiness of arbitrary types in our system. Existential type and refinement by type can be viewed as second and first projections of dependent pairs. Together with existential and universal types, refinement by type allows us to refine types by quantified propositions, providing support for quantified preconditions and postconditions. Some of the type forms we present can be expressed using others; the set of type forms is not minimal.

We define further syntactic sugar, including precise if then else and match types (Figure 24), as an alternative to the ${\tt If}\ {t_{1}}\ {\tt Then}\ {t_{2}}\ {\tt Else}\ {t_{3}}$ that relies on simplifications of Figure 18. We rely on Let type of Figure 23, and we use the ill-typed ${\tt err}$ term in the computations of (respectively) pred, unfold_left and unfold_right, to make sure that the denotations of the Let types are empty when $t$ does not reduce (respectively) to a strictly positive natural number, ${\tt left}({t^{\prime}})$, or ${\tt right}({t^{\prime}})$ for some $t^{\prime}$. We proved soundness of typing rules that show that these types behave as expected. For instance, an if then else expression can be assigned an if then else type of the branches.

These types can be used to encode type level computation reminiscent to one present in Scala HList444https://github.com/milessabin/shapeless/blob/master/core/src/main/scala/shapeless/hlists.scala, as illustrated by the following example. Given a list $L:{\tt List}[{Bool}]$ and types $\tau_{1}$ and $\tau_{2}$, we define a type ${\tt TypeFromList}(L,\tau_{1},\tau_{2})$ that represents nested pairs from $\tau_{1}$ and $\tau_{2}$ according to the boolean values (${\tt false}$ for $\tau_{1}$ and ${\tt true}$ for $\tau_{2}$) and with nesting given by the length of $L$. For example, when $L$ is the list ${\tt true},{\tt false},{\tt true}$ then ${\tt TypeFromList}(L,{\sf Nat},{\sf Nat}\to{\sf Nat})$ represents nested tuples $w$ of the form $(a_{0},(a_{1},(a_{2},\ldots)))$ where $a_{0}:{\sf Nat}$, $a_{1}:{\sf Nat}\to{\sf Nat}$, $a_{2}:{\sf Nat}$.

[TABLE]

The function ${\tt nth}(L,n)$ returns the $n$th element of the list $L$ (defined as a recursive data type). The function ${\tt get}(w,n)$ is also a term-level function that operates on nested pairs $w$ such that e.g. ${\tt get}(w,2)$ expands to $\pi_{1}(\pi_{2}(\pi_{2}(w)))$. The type ${x}\equiv{{\tt get}(w,n)}$ in the expansion of refinement by judgement-as-type ${\_}\,{:}{:}\,{\_}$ (Figure 24) does not require type checking the ${\tt get}$ function; its semantics (see $\approx$ in Figure 13) is that ${\tt get}(w,n)$ reduces to $x$ in the (untyped) operational semantics.

Furthermore, we prove soundness of multiple rules (such as congruence rules) for establishing the equality judgment ${\Theta;\Gamma}\vdash{t_{1}}\equiv{t_{2}}$ described in Section 5. We also prove soundness of a rule that unfolds the definition of a recursive function in the context, which is what is required by the solver in Section 5.3 to unfold the definition of merge. Such rules are a step towards justifying not only the verification condition generation but also verification condition solving.

7. Implementation and Evaluation

We have implemented our bidirectional type checking procedure by writing an alternative verification-condition generator for Stainless555https://github.com/epfl-lara/stainless (LARA, 2019). The code is merged into master and available in e.g. release version 0.4.0. Its functionality can be invoked with the --type-checker command line option in both scalac 2.12 and Dotty front end pipeline for Stainless. Thanks to these frontends, which provide a form of type inference, the type annotation burden is lessened for the user. Precise types such as indexed recursive types (which are not supported out of the box by these frontends) still need to be annotated manually.

The implementation was evaluated on benchmarks shown in Figure 25 totalling 14k LoC, collected from existing Stainless test suites and case studies. The proof/code ratio depends on the properties being proven. It can be 0 or close to 0 as in the merge example of Section 2, or higher than 1 when writing lemmas for proving detailed specifications (as in the Huffman coding example). The benchmarks reside in the frontends/benchmarks/typechecker/valid directory of Stainless. The streams benchmark relies on more expressive annotations of the Dotty compiler that we use to write recursive types, and is available in frontends/benchmarks/dotty-specific/typechecker. We use the following syntax to represent indexed types:

[TABLE]

The suite of all benchmarks verifies in $\sim$6 minutes in total when using implementation based on our type checker. The table shows the number of lines of codes within each benchmark, and the number of verification conditions which were generated by the type checker and verified by the SMT-backed Inox solver. The time given includes the time for generating the verification conditions and solving them, but not the parsing and compilation which is done by the Scala compiler scalac (which we use for some initial type inference and to obtain a tree representation of the program), nor the transformations which are internal to Stainless and which happen before using the type-checker. To understand the impact of these time measurements, note that 11% of time of total verification time is spent in the bidirectional type-checking algorithm that generates verification conditions and that is the focus of this paper, 66% in checking the verification conditions using a SMT-backed solver Inox for recursive and higher-order functions, 13% for the parsing, name resolution and most of the type checking pipeline of Scala’s scalac compiler, and 10% for extraction of scalac abstract syntax trees to Stainless trees. All times were measured on a Lenovo X1 Carbon laptop with an Intel i7-7500U and 16GB RAM.

To illustrate the diversity of benchmarks, we note that InsertionSort, QuickSorts, MergeSorts and StableSort feature various implementations of the sorting algorithms with the typical properties shown. ListMonad and OptionMonad show that the monadic laws hold for the ${\tt List}[{\tt X}]$ and Option[X] types. The List and ListWithSize benchmarks feature a collection of common higher-order functions on lists such as map, filter, forall, etc., as well as many properties shown about the implementations. In the GodelNumbering benchmark, we prove that the pairing function $2^{x}(2y+1)-1$ is a bijection between natural numbers and pairs of natural numbers using a series of lemmas about linear and non-linear arithmetic. Similar non-linearity is featured in the MoreExtendedEuclidGCD benchmark where we show that an implementation of the extended Euclid’s algorithm indeed computes the greatest common divisor and the coefficients of Bézout’s identity. Benchmarks also include persistent data structures (Okasaki, 1998), ConcTree and ConcRope (Prokopec and Odersky, 2015), explicit state model checker ReachabilityChecker, small interpreters, dynamic programming algorithms such as Viterbi and Knapsack, and benchmarks solving assignments from Scala MOOCs (see https://courseware.epfl.ch/ or https://www.coursera.org/specializations/scala).

8. Related Work

In this paper, we tackle program verification using a type-theoretic approach. Other techniques, such as symbolic execution for verification (see e.g. (Nguyen et al., 2017; Hallahan et al., 2019)) or using term rewriting systems (see e.g. (Giesl et al., 2004, 2006, 2011)) can be used instead or in complement to our approach. The use of type checking in verification appears in program verifiers such as F* (Swamy et al., 2013; Ahman et al., 2017; Swamy et al., 2016) and Liquid Haskell (Vazou et al., 2013; Vazou et al., 2014, 2018). Like Dafny (Leino, 2010) and Stainless, these systems rely on SMT solvers to automatically discharge verification conditions.

F* is a dependently-typed programming language which supports a rich set of effects (such as divergence, mutation, etc.). To the best of our knowledge F* does not support proving termination of functions operating on infinite data structures such as streams. Stainless has a desugaring pass that handles local state and certain forms of unique references. Furthermore, for semantic modeling of global state, a user can use monad syntax (Scala’s for comprehensions) explicitly in the surface language, which Scala compiler desugars into higher-order functions that our system can handle. Overall, F* supports a more expressive class of effects than what Stainless currently handles. The goal of Liquid Haskell (Vazou et al., 2018) is to add refinement types to Haskell, a call-by-need language (while we focus here on call-by-value languages). The system supports a sound verification procedure which relies on decidable theories of SMT. The supported language imposes certain restrictions on refinement occurrences and the metatheory does not feature recursive types (although they are supported by the implementation). Similarly to our body-visible recursion, Liquid Haskell allows the type checker to access the body of recursive functions (for recursive calls) while type-checking the function itself using a technique called refinement reflection (Vazou et al., 2018). Dafny verifier (Leino, 2010) supports imperative and object-oriented as well as functional programming, including inductive and coinductive types, recursion using ordinals, quantifiers. We are not aware of metatheory to justify the soundness of Dafny. In contrast, we provide a mechanized proof of soundness for System FR, which increases confidence in VC generation soundness. This is important because it is easy to construct paradoxes when combining features such as impredicativity and contravariant recursion. Being based on a reducibility relation, our proof can be used as a basis to add new language features in a compositional way. Several other systems have been recently formalized, such as MetaCoq (Sozeau et al., 2019).

Proof assistants with great expressive power include Isabelle (Nipkow et al., 2002b; Blanchette et al., 2017), Coq (Bertot and Castéran, 2004b; Barras, 2010; Sacchini, 2013), Idris (Brady, 2013), Agda (Norell, 2007; Abel, 2010), PML2 (Lepigre, 2017), Lean (de Moura, 2016) and Zombie (Casinghino et al., 2014). When coinduction is supported in these systems (which is not always the case), it is typically through special constructs for coinductive types and their corresponding cofixpoint operators, dual to inductive types and their fixpoint operators. In System FR, we instead treat induction and coinduction in a uniform way (see e.g. Section 5.6). Our type system features a single kind of recursive types which allow uniform definition of inductive, coinductive and mixed recursive types. Our operational semantics further rely on the fix operator which roughly corresponds to general recursion in mainstream programming call-by-value languages. An alternative approach to uniform handling of recursion and corecursion is given in (Gianantonio and Miculan, 2002). We were able to encode the first example from this work (in our Streams benchmark) which generates a stream and whose termination proof requires a combination of inductive and coinductive reasoning. Using our system, we expressed that using a simple lexicographic measure combining the index of the type of the produced stream with the inductive measure. In a private communication, Andreas Abel showed us that Agda can also handle this example.

Our system follows Nuprl (Constable et al., 1986) (and other computational type theories) style of starting out with an untyped calculus and then introducing various types to classify untyped terms based on their behaviors. Nuprl supports a very expressive type system, which covers the types we present in this paper, except impredicative polymorphism. In a large development, Nuprl’s metatheory has been formalized in Coq (Anand and Rahli, 2014). One part of that formalization relies on the use of the Coq axiom of functional choice FunctionalChoice_on, which gives a function $f$ from $A$ to $B$ when a formula of the form $\forall a:A.\ \exists b:B.\ \phi(a,b)$ holds. Nuprl does not use SMT solvers for automation, but relies instead on built-in and user-defined tactics similarly to Coq.

Our reducibility definition for recursive type is inspired from step-indexed logical relations (Ahmed, 2006). The main difference is that the indices in step-indexed logical relations do not appear at the level of types, but at the level of the logical relation that gives meaning to types. In System FR we internalize the indices at the level of recursive types in order to give more expressive power to the users, and let them specify decreasing measures for recursive functions that manipulate infinite data structures. This treatment of recursive types is similar to the TORES (Jacob-Rao et al., 2018) type system, where recursive types can be indexed by an arbitrary index language. We only support recursive types indexed by natural numbers. TORES provides a decision procedure for a rich type system with inductive types, coinductive types, and indexed recursive types, yet its metatheory does not handle polymorphism nor refinement types.

Our termination criterion (rule for fix) is inspired by type-based termination (Barthe et al., 2004; Abel and Pientka, 2013; Abel, 2012, 2004, 2008, 2007). Such work also typically uses two different kinds of recursion, one for induction and one for coinduction. In type-based termination, instead of requiring that a measure on the arguments of recursive calls decreases, we require that recursive functions are called at a type which is strictly smaller than the type of the caller. Our fix operator produces a term with a forall type, which is similar to the implicit function type of the implicit calculus of constructions (Miquel, 2001). Our termination measure on types can then be understood as a measure on the implicit argument of a function with an implicit function type. Earlier work on type-based termination checking includes simpler type systems such as DML (Xi, 2001).

A proof of concept of extension of Dotty compiler by a restricted set of (mostly numerical) refinement predicates was presented in (Schmid and Kunčak, 2016), without soundness proof. Developments specific to Scala include dependent object types (Amin, 2016) which focus on path dependency instead of predicate refinement and, by design, admit possibly non-terminating programs. System FR does not attempt to support records, let alone path dependency. Stainless relies on Scala compiler front ends to obtain a symbol-resolved syntax tree. For example, implicit parameters in Scala (Odersky et al., 2018) become ordinary explicit parameters by the time Stainless processes them. Conversely, many of the types we define in System FR do not have their counterparts in Scala. An upcoming PhD thesis of Nicolas Voirol (Voirol, 2019) presents a system related to System FR that more closely follows the expressive power of Inox solver on which Stainless relies.

9. Conclusion

We have presented System FR, a formalized type system and a bidirectional type checking algorithm that can serve as a basis of a verifier for higher-order functional programs. We were able to verify correctness and safety of a wide range of benchmarks amounting to 14k lines of code and proofs. Our formalization suggests that lazy data structures and non-covariant recursion are tractable and that explicit indices required in the general framework can be eliminated in commonly occurring cases. Our type system incorporates $\Pi$ and $\Sigma$ types, yet it also supports their variants ($\forall$ and $\exists$) that correspond to infinite intersections and unions. Along with support for singleton types and refinements, we obtained a rich framework to approximate program semantics, which can also help further type, invariant, and measure inference algorithms. Our experience confirms an advantage of the semantic-based soundness proof: once we adopt an approach of interpreting types as sets of terms, we are less dependent on a particular choice of syntactic rules; we can introduce new classes of types and new rules for verification condition generation and solving, as long as we can justify them semantically. When viewing types in our system as propositions, we obtain an expressive quantified logic. We have proven the soundness of this logic in Coq using countable interpretation of ground System FR types. The success in verification of our benchmarks suggests that the rules of System FR work well for many properties of functional programs. Furthermore, refinement by type along with intersections and unions (Section 6.1) allows System FR to describe types whose interpretations are undecidable countable sets from higher levels of arithmetical hierarchy.

ACKNOWLEDGMENTS

Work supported in part by Swiss National Science Foundation project 200021_175676 “Scaling Predicate Types”. We thank Ravichandhran Kandhadai Madhavan for numerous discussions about termination for higher-order functional programs; Romain Ruetschi for his valuable contributions to Stainless implementation; Paolo G. Giarrusso for interesting discussions and very relevant pointers on type theory; Andreas Abel for explaining us how to mix induction and co-induction in Agda. Thanks to Yoan Géran who implemented another prototype of our algorithm, found formalization discrepancies and proposed improvements to the typing rules.

Appendix A Lexicographic Orderings

Functions whose termination arguments require lexicographic orderings can be encoded by using two levels of recursions, which is a known technique that shows expressive power of System T (Girard, 1990, Section 7.3.2). The right-hand-side uses (twice) the syntactic sugar defined in Figure 17 and described in the previous section. The outermost recursion allows recursive calls whenever the first measure decreases, while the innermost one is used when the first measure stays the same and the second measure decreases.

For the encoding, we assume that in the body of function f (i.e. in the expression $E$), f is always applied to some argument. The notation

[TABLE]

represents the term where that every application of the form f $z$ in $E$ is replaced by the corresponding if  then  else  expression. This expression checks at runtime which measure decreases, and decides to call the outermost or innermost recursion. When the user knows which measure decreases for a given recursive call, the if  then  else  expression can be optimized away by directly calling the appropriate branch. We give as an example the Ackermann function (see Figure 26), which uses the lexicographic ordering of its argument for ensuring termination.

Appendix B Strict Positivity of a Type Variable in a Type

A type variable $\alpha$ is said to be strictly positive (see Figure 27) in a type $\tau$, if it only appears to the right-hand-sides of $\Pi$ and $\forall$ types. This restriction is used in the additional typing rules that are given in Section 5.5.

Appendix C Erasure of Type Annotations in Terms

In Section 5.1, we use the notation ${\sf erase}({t})$ to refer to the erasure of an annotated term $t$. The precise definition is given in Figure 28. Type annotations are used to guide our type-checking algorithm but play no role in the reducibility definition or in the operational semantics, which talk about erased terms with no annotation.

Appendix D Proof of Lemma 4.2

See 4.2

Proof.

Given a list of the form ${\tt fold}({{\tt right}({a_{1},\dots\tt fold({{\tt right}({a_{k},{\tt fold}({{\tt left}({})})})})\dots})})$, we say that $k$ is its size.

($\Leftarrow$) We prove by induction on (the size of) $n\in\llbracket{\sf Nat}\rrbracket_{\textsf{v}}$ that $\llbracket{\tt List}_{n}[{\tt X}]\rrbracket_{\textsf{v}}$ contains all finite lists. Then we can conclude that $\llbracket{\tt List}\rrbracket_{\textsf{v}}$ contains all finite lists.

• •

$(n={\tt zero})$. By definition, $\llbracket{\tt List}_{0}[{\tt X}]\rrbracket_{\textsf{v}}$ contains all values of the form ${\tt fold}({v})$, and therefore all finite lists.

• •

$(n={\tt succ}({n^{\prime}}))$. The induction hypothesis tells us that $\llbracket{\tt List}_{n^{\prime}}[{\tt X}]\rrbracket_{\textsf{v}}$ contains all finite lists. Consider a list $v\in{\sf Val}$, $k\geq 0$ and $a_{1},\dots,a_{k}\in\llbracket\tt X\rrbracket_{\textsf{v}}$ such that:

[TABLE]

We distinguish two cases, if $k=0$, i.e. $v={\tt fold}({{\tt left}({})})$ is the empty list, then we conclude directly by definition of $\llbracket{\tt List}_{n}[{\tt X}]\rrbracket_{\textsf{v}}$ that $v\in\llbracket{\tt List}_{n}[{\tt X}]\rrbracket_{\textsf{v}}$.

If $k>0$, then $v={\tt fold}({{\tt right}({a_{1},\dots\tt fold({{\tt right}({a_{k},{\tt fold}({{\tt left}({})})})})\dots})})$. By definition of $\llbracket{\tt List}_{n}[{\tt X}]\rrbracket_{\textsf{v}}$, we know that $v\in\llbracket{\tt List}_{n}[{\tt X}]\rrbracket_{\textsf{v}}$ if and only if the tail of $v$ belongs to $\llbracket{\tt List}_{n^{\prime}}[{\tt X}]\rrbracket_{\textsf{v}}$, i.e. ${\tt fold}({{\tt right}({a_{2},\dots\tt fold({{\tt right}({a_{k},{\tt fold}({{\tt left}({})})})})\dots})})\in\llbracket{\tt List}_{n^{\prime}}[{\tt X}]\rrbracket_{\textsf{v}}$, which is true by induction hypothesis.

$(\Rightarrow$) In a first step, we prove by induction on (the size of) $n\in\llbracket{\sf Nat}\rrbracket_{\textsf{v}}$ the following statement ($\ast$): if $v\in\llbracket{\tt List}_{n}[{\tt X}]\rrbracket_{\textsf{v}}$, then either $v$ is a list of size at most $n-1$, or there exists $a_{1},\dots,a_{n}\in\llbracket\tt X\rrbracket_{\textsf{v}}$ and $b\in{\sf Val}$ such that $v={\tt fold}({{\tt right}({a_{1},\dots\tt fold({{\tt right}({a_{n},b})})\dots})})$.

We can then use this fact to prove that if $v\in\llbracket{\tt List}[{\tt X}]\rrbracket_{\textsf{v}}$, then $v$ is a finite list, as follows. By definition, we know that, for every $n\in\llbracket{\sf Nat}\rrbracket_{\textsf{v}}$, $v\in\llbracket{\tt List}_{n}[{\tt X}]\rrbracket_{\textsf{v}}$. The term $v$ is represented by a finite syntax tree, and therefore there exists an $n$ (e.g. the size of the syntax tree of $v$ plus one) such that $v$ cannot be of the form $v={\tt fold}({{\tt right}({a_{1},\dots\tt fold({{\tt right}({a_{n},b})})\dots})})$. By using ($\ast$), it follows that $v$ must be a list of size at most $n-1$.

Let us now proceed to the proof of ($\ast$):

• •

$(n={\tt zero})$ The statement holds since ${\tt List}_{0}[{\tt X}]$ represents the values of the form ${\tt fold}({v})$ where $v\in{\sf Val}$, and we can choose $b=v$.

• •

$(n={\tt succ}({n^{\prime}}))$ By definition of $\llbracket{\tt List}_{n}[{\tt X}]\rrbracket_{\textsf{v}}$, we know that either $v={\tt fold}({{\tt left}({})})$ is the empty list, or there exists $a\in\llbracket\tt X\rrbracket_{\textsf{v}}$ and $v^{\prime}\in\llbracket{\tt List}_{n^{\prime}}[{\tt X}]\rrbracket_{\textsf{v}}$ such that $v={\tt fold}({{\tt right}({a,v^{\prime}})})$. By induction hypothesis, we know that $v^{\prime}$ is either a list of size at most $n^{\prime}-1$ or there exists $a_{1},\dots,a_{n^{\prime}}\in\llbracket\tt X\rrbracket_{\textsf{v}}$ and $b\in{\sf Val}$ such that $v^{\prime}={\tt fold}({{\tt right}({a_{1},\dots\tt fold({{\tt right}({a_{n^{\prime}},b})})\dots})})$.

We therefore conclude that $v$ is either a list of size at most $n-1$, or that:

[TABLE]

∎

Appendix E Operations on Natural Numbers

Figure 29 shows the definitions of lessThan, lessEqual, and equalNat that implement comparison and equality on the ${\sf Nat}$ type.