Related papers: Formalizing Higher-Order Termination in Coq
We present an approach for representing abstract argumentation frameworks based on an encoding into classical higher-order logic. This provides a uniform framework for computer-assisted assessment of abstract argumentation frameworks using…
Dependently typed proof assistant rely crucially on definitional equality, which relates types and terms that are automatically identified in the underlying type theory. This paper extends type theory with definitional functor laws,…
The "Concrete Semantics" book gives an introduction to imperative programming languages accompanied by an Isabelle/HOL formalization. In this paper we discuss a re-formalization of the book using the Coq proof assistant. In order to achieve…
We have developed an alternative approach to teaching computer science students how to prove. First, students are taught how to prove theorems with the Coq proof assistant. In a second, more difficult, step students will transfer their…
If a code base is so big and complicated that complete mechanical verification is intractable, can we still apply and benefit from verification methods? We show that by allowing a deliberate mechanized formalization gap we can shrink and…
In this article we present a method for formally proving the correctness of the lazy algorithms for computing homographic and quadratic transformations -- of which field operations are special cases-- on a representation of real numbers by…
We introduce a formal framework for analyzing trades in financial markets. These days, all big exchanges use computer algorithms to match buy and sell requests and these algorithms must abide by certain regulatory guidelines. For example,…
In a previous work, the first author extended to higher-order rewriting and dependent types the use of size annotations in types, a termination proof technique called type or size based termination and initially developed for ML-like…
Many automatic theorem-provers rely on rewriting. Using theorems as rewrite rules helps to simplify the subgoals that arise during a proof. LCF is an interactive theorem-prover intended for reasoning about computation. Its implementation of…
The goal of this lecture is to show how modern theorem provers---in this case, the Coq proof assistant---can be used to mechanize the specification of programming languages and their semantics, and to reason over individual programs and…
Boyer and Moore have discussed a recursive function that puts conditional expressions into normal form [1]. It is difficult to prove that this function terminates on all inputs. Three termination proofs are compared: (1) using a measure…
Hammers are tools that provide general purpose automation for formal proof assistants. Despite the gaining popularity of the more advanced versions of type theory, there are no hammers for such systems. We present an extension of the…
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…
We present a new modular proof method of termination for second-order computation, and report its implementation SOL. The proof method is useful for proving termination of higher-order foundational calculi. To establish the method, we use a…
Termination is a major question in both logic and computer science. In logic, termination is at the heart of proof theory where it is usually called strong normalization (of cut elimination). In computer science, termination has always been…
Libraries of formalized mathematics use a possibly broad range of different representations for a same mathematical concept. Yet light to major manual input from users remains most often required for obtaining the corresponding variants of…
Completion is one of the most studied techniques in term rewriting and fundamental to automated reasoning with equalities. In this paper we present new correctness proofs of abstract completion, both for finite and infinite runs. For the…
Our approach to higher order Fourier analysis is to study the ultra product of finite (or compact) Abelian groups on which a new algebraic theory appears. This theory has consequences on finite (or compact) groups usually in the form of…
In this project, a rather complete proof-theoretical formalization of Lambek Calculus (non-associative with arbitrary extensions) has been ported from Coq proof assistent to HOL4 theorem prover, with some improvements and new theorems.…
Static analyzers based on abstract interpretation are complex pieces of software implementing delicate algorithms. Even if static analysis techniques are well understood, their implementation on real languages is still error-prone. This…