Related papers: Definitions by rewriting in the Calculus of Constr…
The Normalization transformation plays a key role in the compilation of Diderot programs. The transformations are complicated and it would be easy for a bug to go undetected. To increase our confidence in normalization part of the compiler…
In this paper, we present a general realizability semantics for the simply typed $\lambda\mu$-calculus. Then, based on this semantics, we derive both weak and strong normalization results for two versions of the $\lambda\mu$-calculus…
We present the formalization of a theory of syntax with bindings that has been developed and refined over the last decade to support several large formalization efforts. Terms are defined for an arbitrary number of constructors of varying…
Diagram chasing is not an easy task. The coherence holds in a generalized sense if we have a mechanical method to judge whether given two morphisms are equal to each other. A simple way to this end is to reform a concerned category into a…
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…
We start in this work the study of the relation between the theory of regularity structures and paracontrolled calculus. We give a paracontrolled representation of the reconstruction operator and provide a natural parametrization of the…
This paper develops an algorithmic-based approach for proving inductive properties of propositional sequent systems such as admissibility, invertibility, cut-elimination, and identity expansion. Although undecidable in general, these…
This paper addresses the problem of creating simplifiers for logic formulas based on conditional term rewriting. In particular, the paper focuses on a program synthesis application where formula simplifications have been shown to have a…
Recursive relational specifications are commonly used to describe the computational structure of formal systems. Recent research in proof theory has identified two features that facilitate direct, logic-based reasoning about such…
A theory is developed which uses "networks" (directed acyclic graphs with some extra structure) as a formalism for expressions in multilinear algebra. It is shown that this formalism is valid for arbitrary PROPs (short for 'PROducts and…
Rewriting systems are often defined as binary relations over a given set of objects. This simple definition is used to describe various properties of rewriting such as termination, confluence, normal forms etc. In this paper, we introduce a…
Rewriting logic is both a flexible semantic framework within which widely different concurrent systems can be naturally specified and a logical framework in which widely different logics can be specified. Maude programs are exactly rewrite…
Properties of the logical reloading in the Euclidean geometry are considered. The logical reloading is a logical operation which replaces one system of basic concepts of a conception by another system of basic concepts of the same…
We investigate here a new version of the Calculus of Inductive Constructions (CIC) on which the proof assistant Coq is based: the Calculus of Congruent Inductive Constructions, which truly extends CIC by building in arbitrary first-order…
A new understanding of the notion of regularizer is proposed. It is argued that this new notion is more realistic than the old one and better fits the practical computational needs. An example of the regularizer in the new sense is given. A…
We define a compilation scheme for a constructor-based, strongly-sequential, graph rewriting system which shortcuts some needed steps. The object code is another constructor-based graph rewriting system. This system is normalizing for the…
This paper shows how a recently developed view of typing as small-step abstract reduction, due to Kuan, MacQueen, and Findler, can be used to recast the development of simple type theory from a rewriting perspective. We show how standard…
Representation theorems for formal systems often take the form of an inductive translation that satisfies certain invariants, which are proved inductively. Theory morphisms and logical relations are common patterns of such inductive…
Cantor's ordinal numbers, a powerful extension of the natural numbers, are a cornerstone of set theory. They can be used to reason about the termination of processes, prove the consistency of logical systems, and justify some of the core…
Convergent rewriting systems on algebraic structures give methods to solve decision problems, to prove coherence results, and to compute homological invariants. These methods are based on higher-dimensional extensions of the critical…