[Back to Ana Bove's page]

[main page | publications page | top]A Confluent Calculus of Macro Expansion and Evaluation

A. Bove and L. ArbillaSyntactic abbreviations or macros provide a powerful tool to increase the syntactic expressivity of programming languages. The expansion of these abbreviations can be modelled with substitutions. This paper presents an operational semantics of macro expansion and evaluation where the substitutions are handled explicitly. The semantics is defined in terms of a confluent, simple, and intuitive set of rewriting rules. The resulting semantics is also a basis for developing correct implementations.

[main page | publications page | top]A Machine-assisted Proof that Well Typed Expressions Cannot Go Wrong

A. BoveThis paper deals with the application of constructive type theory to the theory of programming languages. By constructive type theory we understand first and foremost Martin-Löf's theory of logical types. The main aim of this work is to investigate constructive formalisations of the mathematics of programs. Here, we consider a small typed functional language and prove some properties about it, arriving at the property that establishes that well typed (closed) expressions cannot go wrong. First, we give all the definitions and proofs in an informal style, and then we present and explain the formalisation of these definitions and proofs. For the formalisation, we use the proof editor ALF and its pattern matching facility.

[main page | publications page | top]Alpha Conversion in Simply Typed Lambda Calculus

A. Bove and P. SeveriIn the usual presentations of simply typed lambda-calculus, it is usual to identify terms that are alpha-convertible. However, this is not at all a practise in most (typed) functional languages, for which simply typed lambda-calculus is a theoretical foundation. Here, five well known variants of the type system for simply lambda-calculus which work with variable names are presented. Essentially, these formulations differ in the way variable declarations are handled and all of them are equivalent if alpha-convertible terms are identified. However, if alpha-convertible terms are not identified, some of the systems turn out to type less terms than the others. The main aim of this paper is to relate these systems by comparing their set of typable terms and study the property of closure under alpha-conversion for each system.

[main page | publications page | top]Simple General Recursion in Type Theory

A. BoveGeneral recursive algorithms are such that the recursive calls are performed on arguments satisfying no condition that guarantees termination. Hence, there is no direct way of formalising them in type theory.The standard way of handling general recursion in type theory uses a well-founded recursion principle. Unfortunately, this way of formalising general recursive algorithms often produces unnecessarily long and complicated codes. On the other hand, functional programming languages like Haskell impose no restrictions on recursive programs, and then writing general recursive algorithms is straightforward. In addition, functional programs are usually short and self-explanatory. However, the existing frameworks for reasoning about the correctness of Haskell-like programs are weaker than the framework provided by type theory.

The goal of this work is to present a method that combines the advantages of both programming styles when writing simple general recursive algorithms. The method introduced here separates the computational and logical parts of the definition of an algorithm, which has several advantages. First, the resulting type-theoretic algorithms are compact and easy to understand; they are as simple as their Haskell versions. Second, totality is now a separate task and hence, this method can also be used in the formalisation of partial functions. Third, the method presented here also simplifies the task of formal verification. Finally, it can easily be extended to treat nested and mutual recursion.

The main feature of the method is the introduction of an inductive predicate, specially defined for the algorithm to be formalised. This predicate can be thought of as characterising the set of inputs for which the algorithm terminates. It contains an introduction rule for each of the cases that need to be considered and provides an easy syntactic condition that guarantees the termination of the algorithm.

[main page | publications page | top]Nested General Recursion and Partiality in Type Theory

A. Bove and V. CaprettaWe extend Bove's technique for formalising simple general recursive algorithms in constructive type theory to nested recursive algorithms. The method consists in defining an inductive special purpose accessibility predicate, that characterizes the inputs on which the algorithm terminates. As a result, the type-theoretic version of the algorithm can be defined by structural recursion on the proof that the input values satisfy this predicate. This technique results in definitions in which the computational and logical parts are clearly separated; hence, the type-theoretic version of the algorithm is given by its purely functional content, similarly to the corresponding program in a functional programming language. In the case of nested recursion, the special predicate and the type-theoretic algorithm must be defined simultaneously, because they depend on each other. This kind of definitions is not allowed in ordinary type theory, but it is provided in type theories extended with Dybjer's schema for simultaneous inductive-recursive definitions. The technique applies also to the formalisation of partial functions as proper type-theoretic functions, rather than relations representing their graphs.

[main page | publications page | top]Mutual General Recursion in Type Theory

A. BoveWe show how the methodology presented by Bove for the formalisation of simple general recursive algorithms and extended by Bove and Capretta to treat nested recursion can also be used in the formalisation of mutual general recursive algorithms. The methodology consists of defining special-purpose accessibility predicates that characterise the inputs on which the algorithms terminate. Each algorithm is then formalised in type theory by structural recursion on the proof that its input satisfies the corresponding special-purpose accessibility predicate. When the mutually recursive algorithms are also nested, we make use of a generalisation of Dybjer's schema for simultaneous inductive-recursive definitions, which we also present in this work. Hence, some of the formalisations we present in this work are not allowed in ordinary type theory, but they can be carried out in type theories extended with such a schema. Similarly to what happens for simple and nested recursive algorithms, this methodology results in definitions in which the computational and logical parts are clearly separated also when the algorithms are mutually recursive. Hence, the type-theoretic version of the algorithms is given by its purely functional content, similarly to the corresponding program in a functional programming language.

[main page | publications page | top]Generalised Simultaneous Inductive-Recursive Definitions and their Application to Programming in Type Theory

A. BoveIn this work we present a generalisation of Dybjer's schema for simultaneous inductive-recursive definitions for the cases where we have several mutually recursive predicates defined simultaneously with several functions which, in turn, are defined by recursion on those predicates. As an application, we can use the methodology developed by Bove and Capretta for formalising general recursive algorithms to define nested and mutually recursive algorithms in type theories extended with the generalised schema we present in this work. Hence, the resulting definitions are such that the computational and logical parts are clearly separated. Moreover, the type-theoretic version of the algorithms is given by its purely functional content, similarly to the corresponding program in a functional programming language.

[main page | publications page | top]General Recursion in Type Theory

A. BoveIn this work, a method to formalise general recursive algorithms in constructive type theory is presented throughout examples. The method separates the computational and logical parts of the definitions. As a consequence, the resulting type-theoretic algorithms are clear, compact and easy to understand. They are as simple as their equivalents in a functional programming language, where there is no restriction on recursive calls. Given a general recursive algorithm, the method consists in defining an inductive special-purpose accessibility predicate that characterises the inputs on which the algorithm terminates. The type-theoretic version of the algorithm can then be defined by structural recursion on the proof that the input values satisfy this predicate. When formalising nested algorithms, the special-purpose accessibility predicate and the type-theoretic version of the algorithm must be defined simultaneously because they depend on each other. Since the method separates the computational part from the logical part of a definition, formalising partial functions becomes also possible

[main page | publications page | top]Formalising Bitonic Sort using Dependent Types

A. BoveWe present a complete formalisation of bitonic sort and its correctness proof in constructive type theory. Bitonic sort is one of the fastest sorting algorithms where the sequence of comparisons is not data-dependent. In addition, it is a general recursive algorithm that works on sequences of length 2^n. In the formalisation we face two main problems: only structural recursion is allowed in type theory, and a formal proof of the correctness of the algorithm needs to consider quite a number of cases. We define the bitonic sort algorithm over dependently-typed binary trees with information in the leaves. In proving that the algorithm sorts its input we make use of the 0-1-principle. To support the use of that principle we also prove a parametricity theorem derived from the type of our bitonic sort from which the 0-1-principle can be proved.

[main page | publications page | top]Formalising Bitonic Sort in Type Theory

A. Bove and T. CoquandWe discuss two complete formalisations of bitonic sort in constructive type theory. Bitonic sort is one of the fastest sorting algorithms where the sequence of comparisons is not data-dependent. In addition, it is a general recursive algorithm. In the formalisation we face two main problems: only structural recursion is allowed in type theory, and a formal proof of the correctness of the algorithm needs to consider quite a number of cases. In our first formalisation we define bitonic sort over dependently-typed binary trees with information in the leaves and we make use of the 0-1-principle to prove that the algorithm sorts inputs of arbitrary types. In our second formalisation we use notions from linear orders, lattice theory and monoids. The correctness proof is directly performed for any ordered set and not only for Boolean values.

[main page | publications page | top]Modelling General Recursion in Type Theory

A. Bove and V. CaprettaConstructive type theory is an expressive programming language where both algorithms and proofs can be represented. A limitation of constructive type theory as a programming language is that only terminating programs can be defined in it. Hence, general recursive algorithms have no direct formalisation in type theory since they contain recursive calls that satisfy no syntactic condition guaranteeing termination. In this work, we present a method to formalise general recursive algorithms in type theory. Given a general recursive algorithm, our method consists in defining an inductive special-purpose accessibility predicate that characterises the inputs on which the algorithm terminates. The type-theoretic version of the algorithm is then defined by structural recursion on the proof that the input values satisfy this predicate. The method separates the computational and logical parts of the definitions and thus the resulting type-theoretic algorithms are clear, compact, and easy to understand. They are as simple as their equivalents in a functional programming language, where there is no restriction on recursive calls. Here, we give a formal definition of the method and discuss its power and its limitations.

[main page | publications page | top]Recursive Functions with Higher Order Domains

A. Bove and V. CaprettaIn a series of articles, we developed a method to translate general recursive functions written in a functional programming style into constructive type theory. Three problems remained: the method could not properly deal with functions taking functional arguments, the translation of terms containing lambda-abstractions was too strict, and partial application of general recursive functions was not allowed. Here, we show how the three problems can be solved by defining a type of partial functions between given types. Every function, including arguments to higher order functions, lambda-abstractions and partially applied functions, is then translated as a pair consisting of a domain predicate and a function dependent on the predicate. Higher order functions are assigned domain predicates that inherit termination conditions from their functional arguments. The translation of a lambda-abstraction} does not need to be total anymore, but generates a local termination condition. The domain predicate of a partially applied function is defined by fixing the given arguments in the domain of the original function. As in our previous articles, simultaneous induction-recursion is required to deal with nested recursive functions. Since by using our method the inductive definition of the domain predicate can refer globally to the domain predicate itself, here we need to work on an impredicative type theory for the method to apply to all functions. However, in most practical cases the method can be adapted to work on a predicative type theory with type universes.

[main page | publications page | top]Verifying Haskell Programs Using Constructive Type Theory

A. Abel, M. Benke, A. Bove, J. Hughes and U. NorellProof assistants based on dependent type theory are closely related to functional programming languages, and so it is tempting to use them to prove the correctness of functional programs. In this paper, we show how Agda, such a proof assistant, can be used to prove theorems about Haskell programs. Haskell programs are translated into an Agda model of their semantics, by translating via GHC's Core language into a monadic form specially adapted to represent Haskell's polymorphism in Agda's predicative type system. The translation can support reasoning about either total values only, or total and partial values, by instantiating the monad appropriately. We claim that, although these Agda models are generated by a relatively complex translation process, proofs about them are simple and natural, and we offer a number of examples to support this claim.

[main page | publications page | top]Computation by Prophecy

A. Bove and V. CaprettaWe describe a new method to represent (partial) recursive functions in type theory. For every recursive definition, we define a co-inductive type ofpropheciesthat characterises the traces of the computation of the function. The structure of a prophecy is a possibly infinite tree, which is coerced by linearisation to a type of partial results defined by applying the delay monad to the co-domain of the function. Using induction on a weight relation defined on the prophecies, we can reason about them and prove that the formal type-theoretic version of the recursive function, resulting from the present method, satisfies the recursive equations of the original function. The advantages of this technique over the method previously developed by the authors via a special-purpose accessibility (domain) predicate are: there is no need of extra logical arguments in the definition of the recursive function; the function can be applied to any element in its domain, regardless of termination properties; we obtain a type of partial recursive functions between any two given types; and composition of recursive functions can be easily defined.

[main page | publications page | top]A Type of Partial Recursive Functions

A. Bove and V. CaprettaOur goal is to define a type of partial recursive functions in constructive type theory. In a series of previous articles, we studied two different formulations of partial functions and general recursion. We could obtain a type only by extending the theory with either an impredicative universe or with coinductive definitions. Here we present a new type constructor that eludes such entities of dubious constructive credentials.We start by showing how to break down a recursive function definition into three components: the first component generates the arguments of the recursive calls, the second evaluates them, and the last computes the output from the results of the recursive calls. We use this dissection as the basis for the introduction rule of the new type constructor.

Every partial recursive function is associated with an inductive domain predicate; evaluation of the function requires a proof that the input values satisfy the predicate.

We give a constructive justification for the new construct by interpreting it into the base type theory. This shows that the extended theory is consistent and constructive.

[main page | publications page | top]Depedent Types at Work

A. Bove and P. DybjerIn these lecture notes we give an introduction to functional programming with dependent types. We use the dependently typed programming language Agda which is an extension of Martin-Löf type theory. First we show how to do simply typed functional programming in the style of Haskell and ML. Some differences between Agda's type system and the Hindley-Milner type system of Haskell and ML are also discussed. Then we show how to use dependent types for programming and we explain the basic ideas behind type-checking dependent types. We go on to explain the Curry-Howard identification of propositions and types. This is what makes Agda a programming logic and not only a programming language. According to Curry-Howard, we identify programs and proofs, something which is possible only by requiring that all program terminate. However, at the end of these notes we present a method for encoding partial and general recursive functions as total functions using dependent types.

[main page | publications page | top]Embedding a Logical Theory of Constructions in Agda

A. Bove, P. Dybjer and A. Sicard-RamírezWe propose a new way to reason about general recursive functional programs in the dependently typed programming language Agda, which is based on Martin-Löf's intuitionistic type theory. We show how to embed an external programming logic, Aczel's Logical Theory of Constructions (LTC) inside Agda. To this end we postulate the existence of a domain of untyped functional programs and the conversion rules for these programs. Furthermore, we represent the inductive notions in LTC (intuitionistic predicate logic with equality, and totality predicates) as inductive notions in Agda. To illustrate our approach we specify an LTC-style logic for PCF, and show how to prove the termination and correctness of a general recursive algorithm for computing the greatest common divisor of two numbers.

[main page | publications page | top]Another Look at Function Domains

A. BoveBove and Capretta have presented a method to deal with partial and general recursive functions in constructive type theory which relies on an inductive characterisation of the domains of the functions. The method separates the logical and the computational aspects of an algorithm, and facilitates the formal verification of the functions being defined. For nested recursive functions, the method uses Dybjer' schema for simultaneous inductive-recursive definitions. However, not all constructive type theories support this kind of definitions.Here we present a new approach for dealing with partial and general recursive functions that preserves the advantages of the method by Bove and Capretta, but which does not rely on inductive-recursive definitions. In this approach, we start by inductively defining the graph of the function, from which we \emph{first} define the domain and \emph{afterwards} the type-theoretic version of the function. We show two ways of proving the formal specification of the functions defined with this new approach: by induction on the graph, or by using an induction principle in the style of the induction principle associated to the domain predicates of the Bove-Capretta method.

[main page | publications page | top]A Brief Overview of Agda -- A Functional Language with Dependent Types

A. Bove, P. Dybjer and U. NorellWe give an overview of Agda, the latest in a series of dependently typed programming languages developed in Gothenburg. Agda is based on Martin-Löf's intuitionistic type theory but extends it with numerous programming language features. It supports a wide range of inductive data types, including inductive families and inductive-recursive types, with associated flexible pattern-matching. Unlike other proof assistants, Agda is not tactic-based. Instead it has an Emacs-based interface which allows programming by gradual refinement of incomplete type-correct terms.

[main page | publications page | top]Combining Interactive and Automatic Reasoning about Functional Programs

A. Bove, P. Dybjer and A. Sicard-RamírezWe propose a new approach to the computer-assisted verification of functional programs. We work in first order theories of functional programs which are obtained by extending Aczel's first order theory of combinatory formal arithmetic with positive inductive and coinductive predicates. Rather than building a special purpose system we implement our theories in Agda, a proof assistant for dependent type theory which can be used as a generic theorem prover. Agda provides support for interactive reasoning by encoding first order theories using the formulae-as-types principle. Further support is provided by off-the-shelf automatic theorem provers for first order logic which can be called by a program which translates Agda representations of first order formulae into the TPTP language understood by the provers. We show some examples where we combine interactive and automatic reasoning, covering both proof by induction and coinduction.

[main page | publications page | top]Partiality and Recursion in Interactive Theorem Provers --- An Overview

A. Bove, A. Krauss, and M. SozeauThe use of interactive theorem provers to establish the correctness of critical parts of a software development or for formalising mathematics is becoming more common and feasible in practice. However, most mature theorem provers lack a direct treatment of partial and general recursive functions; overcoming this weakness has been the objective of intensive research during the last decades.In this article, we review several techniques that have been proposed in the literature to simplify the formalisation of partial and general recursive functions in interactive theorem provers.

Moreover, we classify the techniques according to their theoretical basis and their practical use. This uniform presentation of the different techniques facilitates the comparison and highlights their commonalities and differences, as well as their relative advantages and limitations.

We focus on theorem provers based on constructive type theory (in particular, Agda and Coq) and higher-order logic (in particular Isabelle/HOL). Other systems and logics are covered to a certain extent, but not exhaustively.

In addition to the description of the techniques, we also demonstrate tools which facilitate working with the problematic functions in particular theorem provers.

[main page | publications page | top]Principles of Alpha-Induction and Recursion for the Lambda Calculus in Constructive Type Theory

E. Copello, A. Tasistro, N Szasz, A. Bove and M. FernándezWe formulate principles of induction and recursion for a variant of lambda calculus in its original syntax (i.e., with only one sort of names) where α-conversion is based upon name swapping as in nominal abstract syntax. The principles allow to work modulo α-conversion and implement the Barendregt variable convention. We derive them all from the simple structural induction principle on concrete terms and work out applications to some fundamental meta-theoretical results, such as the substitution lemma for α-conversion and the lemma on substitution composition. The whole work is implemented in Agda.

Last modified: Tue Dec 8 16:15:28 CET 2015