Related papers: Specifying programs with propositions and with con…
SOFT ('Second-Order Functions and Theorems') is a tool to mimic second-order functions and theorems in the first-order logic of ACL2. Second-order functions are mimicked by first-order functions that reference explicitly designated…
We present polygraphic programs, a subclass of Albert Burroni's polygraphs, as a computational model, showing how these objects can be seen as first-order functional programs. We prove that the model is Turing complete. We use polygraphic…
A central topic in mathematical logic is the classification of theorems from mathematics in hierarchies according to their logical strength. Ideally, the place of a theorem in a hierarchy does not depend on the representation (aka coding)…
We investigate the power of non-determinism in purely functional programming languages with higher-order types. Specifically, we consider cons-free programs of varying data orders, equipped with explicit non-deterministic choice.…
The lambda-PRK-calculus is a typed lambda-calculus that exploits the duality between the notions of proof and refutation to provide a computational interpretation for classical propositional logic. In this work, we extend lambda-PRK to…
A class of models is presented, in the form of continuation monads polymorphic for first-order individuals, that is sound and complete for minimal intuitionistic predicate logic. The proofs of soundness and completeness are constructive and…
We pursue the question how integers can be ordered or partitioned according to their divisibility properties. Based on pseudometrics on $\mathbb{Z}$, we investigate induced preorders, associated equivalence relations, and quotient sets. The…
The sequential composition of propositional logic programs has been recently introduced. This paper studies the sequential {\em decomposition} of programs by studying Green's relations $\mathcal{L,R,J}$ -- well-known in semigroup theory --…
We analyze congruence classes of $S(n,k)$, the Stirling numbers of the second kind, modulo powers of 2. This analysis provides insight into a conjecture posed by Amdeberhan, Manna and Moll, which those authors established for $k\le5$. We…
The Curry-Howard correspondence is about a relationship between types and programs on the one hand and propositions and proofs on the other. The implications for programming language design and program verification is an active field of…
The Curry-Howard correspondence is often described as relating proofs (in intutionistic natural deduction) to programs (terms in simply-typed lambda calculus). However this narrative is hardly a perfect fit, due to the computational content…
Notions of k-asimulation and asimulation are introduced as asymmetric counterparts to k-bisimulation and bisimulation, respectively. It is proved that a first-order formula is equivalent to a standard translation of an intuitionistic…
We discuss the application of random projections to conic programming: notably linear, second-order and semidefinite programs. We prove general approximation results on feasibility and optimality using the framework of formally real Jordan…
To derive a program for a given specification R means to find an artifact P that satisfies two conditions: P is executable in some programming language; and P is correct with respect to R. Refinement-based program derivation achieves this…
A general theory of programs, programming and programming languages built up from a few concepts of elementary set theory. Derives, as theorems, properties treated as axioms by classic approaches to programming. Covers sequential and…
Persistence modules are representations of products of totally ordered sets in the category of vector spaces. They appear naturally in the representation theory of algebras, but in recent years they have also found applications in other…
This article first presents two examples of algorithms that extracts information on scheme out of its defining equations. We also give a review on the notion of Castelnuovo-Mumford regularity, its main properties (in particular its relation…
We continue our investigation into hybrid polyadic multi-sorted logic with a focus on expresivity related to the operational and axiomatic semantics of rogramming languages, and relations with first-order logic. We identify a fragment of…
This paper describes a generalization of Clark's completion that is applicable to logic programs containing arithmetic operations and produces syntactically simple, natural looking formulas. If a set of first-order axioms is equivalent to…
We extend to natural deduction the approach of Linear Nested Sequents and of 2-sequents. Formulas are decorated with a spatial coordinate, which allows a formulation of formal systems in the original spirit of natural deduction -- only one…