Under consideration for publication in Math. Struct. in Comp. Science Partiality and Recursion in Interactive Theorem Provers — An Overview
---
paper_title: Notions of computation and monads

paper_content:

Abstract The λ-calculus is considered a useful mathematical tool in the study of programming languages, since programs can be identified with λ-terms. However, if one goes further and uses βη-conversion to prove equivalence of programs, then a gross simplification is introduced (programs are identified with total functions from values to values ) that may jeopardise the applicability of theoretical results. In this paper we introduce calculi, based on a categorical semantics for computations , that provide a correct basis for proving equivalence of programs for a wide range of notions of computation .
---
paper_title: An Introduction to Inductive Definitions

paper_content:

Publisher Summary Inductive definitions of sets are often informally presented by giving some rules for generating elements of the set and then adding that an object is to be in the set only if it has been generated according to the rules. An equivalent formulation is to characterize the set as the smallest set closed under the rules. This chapter discusses monotone induction and its role in extensions of recursion theory. The chapter reviews some of the work on non-monotone induction and outlines the separate motivation that has led to its development. The chapter briefly considers inductive definitions in a more general context.
---
paper_title: A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory

paper_content:

The first example of a simultaneous inductive-recursive definition in intuitionistic type theory is Martin-LUf's universe a la Tarski. A set Uo of codes for small sets is generated inductively at the same time as a function To, which maps a code to the corresponding small set, is defined by recursion on the way the elements of Uo are generated. In this paper we argue that there is an underlying general notion of simultaneous inductive-recursive definition which is implicit in Martin-LUf's intuitionistic type theory. We extend previously given schematic formulations of inductive definitions in type theory to encompass a general notion of simultaneous inductionrecursion. This enables us to give a unified treatment of several interesting constructions including various universe constructions by Palmgren, Griffor, Rathjen, and Setzer and a constructive version of Aczel's Frege structures. Consistency of a restricted version of the extension is shown by constructing a realisability model in the style of Allen. ?
---
paper_title: Towards a practical programming language based on dependent type theory

paper_content:

Dependent type theories have a long history of being used for theorem proving. One aspect of type theory which makes it very powerful as a proof language is that it mixes deduction with computation. This also makes type theory a good candidate for programming---the strength of the type system allows properties of programs to be stated and established, and the computational properties provide semantics for the programs. ::: ::: This thesis is concerned with bridging the gap between the theoretical presentations of type theory and the requirements on a practical programming language. Although there are many challenging research problems left to solve before we have an industrial scale programming language based on type theory, this thesis takes us a good step along the way.
---
paper_title: Dependent Type Theory with Parameterized First-Order Data Types and Well-Founded Recursion

paper_content:

We present a variation of Martin-Lof's logical framework with "beta-iota-equality", extended with first-order parameterized algebraic data types and recursive pattern-matching definitions. Our contribution is a proof of normalization for the proposed system, from which we obtain decidable type-correctness. Our result holds under the assumption that the call relation of the recursive definitions is well-founded. ::: ::: ::: Recursive definitions can be read as intuitive specifications, which makes it easier to understand their intended meaning, compared to definitions that use only pre-defined recursion operators, called elimination rules in type theory. Pattern-matching definitions can be seen as the underlying mechanism with which we describe elimination rules. The arguments used to justify recursively defined elimination rules are essentially the same as those justifying pattern-matching definitions. The use of pattern-matching takes the proof system closer to the look and feel of a programming language like Haskell or ML. ::: ::: ::: We use the "Size-Change Principle for Program Termination" (C.S. Lee, N.D. Jones, A. Ben-Amram 2001) to establish that the recursive definitions have a well-founded call relation. The size-change criterion subsumes many known characterizations of terminating recursions, including primitive recursion and lexicographical ordering, but it also deals transparently with permuted arguments and mutual recursion. When instantiating the size-change relation for this criterion to be constructor decomposition, it corresponds closely to what we could call well-founded structural recursion.
---
paper_title: Code generation via higher-order rewrite systems

paper_content:

We present the meta-theory behind the code generation facilities of Isabelle/HOL. To bridge the gap between the source (higher-order logic with type classes) and the many possible targets (functional programming languages), we introduce an intermediate language, Mini-Haskell. To relate the source and the intermediate language, both are given a semantics in terms of higher-order rewrite systems (HRSs). In a second step, type classes are removed from Mini-Haskell programs by means of a dictionary translation; we prove the correctness of this step. Building on equational logic also directly supports a simple but powerful algorithm and data refinement concept.
---
paper_title: Introduction to HOL: a theorem proving environment for higher order logic

paper_content:

Part I. Tutorial: 1. Introduction to ML 2. The HOL logic 3. Introduction to proof with HOL 4. Goal-oriented proof: tactics and tacticals 5. Example: a simple parity checker 6. How to program a proof tool 7. Example: the binomial theorem Part II. The Meta-Language ML: 8. The history of ML 9. Introduction and examples 10. Syntax of ML 11. Semantics of ML 12. ML types 13. Primitive ML identifier bindings 14. General purpose and list processing functions 15. ML system functions Part III. The Hol Logic: 16. Syntax and semantics 17. Theories Part IV. The Hol System: 18. The HOL logic in ML Part V. Theorem-Proving With HOL: 19. Derived inference rules 20. Conversions 21. Goal-directed proof: tactics and tacticals Appendices.
---
paper_title: The Isabelle Framework

paper_content:

Isabelle, which is available from http://isabelle.in.tum.de , is a generic framework for interactive theorem proving. The Isabelle/Puremeta-logic allows the formalization of the syntax and inference rules of a broad range of object-logics following the general idea of natural deduction [32,33]. The logical core is implemented according to the well-known "LCF approach" of secure inferences as abstract datatype constructors in ML [16]; explicit proof terms are also available [8]. Isabelle/Isarprovides sophisticated extra-logical infrastructure supporting structured proofs and specifications, including concepts for modular theory development. Isabelle/HOLis a large application within the generic framework, with plenty of logic-specific add-on tools and a large theory library. Other notable object-logics are Isabelle/ZF(Zermelo-Fraenkel set-theory, see [34,36] and Isabelle/HOLCF[26] (Scott's domain theory within HOL). Users can build further formal-methods tools on top, e.g. see [53].
---
paper_title: Inductive Datatypes in HOL - Lessons Learned in Formal-Logic Engineering

paper_content:

Isabelle/HOL has recently acquired new versions of Definitional packages for inductive datatypes and primitive recursive functions. In contrast to its predecessors and most other implementations, Isabelle/HOL datatypes may be mutually and indirect recursive, even infinitely branching. We also support inverted datatype definitions for characterizing existing types as being inductive ones later. All our constructions are fully Definitional according to established HOL tradition. Stepping back from the logical details, we also see this work as a typical example of what could be called "Formal-Logic Engineering". We observe that building realistic theorem proving environments involves further issues rather than pure logic only.
---
paper_title: A predicative analysis of structural recursion

paper_content:

We introduce a language based upon lambda calculus with products, coproducts and strictly positive inductive types that allows the definition of recursive terms. We present the implementation (foetus) of a syntactical check that ensures that all such terms are structurally recursive, i.e. recursive calls appear only with arguments structurally smaller than the input parameters of terms considered. To ensure the correctness of the termination checker, we show that all structurally recursive terms are normalizing with respect to a given operational semantics. To this end, we define a semantics on all types and a structural ordering on the values in this semantics and prove that all values are accessible with regard to this ordering. Finally, we point out how to do this proof predicatively using set based operators.
---
paper_title: Decidability of type-checking in the calculus of algebraic constructions with size annotations

paper_content:

Since Val Tannen's pioneering work on the combination of simply-typed λ-calculus and first-order rewriting [11], many authors have contributed to this subject by extending it to richer typed λ-calculi and rewriting paradigms, culminating in the Calculus of Algebraic Constructions. These works provide theoretical foundations for type-theoretic proof assistants where functions and predicates are defined by oriented higher-order equations. This kind of definitions subsumes usual inductive definitions, is easier to write and provides more automation. ::: ::: On the other hand, checking that such user-defined rewrite rules, when combined with β-reduction, are strongly normalizing and confluent, and preserve the decidability of type-checking, is more difficult. Most termination criteria rely on the term structure. In a previous work, we extended to dependent types and higher-order rewriting, the notion of “sized types” studied by several authors in the simpler framework of ML-like languages, and proved that it preserves strong normalization. ::: ::: The main contribution of the present paper is twofold. First, we prove that, in the Calculus of Algebraic Constructions with size annotations, the problems of type inference and type-checking are decidable, provided that the sets of constraints generated by size annotations are satisfiable and admit most general solutions. Second, we prove the latter properties for a size algebra rich enough for capturing usual induction-based definitions and much more.
---
paper_title: A Tutorial on Type-Based Termination

paper_content:

Type-based termination is a method to enforce termination of recursive definitions through a non-standard type system that introduces a notion of size for inhabitants of inductively defined types. The purpose of this tutorial is to provide a gentle introduction to a polymorphically typed ?-calculus with type-based termination, and to the size inference algorithm which is used to guarantee automatically termination of recursive definitions.
---
paper_title: Dependent types for program termination verification

paper_content:

Program termination verification is a challenging research subject of significant practical importance. While there is already a rich body of literature on this subject, it is still undeniably a difficult task to design a termination checker for a realistic programming language that supports general recursion. In this paper, we present an approach to program termination verification that makes use of a form of dependent types developed in Dependent ML (DML), demonstrating a novel application of such dependent types to establishing a liveness property. We design a type system that enables the programmer to supply metrics for verifying program termination and prove that every well-typed program in this type system is terminating. We also provide realistic examples, which are all verified in a prototype implementation, to support the effectiveness of our approach to program termination verification as well as its unobtrusiveness to programming. The main contribution of the paper lies in the design of an approach to program termination verification that smoothly combines types with metrics, yielding a type system capable of guaranteeing program termination that supports a general form of recursion (including mutual recursion), higher-order functions, algebraic data types and polymorphism.
---
paper_title: Semi-continuous sized types and termination

paper_content:

A type-based approach to termination uses sized types: an ordinal bound for the size of a data structure is stored in its type. A recursive function over a sized type is accepted if it is visible in the type system that recursive calls occur just at a smaller size. This approach is only sound if the type of the recursive function is admissible, i.e., depends on the size index in a certain way. To explore the space of admissible functions in the presence of higher-kinded data types and impredicative polymorphism, a semantics is developed where sized types are interpreted as functions from ordinals into sets of strongly normalizing terms. It is shown that upper semi-continuity of such functions is a sufficient semantical criterion for admissibility. To provide a syntactical criterion, a calculus for semi-continuous function is developed.
---
paper_title: Type-based termination of recursive definitions

paper_content:

This paper introduces $\lambda^\widehat$, a simply typed lambda calculus supporting inductive types and recursive function definitions with termination ensured by types. The system is shown to enjoy subject reduction, strong normalisation of typable terms and to be stronger than a related system $\lambda_{\mathcal{G}}$ in which termination is ensured by a syntactic guard condition. The system can, at will, be extended to support coinductive types and corecursive function definitions also.
---
paper_title: Type-Based Termination with Sized Products

paper_content:

Type-based termination is a semantically intuitive method that ensures termination of recursive definitions by tracking the size of datatype elements, and by checking that recursive calls operate on smaller arguments. However, many systems using type-based termination rely on a semantical anomaly to guarantee strong normalization; namely, they impose that non-recursive elements of a datatype, e.g. the empty list, have size 1 instead of 0. This semantical anomaly also prevents functions such as quicksort to be given a precise typing. ::: ::: The main contribution of this paper is a type system that remedies this anomaly, and still ensures termination. In addition, our type system features prenex stage polymorphism, a weakening of existential quantification over stages, and is precise enough to type quicksort as a non-size increasing function. Moreover, our system accomodate stage addition with all positive inductive types.
---
paper_title: CIC : Type-based termination of recursive definitions in the calculus of inductive constructions

paper_content:

Sized types provides a type-based mechanism to enforce termination of recursive definitions in typed A-calculi. Previous work has provided strong indications that type-based termination provides an appropriate foundation for proof assistants based on type theory; however, most work to date has been confined to non-dependent type systems. In this article, we introduce a variant of the Calculus of Inductive Constructions with sized types and study its meta theoretical properties: subject reduction, normalization, and thus consistency and decidability of type-checking and of size-inference. A prototype implementation has been developed alongside case studies.
---
paper_title: A logic covering undefinedness in program proofs

paper_content:

Recursive definition often results in partial functions; iteration gives rise to programs which may fail to terminate for some imputs. Proofs about such functions or programs should be conducted in logical systems which reflect the possibility of "undefined values". This paper provides an axiomatization of such a logic together with examples of its use.
---
paper_title: A simple type theory with partial functions and subtypes

paper_content:

Farmer, W.M., A simple type theory with partial functions and subtypes, Annals of Pure and Applied Logic 64 (1993) 21 l-240. Simple type theory is a higher-order predicate logic for reasoning about truth values, individuals, and simply typed total functions. We present in this paper a version of simple type theory, called PF*, in which functions may be partial and types may have subtypes. We define both a Henkin-style general models semantics and an axiomatic system for PF*, and we prove that the axiomatic system is complete with respect to the general models semantics. We also define a notion of an interpretation of one PF* theory in another. PF* is intended as a foundation for mechanized mathematics. It is the basis for the logic of IMPS, an Interactive Mathematical Proof System developed at The MITRE Corporation.
---
paper_title: Systematic software development using VDM

paper_content:

Logic of propositions reasoning about predicates functions and operations set notation composite objects and invariants map notation sequence notation data rectification more on data types operation decomposition a small case study.
---
paper_title: Recursive Definitions in Type Theory

paper_content:

The type theories we consider are adequate for the foundations of mathematics and computer science. Recursive type definitions are important practical ways to organize data, and they express powerful axioms about the termination of procedures. In the theory examined here, the demands of practicality arising from our implemented system, Nuprl, suggest an approach to recursive types that significantly increases the proof theoretic power of the theory and leads to insights into computational semantics. We offer a new account of recursive definitions for both types and partial functions. The computational requirements of the theory restrict recursive type definitions involving the total function-space constructor ($\rightarrow$) to those with only positive occurrences of the defined type. But we show that arbitrary recursive definitions with respect to the partial function-space constructor are sensible. The partial function-space constructor allows us to express reflexive types of Scott''s domain theory (as needed to model the lambda calculus) and thereby reconcile parts of domain theory with constructive type theory.
---
paper_title: A Type of Partial Recursive Functions

paper_content:

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 justification for the new construct by interpreting it into the base type theory. This shows that the extended theory is consistent and constructive.
---
paper_title: An Introduction to Inductive Definitions

paper_content:

Publisher Summary Inductive definitions of sets are often informally presented by giving some rules for generating elements of the set and then adding that an object is to be in the set only if it has been generated according to the rules. An equivalent formulation is to characterize the set as the smallest set closed under the rules. This chapter discusses monotone induction and its role in extensions of recursion theory. The chapter reviews some of the work on non-monotone induction and outlines the separate motivation that has led to its development. The chapter briefly considers inductive definitions in a more general context.
---
paper_title: Inductive invariants for nested recursion

paper_content:

We show that certain input-output relations, termed inductive invariants are of central importance for termination proofs of algorithms defined by nested recursion. Inductive invariants can be used to enhance recursive function definition packages in higher-order logic mechanizations. We demonstrate the usefulness of inductive invariants on a large example of the BDD algorithm Apply. Finally, we introduce a related concept of inductive fixpoints with the property that for every functional in higher-order logic there exists a largest partial function that is such a fixpoint.
---
paper_title: Defining and reasoning about recursive functions: A practical tool for the Coq proof assistant

paper_content:

We present a practical tool for defining and proving properties of recursive functions in the Coq proof assistant. The tool generates from pseudo-code the graph of the intended function as an inductive relation. Then it proves that the relation actually represents a function, which is by construction the function that we are trying to define. Then, we generate induction and inversion principles, and a fixpoint equation for proving other properties of the function. Our tool builds upon state-of-the-art techniques for defining recursive functions, and can also be used to generate executable functions from inductive descriptions of their graph. We illustrate the benefits of our tool on two case studies.
---
paper_title: Function Definition in Higher-Order Logic

paper_content:

We use a formally proven wellfounded recursion theorem as the basis upon which to build a function definition facility for Higher Order Logic. This approach offers flexibility in the choice of wellfounded relations used, the deferral of termination arguments, and automatic isolation of termination conditions. Building on this platform, we provide the ability to define recursive functions via pattern matching. The system is parameterized and has been instantiated to quite different theorem provers.
---
paper_title: Inductive Definitions: Automation and Application

paper_content:

This paper demonstrates the great practical utility of inductive definitions in HOL. We describe a new package we have implemented for automating inductive definitions, based on the Knaster-Tarski fixpoint theorem. As an example, we use it to give a simple proof of the well-founded recursion theorem. We then describe how to generate free recursive types starting just from the Axiom of Infinity. This contrasts with the existing HOL development where several specific free recursive types are developed first.
---
paper_title: Fix-point Equations for Well-Founded Recursion in Type Theory

paper_content:

Inductive type theories, as used in systems like Coq or Lego [11,14,4], provide a systematic approach to program recursive functions over inductive data-structures and to reason about these functions. Recursive computation is described by reduction rules, included in the type system under the name ι-reduction. If t is an element of a recursive type, f is a recursive function over that type and v is the value of f(t), then the equality f(t) = v is a simple tautology, because f(t) and v are equal modulo ι-reduction.
---
paper_title: First-order unification by structural recursion

paper_content:

First-order unification algorithms (Robinson, 1965) are traditionally implemented via general recursion, with separate proofs for partial correctness and termination. The latter tends to involve counting the number of unsolved variables and showing that this total decreases each time a substitution enlarges the terms. There are many such proofs in the literature (Manna & Waldinger, 1981; Paulson, 1985; Coen, 1992; Rouyer, 1992; Jaume, 1997; Bove, 1999). This paper shows how a dependent type can relate terms to the set of variables over which they are constructed. As a consequence, first-order unification becomes a structurally recursive program, and a termination proof is no longer required. Both the program and its correctness proof have been checked using the proof assistant LEGO (Luo & Pollack, 1992; McBride, 1999).
---
paper_title: Flyspeck I: Tame Graphs

paper_content:

We present a verified enumeration of tame graphs as defined in Hales' proof of the Kepler Conjecture and confirm the completeness of Hales' list of all tame graphs while reducing it from 5128 to 2771 graphs.
---
paper_title: Formal certification of a compiler back-end or: programming a compiler with a proof assistant

paper_content:

This paper reports on the development and formal certification (proof of semantic preservation) of a compiler from Cminor (a C-like imperative language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a certified compiler is useful in the context of formal methods applied to the certification of critical software: the certification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well.
---
paper_title: A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory

paper_content:

The first example of a simultaneous inductive-recursive definition in intuitionistic type theory is Martin-LUf's universe a la Tarski. A set Uo of codes for small sets is generated inductively at the same time as a function To, which maps a code to the corresponding small set, is defined by recursion on the way the elements of Uo are generated. In this paper we argue that there is an underlying general notion of simultaneous inductive-recursive definition which is implicit in Martin-LUf's intuitionistic type theory. We extend previously given schematic formulations of inductive definitions in type theory to encompass a general notion of simultaneous inductionrecursion. This enables us to give a unified treatment of several interesting constructions including various universe constructions by Palmgren, Griffor, Rathjen, and Setzer and a constructive version of Aczel's Frege structures. Consistency of a restricted version of the extension is shown by constructing a realisability model in the style of Allen. ?
---
paper_title: Type-theoretic functional semantics

paper_content:

We describe the operational and denotational semantics of a small imperative language in type theory with inductive and recursive definitions. The operational semantics is given by natural inference rules, implemented as an inductive relation. The realization of the denotational semantics is more delicate: The nature of the language imposes a few difficulties on us. First, the language is Turing-complete, and therefore the interpretation function we consider is necessarily partial. Second, the language contains strict sequential operators, and therefore the function necessarily exhibits nested recursion. Our solution combines and extends recent work by the authors and others on the treatment of general recursive functions and partial and nested recursive functions. The first new result is a technique to encode the approach of Bove and Capretta for partial and nested recursive functions in type theories that do not provide simultaneous induction-recursion. A second result is a clear understanding of the characterization of the definition domain for general recursive functions, a key aspect in the approach by iteration of Balaa and Bertot. In this respect, the work on operational semantics is a meaningful example, but the applicability of the technique should extend to other circumstances where complex recursive functions need to be described formally.
---
paper_title: Another Look at Function Domains

paper_content:

Bove 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 first define the domain and 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.
---
paper_title: Recursive functions with higher order domains

paper_content:

In 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 λ-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, λ-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 λ-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.
---
paper_title: Fix-point Equations for Well-Founded Recursion in Type Theory

paper_content:

Inductive type theories, as used in systems like Coq or Lego [11,14,4], provide a systematic approach to program recursive functions over inductive data-structures and to reason about these functions. Recursive computation is described by reduction rules, included in the type system under the name ι-reduction. If t is an element of a recursive type, f is a recursive function over that type and v is the value of f(t), then the equality f(t) = v is a simple tautology, because f(t) and v are equal modulo ι-reduction.
---
paper_title: Modelling general recursion in type theory

paper_content:

Constructive type theory is an expressive programming language in which 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 is to define 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.
---
paper_title: A data type of partial recursive functions in Martin-Löf Type Theory

paper_content:

In this article we revisit the approach by Bove and Capretta for formulating partial recursive functions in Martin-Lof Type Theory by indexed inductive-recursive definitions. We will show that all inductive-recursive definitions used there can be replaced by inductive definitions. However, this encoding results in an additional technical overhead. In order to obtain directly executable partial recursive functions, we introduce restrictions on the indexed inductive-recursive definitions used. Then we introduce a data type of partial recursive functions. This allows to define higher order partial recursive functions like the map functional, which depend on other partial recursive functions. This data type will be based on the closed formalisation of indexed inductive-recursive definitions introduced by Dybjer and the author. All elements of this data type will represent partial recursive functions, and the set of partial recursive functions will be closed under the standard operations for forming partial recursive functions, and under the total functions.
---
paper_title: Partial and Nested Recursive Function Definitions in Higher-order Logic

paper_content:

Based on inductive definitions, we develop a tool that automates the definition of partial recursive functions in higher-order logic (HOL) and provides appropriate proof rules for reasoning about them. Termination is modeled by an inductive domain predicate which follows the structure of the recursion. Since a partial induction rule is available immediately, partial correctness properties can be proved before termination is established. It turns out that this modularity also facilitates termination arguments for total functions, in particular for nested recursions. Our tool is implemented as a definitional package extending Isabelle/HOL. Various extensions provide convenience to the user: pattern matching, default values, tail recursion, mutual recursion and currying.
---
paper_title: Induction Proofs with Partial Functions

paper_content:

In this paper we present a method for automated induction proofs about partial functions. We show that most well-known techniques developed for (explicit) induction theorem proving are unsound when dealing with partial functions. But surprisingly, by slightly restricting the application of these techniques, it is possible to develop a calculus for automated induction proofs with partial functions. In particular, under certain conditions one may even generate induction schemes from the recursions of nonterminating algorithms. The need for such induction schemes and the power of our calculus have been demonstrated on a large collection of nontrivial theorems (including Knuth and Bendix's critical pair lemma). In this way, existing induction theorem provers can be directly extended to partial functions without major changes of their logical framework.
---
paper_title: Partial Functions in a Total Setting

paper_content:

We discuss a scheme for defining and reasoning about partial recursive functions within a classical two-valued logic in which all terms denote. We show how a total extension of the partial function introduced by a recursive declaration may be axiomatized within a classical logic, and illustrate by an example the kind of reasoning that our scheme supports. By presenting a naive set-theoretic semantics, we show that the system we propose is logically consistent. Our work is motivated largely by the pragmatic issues arising from mechanical theorem proving – we discuss some of the practical benefits and limitations of our scheme for mechanical verification of software and hardware systems.
---
paper_title: Partial recursive functions in higher-order logic

paper_content:

Based on inductive definitions, we develop an automated tool for defining partial recursive functions in Higher-Order Logic and providing appropriate reasoning tools for them. Our method expresses termination in a uniform manner and includes a very general form of pattern matching, where patterns can be arbitrary expressions. Termination proofs can be deferred, restricted to subsets of arguments and are interchangeable with other proofs about the function. We show that this approach can also facilitate termination arguments for total functions, in particular for nested recursions. We implemented our tool as a definitional specification mechanism for Isabelle/HOL.
---
paper_title: Termination of Nested and Mutually Recursive Algorithms

paper_content:

This paper deals with automated termination analysis for functional programs. Previously developed methods for automated termination proofs of functional programs often fail for algorithms with nested recursion and they cannot handle algorithms with mutual recursion.We show that termination proofs for nested and mutually recursive algorithms can be performed without having to prove the correctness of the algorithms simultaneously. Using this result, nested and mutually recursive algorithms do no longer constitute a special problem and the existing methods for automated termination analysis can be extended to nested and mutual recursion in a straightforward way. We give some examples of algorithms whose termination can now be proved automatically (including well-known challenge problems such as McCarthy’s f_91 function).
---
paper_title: Assuming termination

paper_content:

A requirement for the admission of a recursive function definition in ACL2 is a proof that the recursion terminates. Establishing termination involves identifying a well-founded relation and an appropriate measure function that decreases according to the well-founded relation with each recursive call. Depending on the domain this process may prove difficult, unnecessary or even impossible. Manolios and Moore introduced a method for admitting tail-recursive function definitions that does not require the specification of a measure. Their method, however, does not produce an induction scheme. We present an extension of their method that enables the admission of arbitrary recursive function definitions and their associated induction schemes augmented with a termination check and justified by a partial measure. We demonstrate the use of this method by defining the tarai function and proving by induction its unwinding under the assumption that it terminates.
---
paper_title: A Purely Definitional Universal Domain

paper_content:

Existing theorem prover tools do not adequately support reasoning about general recursive datatypes. Better support for such datatypes would facilitate reasoning about a wide variety of real-world programs, including those written in continuation-passing style, that are beyond the scope of current tools. ::: ::: This paper introduces a new formalization of a universal domain that is suitable for modeling general recursive datatypes. The construction is purely definitional, introducing no new axioms. Defining recursive types in terms of this universal domain will allow a theorem prover to derive strong reasoning principles, with soundness ensured by construction.
---
paper_title: HOLCF: Higher Order Logic of Computable Functions

paper_content:

This paper presents a survey of HOLCF, a higher order logic of computable functions. The logic HOLCF is based on HOLC, a variant of the well known higher order logic HOL, which offers the additional concept of type classes.
---
paper_title: Recursive Definitions of Monadic Functions

paper_content:

Using standard domain-theoretic fixed-points, we present an approach for defining recursive functions that are formulated in monadic style. The method works both in the simple option monad and the state-exception monad of Isabelle/HOL's imperative programming extension, which results in a convenient definition principle for imperative programs, which were previously hard to define. ::: For such monadic functions, the recursion equation can always be derived without preconditions, even if the function is partial. The construction is easy to automate, and convenient induction principles can be derived automatically.
---
paper_title: Computation by prophecy

paper_content:

We describe a new method to represent (partial) recursive functions in type theory. For every recursive definition, we define a co-inductive type of prophecies that 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.
---
paper_title: General Recursion via Coinductive Types

paper_content:

A fertile field of research in theoretical computer science investigates the rep- resentation of general recursive functions in intensional type theories. Among the most successful approaches are: the use of wellfounded relations, implementation of operational semantics, formalization of domain theory, and inductive definition of domain predicates. Here, a different solution is proposed: exploiting coinductive types to model infinite com- putations. To every type A we associate a type of partial elements A � , coinductively generated by two constructors: the first, p aq just returns an element a: A; the second, ⊲ x, adds a computation step to a recursive element x: A � . We show how this simple device is sufficient to formalize all recursive functions between two given types. It allows the definition of fixed points of finitary, that is, continuous, operators. We will compare this approach to different ones from the literature. Finally, we mention that the formalization, with appropriate structural maps, defines a strong monad.
---
paper_title: Partial Functions in ACL2

paper_content:

We describe a method for introducing “partial functions” into ACL2, that is, functions not defined everywhere. The function “definitions” are actually admitted via the encapsulation principle: the new function symbol is constrained to satisfy the appropriate equation. This is permitted only when a witness function can be exhibited, establishing that the constraint is satisfiable. Of particular interest is the observation that every tail recursive definition can be witnessed in ACL2. We describe a macro that allows the convenient introduction of arbitrary tail recursive functions, and we discuss how such functions can be used to prove theorems about state machine models without reasoning about “clocks” or counting the number of steps until termination. Our macro for introducing “partial functions” also permits a variety of other recursive schemes, and we briefly illustrate some of them.
---
paper_title: Recursive Definitions of Monadic Functions

paper_content:

Using standard domain-theoretic fixed-points, we present an approach for defining recursive functions that are formulated in monadic style. The method works both in the simple option monad and the state-exception monad of Isabelle/HOL's imperative programming extension, which results in a convenient definition principle for imperative programs, which were previously hard to define. ::: For such monadic functions, the recursion equation can always be derived without preconditions, even if the function is partial. The construction is easy to automate, and convenient induction principles can be derived automatically.
---
paper_title: Efficient Reasoning about Executable Specifications in Coq

paper_content:

We describe a package to reason efficiently about executable specifications in Coq. The package provides a command for synthesizing a customized induction principle for a recursively defined function, and a tactic that combines the application of the customized induction principle with automatic rewriting. We further illustrate how the package leads to a drastic reduction (by a factor of 10 approximately) of the size of the proofs in a large-scale case study on reasoning about JavaCard.
---
paper_title: Defining and reasoning about recursive functions: A practical tool for the Coq proof assistant

paper_content:

We present a practical tool for defining and proving properties of recursive functions in the Coq proof assistant. The tool generates from pseudo-code the graph of the intended function as an inductive relation. Then it proves that the relation actually represents a function, which is by construction the function that we are trying to define. Then, we generate induction and inversion principles, and a fixpoint equation for proving other properties of the function. Our tool builds upon state-of-the-art techniques for defining recursive functions, and can also be used to generate executable functions from inductive descriptions of their graph. We illustrate the benefits of our tool on two case studies.
---
paper_title: Fix-point Equations for Well-Founded Recursion in Type Theory

paper_content:

Inductive type theories, as used in systems like Coq or Lego [11,14,4], provide a systematic approach to program recursive functions over inductive data-structures and to reason about these functions. Recursive computation is described by reduction rules, included in the type system under the name ι-reduction. If t is an element of a recursive type, f is a recursive function over that type and v is the value of f(t), then the equality f(t) = v is a simple tautology, because f(t) and v are equal modulo ι-reduction.
---
paper_title: Subset coercions in Coq

paper_content:

We propose a new language for writing programs with dependent types on top of the COQ proof assistant. This language permits to establish a phase distinction between writing and proving algorithms in the COQ environment. Concretely, this means allowing to write algorithms as easily as in a practical functional programming language whilst giving them as rich a specification as desired and proving that the code meets the specification using the whole COQ proof apparatus. This is achieved by extending conversion to an equivalence which relates types and subsets based on them, a technique originating from the "Predicate subtyping" feature of PVS and following mathematical convention. The typing judgements can be translated to the Calculus of (Co-)Inductive Constructions (CIC) by means of an interpretation which inserts coercions at the appropriate places. These coercions can contain existential variables representing the propositional parts of the final term, corresponding to proof obligations (or PVS type-checking conditions). A prototype implementation of this process is integrated with the COQ environment.
---
paper_title: The view from the left

paper_content:

Pattern matching has proved an extremely powerful and durable notion in functional programming. This paper contributes a new programming notation for type theory which elaborates the notion in various ways. First, as is by now quite well-known in the type theory community, definition by pattern matching becomes a more discriminating tool in the presence of dependent types, since it refines the explanation of types as well as values. This becomes all the more true in the presence of the rich class of datatypes known as inductive families (Dybjer, 1991). Secondly, as proposed by Peyton Jones (1997) for Haskell, and independently rediscovered by us, subsidiary case analyses on the results of intermediate computations, which commonly take place on the right-hand side of definitions by pattern matching, should rather be handled on the left. In simply-typed languages, this subsumes the trivial case of Boolean guards; in our setting it becomes yet more powerful. Thirdly, elementary pattern matching decompositions have a well-defined interface given by a dependent type; they correspond to the statement of an induction principle for the datatype. More general, user-definable decompositions may be defined which also have types of the same general form. Elementary pattern matching may therefore be recast in abstract form, with a semantics given by translation. Such abstract decompositions of data generalize Wadler's (1987) notion of ‘view’. The programmer wishing to introduce a new view of a type $\mathit{T}$, and exploit it directly in pattern matching, may do so via a standard programming idiom. The type theorist, looking through the Curry–Howard lens, may see this as proving a theorem, one which establishes the validity of a new induction principle for $\mathit{T}$. We develop enough syntax and semantics to account for this high-level style of programming in dependent type theory. We close with the development of a typechecker for the simply-typed lambda calculus, which furnishes a view of raw terms as either being well-typed, or containing an error. The implementation of this view is ipso facto a proof that typechecking is decidable.
---
paper_title: Equations: a dependent pattern-matching compiler

paper_content:

We present a compiler for definitions made by pattern matching on inductive families in the Coq system. It allows to write structured, recursive dependently-typed functions as a set of equations, automatically find their realization in the core type theory and generate proofs to ease reasoning on them. It provides a complete package to define and reason on functions in the proof assistant, substantially reducing the boilerplate code and proofs one usually has to write, also hiding the intricacies related to the use of dependent types and complex recursion schemes.
---
paper_title: Partial and Nested Recursive Function Definitions in Higher-order Logic

paper_content:

Based on inductive definitions, we develop a tool that automates the definition of partial recursive functions in higher-order logic (HOL) and provides appropriate proof rules for reasoning about them. Termination is modeled by an inductive domain predicate which follows the structure of the recursion. Since a partial induction rule is available immediately, partial correctness properties can be proved before termination is established. It turns out that this modularity also facilitates termination arguments for total functions, in particular for nested recursions. Our tool is implemented as a definitional package extending Isabelle/HOL. Various extensions provide convenience to the user: pattern matching, default values, tail recursion, mutual recursion and currying.
---
paper_title: Certified size-change termination

paper_content:

We develop a formalization of the Size-Change Principle in Isabelle/HOL and use it to construct formally certified termination proofs for recursive functions automatically.
---
paper_title: Partial recursive functions in higher-order logic

paper_content:

Based on inductive definitions, we develop an automated tool for defining partial recursive functions in Higher-Order Logic and providing appropriate reasoning tools for them. Our method expresses termination in a uniform manner and includes a very general form of pattern matching, where patterns can be arbitrary expressions. Termination proofs can be deferred, restricted to subsets of arguments and are interchangeable with other proofs about the function. We show that this approach can also facilitate termination arguments for total functions, in particular for nested recursions. We implemented our tool as a definitional specification mechanism for Isabelle/HOL.
---
paper_title: Finding lexicographic orders for termination proofs in Isabelle/HOL

paper_content:

We present a simple method to formally prove termination of recursive functions by searching for lexicographic combinations of size measures. Despite its simplicity, the method turns out to be powerful enough to solve a large majority of termination problems encountered in daily theorem proving practice.
---
paper_title: Adapting Functional Programs to Higher-Order Logic

paper_content:

Higher-order logic proof systems combine functional programming with logic, providing functional programmers with a comfortable setting for the formalization of programs, specifications, and proofs. However, a possibly unfamiliar aspect of working in such an environment is that formally establishing program termination is necessary. In many cases, termination can be automatically proved, but there are useful programs that diverge and others that always terminate but have difficult termination proofs. We discuss techniques that support the expression of such programs as logical functions.
---

Title: Partiality and Recursion in Interactive Theorem Provers — An Overview

Section 1: Introduction
Description 1: Introduce the topic focusing on the limitations of current proof assistants in handling partial functions and recursion.

Section 2: Scope of This Paper
Description 2: Discuss the scope of the work, including the specific logics and proof assistants covered, and any exclusions.

Section 3: Terminology and Notation
Description 3: Introduce the terminology and notation used throughout the paper to ease readability.

Section 4: Some Preliminary Notions
Description 4: Recall known concepts necessary for understanding the paper, such as the graph of a function, monads, and well-foundedness.

Section 5: Outline of the Paper
Description 5: Provide a detailed outline for the rest of the paper, summarizing the content of each major section.

Section 6: Running Examples
Description 6: Introduce a collection of running examples used throughout the paper to illustrate different forms of function definitions.

Section 7: Logical Foundations
Description 7: Introduce the logical foundations, including constructive type theory and higher-order logic, required for understanding the techniques presented.

Section 8: Axiomatic Techniques
Description 8: Discuss axiomatic techniques that extend or modify the logical foundation of the theory to handle partiality and general recursion.

Section 9: Definitional Techniques
Description 9: Present techniques that work within the existing logical framework without adding new axioms, using well-founded recursion to define general recursive functions.

Section 10: Tool Support
Description 10: Introduce tools implemented on top of Coq and Isabelle/HOL that simplify the formalization of partial and general recursive functions in proof assistants.

Section 11: Conclusions
Description 11: Summarize the findings, discuss the effectiveness of different techniques, and mention open challenges and future directions.