SU\G(𝔸)/K·U
Sign Up for free Log In

Formalizing Higher-Order Termination in Coq

Authors

Deivid Vale, Niels van der Weide
Type: Preprint
Publication Date: 2021-01-01
Citations: 0
DOI: https://doi.org/10.48550/arxiv.2112.05715

Abstract

We describe a formalization of higher-order rewriting theory and formally prove that an AFS is strongly normalizing if it can be interpreted in a well-founded domain. To do so, we use Coq, which is a proof assistant based on dependent type theory. Using this formalization, one can implement several termination techniques, like the interpretation method or dependency pairs, and prove their correctness. Those implementations can then be extracted to OCaml, which results in a verified termination checker.

Locations

  • arXiv (Cornell University)
    View
  • DataCite API
    View

Ask a Question About This Paper

Summary

Login to see paper summary

Certifying Higher-Order Polynomial Interpretations

2023-01-01
Niels van der Weide , Deivid Vale , Cynthia Kop
Higher-order rewriting is a framework in which one can write higher-order programs and study their properties. One such property is termination: the situation that for all inputs, the program eventually … Higher-order rewriting is a framework in which one can write higher-order programs and study their properties. One such property is termination: the situation that for all inputs, the program eventually halts its execution and produces an output. Several tools have been developed to check whether higher-order rewriting systems are terminating. However, developing such tools is difficult and can be error-prone. In this paper, we present a way of certifying termination proofs of higher-order term rewriting systems. We formalize a specific method, namely the polynomial interpretation method, that is used to prove termination. In addition, we give a program that turns the output of Wanda, a termination analysis tool for higher-order rewriting systems, into a Coq script, so that we can check whether the output is a valid proof of termination.

Certifying Higher-Order Polynomial Interpretations

2023-02-23
Niels van der Weide , Deivid Vale , Cynthia Kop
Higher-order rewriting is a framework in which one can write higher-order programs and study their properties. One such property is termination: the situation that for all inputs, the program eventually … Higher-order rewriting is a framework in which one can write higher-order programs and study their properties. One such property is termination: the situation that for all inputs, the program eventually halts its execution and produces an output. Several tools have been developed to check whether higher-order rewriting systems are terminating. However, developing such tools is difficult and can be error-prone. In this paper, we present a way of certifying termination proofs of higher-order term rewriting systems. We formalize a specific method, namely the polynomial interpretation method, that is used to prove termination. In addition, we give a program that turns the output of Wanda, a termination analysis tool for higher-order rewriting systems, into a Coq script, so that we can check whether the output is a valid proof of termination.
View PDF Chat

Strong Normalization for the Calculus of Constructions

2022-01-01
Chris Casinghino
The calculus of constructions (CC) is a core theory for dependently typed programming and higher-order constructive logic. Originally introduced in Coquand's 1985 thesis, CC has inspired 25 years of research … The calculus of constructions (CC) is a core theory for dependently typed programming and higher-order constructive logic. Originally introduced in Coquand's 1985 thesis, CC has inspired 25 years of research in programming languages and type theory. Today, extensions of CC form the basis of languages like Coq and Agda. This survey reviews three proofs of CC's strong normalization property (the fact that there are no infinite reduction sequences from well-typed expressions). It highlights the similarities in the structure of the proofs while showing how their differences are motivated by the varying goals of their authors.
View PDF Chat

Termination and Confluence of Higher-Order Rewrite Systems

2000-01-01
Frédéric Blanqui
View PDF Chat

A higher-order implementation of rewriting

1983-08-01
Lawrence C. Paulson
View PDF Chat

General Automation in Coq through Modular Transformations

2021-07-04
Valentin Blot , Louise Dubois de Prisque , Chantal Keller +1 more
Whereas proof assistants based on Higher-Order Logic benefit from external solvers' automation, those based on Type Theory resist automation and thus require more expertise. Indeed, the latter use a more … Whereas proof assistants based on Higher-Order Logic benefit from external solvers' automation, those based on Type Theory resist automation and thus require more expertise. Indeed, the latter use a more expressive logic which is further away from first-order logic, the logic of most automatic theorem provers. In this article, we develop a methodology to transform a subset of Coq goals into first-order statements that can be automatically discharged by automatic provers. The general idea is to write modular, pairwise independent transformations and combine them. Each of these eliminates a specific aspect of Coq logic towards first-order logic. As a proof of concept, we apply this methodology to a set of simple but crucial transformations which extend the local context with proven first-order assertions that make Coq definitions and algebraic types explicit. They allow users of Coq to solve non-trivial goals automatically. This methodology paves the way towards the definition and combination of more complex transformations, making Coq more accessible.
View PDF Chat

General Automation in Coq through Modular Transformations

2021-07-11
Valentin Blot , Louise Dubois de Prisque , Chantal Keller +1 more
Whereas proof assistants based on Higher-Order Logic benefit from external solvers' automation, those based on Type Theory resist automation and thus require more expertise. Indeed, the latter use a more … Whereas proof assistants based on Higher-Order Logic benefit from external solvers' automation, those based on Type Theory resist automation and thus require more expertise. Indeed, the latter use a more expressive logic which is further away from first-order logic, the logic of most automatic theorem provers. In this article, we develop a methodology to transform a subset of Coq goals into first-order statements that can be automatically discharged by automatic provers. The general idea is to write modular, pairwise independent transformations and combine them. Each of these eliminates a specific aspect of Coq logic towards first-order logic. As a proof of concept, we apply this methodology to a set of simple but crucial transformations which extend the local context with proven first-order assertions that make Coq definitions and algebraic types explicit. They allow users of Coq to solve non-trivial goals automatically. This methodology paves the way towards the definition and combination of more complex transformations, making Coq more accessible.
View PDF Chat

A certifying extraction with time bounds from Coq to call-by-value $\lambda$-calculus

2019-04-26
Yannick Forster , Fabian Kunze
We provide a plugin extracting Coq functions of simple polymorphic types to the (untyped) call-by-value $\lambda$-calculus L. The plugin is implemented in the MetaCoq framework and entirely written in Coq. … We provide a plugin extracting Coq functions of simple polymorphic types to the (untyped) call-by-value $\lambda$-calculus L. The plugin is implemented in the MetaCoq framework and entirely written in Coq. We provide Ltac tactics to automatically verify the extracted terms w.r.t a logical relation connecting Coq functions with correct extractions and time bounds, essentially performing a certifying translation and running time validation. We provide three case studies: A universal L-term obtained as extraction from the Coq definition of a step-indexed self-interpreter for Ł, a many-reduction from solvability of Diophantine equations to the halting problem of L, and a polynomial-time simulation of Turing machines in L.

A certifying extraction with time bounds from Coq to call-by-value $λ$-calculus

2019-01-01
Yannick Forster , Fabian Kunze
We provide a plugin extracting Coq functions of simple polymorphic types to the (untyped) call-by-value $λ$-calculus L. The plugin is implemented in the MetaCoq framework and entirely written in Coq. … We provide a plugin extracting Coq functions of simple polymorphic types to the (untyped) call-by-value $λ$-calculus L. The plugin is implemented in the MetaCoq framework and entirely written in Coq. We provide Ltac tactics to automatically verify the extracted terms w.r.t a logical relation connecting Coq functions with correct extractions and time bounds, essentially performing a certifying translation and running time validation. We provide three case studies: A universal L-term obtained as extraction from the Coq definition of a step-indexed self-interpreter for Ł, a many-reduction from solvability of Diophantine equations to the halting problem of L, and a polynomial-time simulation of Turing machines in L.
View PDF Chat

Extending Nunchaku to Dependent Type Theory

2016-06-17
Simon Cruanes , Jasmin Christian Blanchette
Nunchaku is a new higher-order counterexample generator based on a sequence of transformations from polymorphic higher-order logic to first-order logic. Unlike its predecessor Nitpick for Isabelle, it is designed as … Nunchaku is a new higher-order counterexample generator based on a sequence of transformations from polymorphic higher-order logic to first-order logic. Unlike its predecessor Nitpick for Isabelle, it is designed as a stand-alone tool, with frontends for various proof assistants. In this short paper, we present some ideas to extend Nunchaku with partial support for dependent types and type classes, to make frontends for Coq and other systems based on dependent type theory more useful.
View PDF Chat

Modular Denotational Semantics for Effects with Guarded Interaction Trees

2024-01-05
Dan Frumin , Amin Timany , Lars Birkedal
We present guarded interaction trees — a structure and a fully formalized framework for representing higher-order computations with higher-order effects in Coq, inspired by domain theory and the recently proposed … We present guarded interaction trees — a structure and a fully formalized framework for representing higher-order computations with higher-order effects in Coq, inspired by domain theory and the recently proposed interaction trees. We also present an accompanying separation logic for reasoning about guarded interaction trees. To demonstrate that guarded interaction trees provide a convenient domain for interpreting higher-order languages with effects, we define an interpretation of a PCF-like language with effects and show that this interpretation is sound and computationally adequate; we prove the latter using a logical relation defined using the separation logic. Guarded interaction trees also allow us to combine different effects and reason about them modularly. To illustrate this point, we give a modular proof of type soundness of cross-language interactions for safe interoperability of different higher-order languages with different effects. All results in the paper are formalized in Coq using the Iris logic over guarded type theory.
View PDF Chat

Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order (Long Version)

2015-01-01
Martin Avanzini , Ugo Dal Lago , Georg Moser
We show how the complexity of higher-order functional programs can be analysed automatically by applying program transformations to a defunctionalized versions of them, and feeding the result to existing tools … We show how the complexity of higher-order functional programs can be analysed automatically by applying program transformations to a defunctionalized versions of them, and feeding the result to existing tools for the complexity analysis of first-order term rewrite systems. This is done while carefully analysing complexity preservation and reflection of the employed transformations such that the complexity of the obtained term rewrite system reflects on the complexity of the initial program. Further, we describe suitable strategies for the application of the studied transformations and provide ample experimental data for assessing the viability of our method.

A certifying extraction with time bounds from Coq to call-by-value $\lambda$-calculus

2019-04-26
Yannick Forster , Fabian Kunze
We provide a plugin extracting Coq functions of simple polymorphic types to the (untyped) call-by-value $\lambda$-calculus L. The plugin is implemented in the MetaCoq framework and entirely written in Coq. … We provide a plugin extracting Coq functions of simple polymorphic types to the (untyped) call-by-value $\lambda$-calculus L. The plugin is implemented in the MetaCoq framework and entirely written in Coq. We provide Ltac tactics to automatically verify the extracted terms w.r.t a logical relation connecting Coq functions with correct extractions and time bounds, essentially performing a certifying translation and running time validation. We provide three case studies: A universal L-term obtained as extraction from the Coq definition of a step-indexed self-interpreter for \L, a many-reduction from solvability of Diophantine equations to the halting problem of L, and a polynomial-time simulation of Turing machines in L.
View PDF Chat

Modular Denotational Semantics for Effects with Guarded Interaction Trees

2023-01-01
Dan Frumin , Amin Timany , Lars Birkedal
We present guarded interaction trees -- a structure and a fully formalized framework for representing higher-order computations with higher-order effects in Coq, inspired by domain theory and the recently proposed … We present guarded interaction trees -- a structure and a fully formalized framework for representing higher-order computations with higher-order effects in Coq, inspired by domain theory and the recently proposed interaction trees. We also present an accompanying separation logic for reasoning about guarded interaction trees. To demonstrate that guarded interaction trees provide a convenient domain for interpreting higher-order languages with effects, we define an interpretation of a PCF-like language with effects and show that this interpretation is sound and computationally adequate; we prove the latter using a logical relation defined using the separation logic. Guarded interaction trees also allow us to combine different effects and reason about them modularly. To illustrate this point, we give a modular proof of type soundness of cross-language interactions for safe interoperability of different higher-order languages with different effects. All results in the paper are formalized in Coq using the Iris logic over guarded type theory.

Polynomial Interpretations for Higher-Order Rewriting

2012-03-26
Carsten Fuhs , Cynthia Kop
The termination method of weakly monotonic algebras, which has been defined for higher-order rewriting in the HRS formalism, offers a lot of power, but has seen little use in recent … The termination method of weakly monotonic algebras, which has been defined for higher-order rewriting in the HRS formalism, offers a lot of power, but has seen little use in recent years. We adapt and extend this method to the alternative formalism of algebraic functional systems, where the simply-typed lambda-calculus is combined with algebraic reduction. Using this theory, we define higher-order polynomial interpretations, and show how the implementation challenges of this technique can be tackled. A full implementation is provided in the termination tool WANDA.

Polynomial Interpretations for Higher-Order Rewriting

2012-01-01
Carsten Fuhs , Cynthia Kop
The termination method of weakly monotonic algebras, which has been defined for higher-order rewriting in the HRS formalism, offers a lot of power, but has seen little use in recent … The termination method of weakly monotonic algebras, which has been defined for higher-order rewriting in the HRS formalism, offers a lot of power, but has seen little use in recent years. We adapt and extend this method to the alternative formalism of algebraic functional systems, where the simply-typed lambda-calculus is combined with algebraic reduction. Using this theory, we define higher-order polynomial interpretations, and show how the implementation challenges of this technique can be tackled. A full implementation is provided in the termination tool WANDA.
View PDF Chat

A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems

2004-01-01
Frédéric Blanqui
View PDF Chat

Initial Semantics for higher-order typed syntax in Coq

2010-01-01
Benedikt Ahrens , Julianna Zsidó
Initial Semantics aims at characterizing the syntax associated to a signature as the initial object of some category. We present an initial semantics result for typed higher-order syntax together with … Initial Semantics aims at characterizing the syntax associated to a signature as the initial object of some category. We present an initial semantics result for typed higher-order syntax together with its formalization in the Coq proof assistant. The main theorem was first proved on paper in the second author's PhD thesis in 2010, and verified formally shortly afterwards. To a simply-typed binding signature S over a fixed set T of object types we associate a category called the category of representations of S. We show that this category has an initial object Sigma(S). From its construction it will be clear that the object Sigma(S) merits the name abstract syntax associated to S. Our theorem is implemented and proved correct in the proof assistant Coq through heavy use of dependent types. The approach through monads gives rise to an implementation of syntax where both terms and variables are intrinsically typed, i.e. where the object types are reflected in the meta-level types. This article is to be seen as a research article rather than about the formalization of a classical mathematical result. The nature of our theorem - involving lengthy, technical proofs and complicated algebraic structures - makes it particularly interesting for formal verification. Our goal is to promote the use of computer theorem provers as research tools, and, accordingly, a new way of publishing mathematical results: a parallel description of a theorem and its formalization should allow the verification of correct transcription of definitions and statements into the proof assistant, and straightforward but technical proofs should be well-hidden in a digital library. We argue that Coq's rich type theory, combined with its various features such as implicit arguments, allows a particularly readable formalization and is hence well-suited for communicating mathematics.
View PDF Chat

A Deductive Verification Framework For Higher Order Programs

2020-01-01
Tiago Lopes Soares
In this report, we present the preliminary work developed for our research project for the APDC (\'Area Pr\'atica de Desenvolvimento Curricular) course. The main goal of this project is to … In this report, we present the preliminary work developed for our research project for the APDC (\'Area Pr\'atica de Desenvolvimento Curricular) course. The main goal of this project is to develop a framework, on top of the Why3 tool, for the verification of effectful higher-order programs. We use defunctionalization as an intermediate transformation from higher-order OCaml implementations into first order ones. The target for our translation is WhyML, the Why3's programming language. We believe defunctionalization can be an interesting route for the automated verification of higher-order programs, since one can employ off-the-shelf automated program verifiers to prove the correctness of the generated first-order program. This report also serves to introduce the reader to the subject of deductive program verification and some of the tools and concepts used to prove higher order effectful programs.
View PDF Chat

Higher-Order LCTRSs and Their Termination

2023-01-01
Liye Guo , Cynthia Kop
Logically constrained term rewriting systems (LCTRSs) are a program analyzing formalism with native support for data types which are not (co)inductively defined. As a first-order formalism, LCTRSs have accommodated only … Logically constrained term rewriting systems (LCTRSs) are a program analyzing formalism with native support for data types which are not (co)inductively defined. As a first-order formalism, LCTRSs have accommodated only analysis of imperative programs so far. In this paper, we present a higher-order variant of the LCTRS formalism, which can be used to analyze functional programs. Then we study the termination problem and define a higher-order recursive path ordering (HORPO) for this new formalism.
View PDF Chat