at is, to investigate the production of verified implementations of programming languages. Writin... more at is, to investigate the production of verified implementations of programming languages. Writing programs in constructive type theory amounts to writing completely formal proofs of often complex theorems. This makes the practical applicability of type theory depends strongly on the availability of adequate programming environments (alias proof assistants). A number of these systems have been or are being developed. We expect our work to become a useful experience in this connection too. In the present work, we conduct a first experiment along the lines given above. We consider a small polymorphic functional language and write a formal proof in constructive type theory of the main property relating the type system of the language with the evaluation of its expressions, namely the Subject Reduction Property. We use the proof assistant ALF ([Alt 94]). The abstract syntax of the language considered is the following : e ::= x j x : e<F
General recursive algorithms are such that the recursive calls are performed on arguments satisfy... more General 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....
We propose a new way to reason about general recursive functional programs in the dependently typ... more We 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 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.
We formulate principles of induction and recursion for a variant of lambda calculus in its origin... more We 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 alpha-conversion is based upon name swapping as in nominal abstract syntax. The principles allow to work modulo alpha-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 alpha-conversion and the lemma on substitution composition. The whole work is implemented in Agda.
We present a complete formalisation of bitonic sort and its correctness proof in constructive typ... more We 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.
Abstract. Our goal is to define a type of partial recursive functions in constructive type theory... more Abstract. Our 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 justifica...
In these lecture notes we give an introduction to functional programming with dependent types. We... more In 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.
We formulate principles of induction and recursion for a variant of lambda calculus in its origin... more We formulate principles of induction and recursion for a variant of lambda calculus in its original syntax (i.e., with only one sort of names for both bound and free variables) in which -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 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.
... The al-gorithms rev and rev2 are nested and mutually recursive. ... Our special accessibility... more ... The al-gorithms rev and rev2 are nested and mutually recursive. ... Our special accessibility predicate gives, in their sense, the view of a function's domain which allows the machine to check the recursive calls of the function without further notational overhead. ...
at is, to investigate the production of verified implementations of programming languages. Writin... more at is, to investigate the production of verified implementations of programming languages. Writing programs in constructive type theory amounts to writing completely formal proofs of often complex theorems. This makes the practical applicability of type theory depends strongly on the availability of adequate programming environments (alias proof assistants). A number of these systems have been or are being developed. We expect our work to become a useful experience in this connection too. In the present work, we conduct a first experiment along the lines given above. We consider a small polymorphic functional language and write a formal proof in constructive type theory of the main property relating the type system of the language with the evaluation of its expressions, namely the Subject Reduction Property. We use the proof assistant ALF ([Alt 94]). The abstract syntax of the language considered is the following : e ::= x j x : e<F
General recursive algorithms are such that the recursive calls are performed on arguments satisfy... more General 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....
We propose a new way to reason about general recursive functional programs in the dependently typ... more We 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 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.
We formulate principles of induction and recursion for a variant of lambda calculus in its origin... more We 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 alpha-conversion is based upon name swapping as in nominal abstract syntax. The principles allow to work modulo alpha-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 alpha-conversion and the lemma on substitution composition. The whole work is implemented in Agda.
We present a complete formalisation of bitonic sort and its correctness proof in constructive typ... more We 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.
Abstract. Our goal is to define a type of partial recursive functions in constructive type theory... more Abstract. Our 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 justifica...
In these lecture notes we give an introduction to functional programming with dependent types. We... more In 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.
We formulate principles of induction and recursion for a variant of lambda calculus in its origin... more We formulate principles of induction and recursion for a variant of lambda calculus in its original syntax (i.e., with only one sort of names for both bound and free variables) in which -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 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.
... The al-gorithms rev and rev2 are nested and mutually recursive. ... Our special accessibility... more ... The al-gorithms rev and rev2 are nested and mutually recursive. ... Our special accessibility predicate gives, in their sense, the view of a function's domain which allows the machine to check the recursive calls of the function without further notational overhead. ...
Uploads
Papers by Ana Bove