Related papers: (HO)RPO Revisited
Primitive recursion is a mature, well-understood topic in the theory and practice of programming. Yet its dual, primitive corecursion, is underappreciated and still seen as exotic. We aim to put them both on equal footing by giving a…
Proof search has been used to specify a wide range of computation systems. In order to build a framework for reasoning about such specifications, we make use of a sequent calculus involving induction and co-induction. These proof principles…
We introduce a variation on Barthe et al.'s higher-order logic in which formulas are interpreted as predicates over open rather than closed objects. This way, concepts which have an intrinsically functional nature, like continuity,…
We consider different classes of combinatory structures related to Krivine realizability. We show, in the precise sense that they give rise to the same class of triposes, that they are equivalent for the purpose of modeling higher-order…
We develop synthetic notions of oracle computability and Turing reducibility in the Calculus of Inductive Constructions (CIC), the constructive type theory underlying the Coq proof assistant. As usual in synthetic approaches, we employ a…
Relational program verification is a variant of program verification where one can reason about two programs and as a special case about two executions of a single program on different inputs. Relational program verification can be used for…
To enable the study of open sets in computational approaches to mathematics, lots of extra data and structure on these sets is assumed. For both foundational and mathematical reasons, it is then a natural question, and the subject of this…
For which sets A does there exist a mapping, computed by a total or partial recursive function, such that the mapping, when its domain is restricted to A, is a 1-to-1, onto mapping to $\Sigma^*$? And for which sets A does there exist such a…
We study the computability-theoretic complexity and proof-theoretic strength of the following statements: (1) "If X is a well-ordering, then so is epsilon_X", and (2) "If X is a well-ordering, then so is phi(alpha,X)", where alpha is a…
We present an extension to the $\mathtt{mathlib}$ library of the Lean theorem prover formalizing the foundations of computability theory. We use primitive recursive functions and partial recursive functions as the main objects of study, and…
A well-established approach to reasoning about loops during program analysis is to capture the effect of a loop by extracting recurrences from the loop; these express relationships between the values of variables, or program properties such…
This paper discusses the method of formative rules for first-order term rewriting, which was previously defined for a higher-order setting. Dual to the well-known usable rules, formative rules allow dropping some of the term constraints…
Logical relations are one of the most powerful techniques in the theory of programming languages, and have been used extensively for proving properties of a variety of higher-order calculi. However, there are properties that cannot be…
We model collapsible and ordered pushdown systems with term rewriting, by encoding higher-order stacks and multiple stacks into trees. We show a uniform inverse preservation of recognizability result for the resulting class of term…
Higher-order constructs extend the expressiveness of first-order (Constraint) Logic Programming ((C)LP) both syntactically and semantically. At the same time assertions have been in use for some time in (C)LP systems helping programmers…
In deduction modulo, a theory is not represented by a set of axioms but by a congruence on propositions modulo which the inference rules of standard deductive systems---such as for instance natural deduction---are applied. Therefore, the…
In this paper, we explain how the connection between higher-order model-checking and linear logic recently exhibited by the authors leads to a new and conceptually enlightening proof of the selection problem originally established by…
First-order probabilistic models combine representational power of first-order logic with graphical models. There is an ongoing effort to design lifted inference algorithms for first-order probabilistic models. We analyze lifted inference…
In this article we define a new reducibility based on the enumeration orders of r.e. sets.
The notion of computable reducibility between equivalence relations on the natural numbers provides a natural computable analogue of Borel reducibility. We investigate the computable reducibility hierarchy, comparing and contrasting it with…