相关论文: Cons-free Programming with Immutable Functions

In automated complexity analysis, noninterference-based type systems statically guarantee, via soundness, the property that well-typed programs compute functions of a given complexity class, e.g., the class FP of functions computable in…

Since more than three decades, interior-point methods proved very useful for optimization, from linear over semidefinite to conic (and partly beyond non-convex) programming; despite the fact that already in the semidefinite case (even when…

Relying on the formulae-as-types paradigm for classical logic, we define a program logic for an imperative language with higher-order procedural variables and non-local jumps. Then, we show how to derive a sound program logic for this…

In this paper, we study a class of nonsmooth fractional programs {\rm (FP, for short)} with SOS-convex semi-algebraic functions. Under suitable assumptions, we derive a strong duality result between the problem (FP) and its semidefinite…

One of the main applications of semidefinite programming lies in linear systems and control theory. Many problems in this subject, certainly the textbook classics, have matrices as variables, and the formulas naturally contain…

We study the problem of deciding whether a given language is directed. A language $L$ is \emph{directed} if every pair of words in $L$ have a common (scattered) superword in $L$. Deciding directedness is a fundamental problem in connection…

This paper obtains a completeness result for inequational reasoning with applicative terms without variables in a setting where the intended semantic models are the full structures, the full type hierarchies over preorders for the base…

Traditional recurrent neural networks (RNNs) have a fixed, finite number of memory cells. In theory (assuming bounded range and precision), this limits their formal language recognition power to regular languages, and in practice, RNNs have…

In Programming by Example, a system attempts to infer a program from input and output examples, generally by searching for a composition of certain base functions. Performing a naive brute force search is infeasible for even mildly involved…

The idea of functional programming has played a big role in shaping today's landscape of mainstream programming languages. Another concept that dominates the current programming style is Dijkstra's structured programming. Both concepts have…

We give some connections between various functions defined on finitely presented groups (isoperimetric, isodiametric, Todd-Coxeter radius, filling length functions, etc.), and we study the relation between those functions and the…

Throughout the history of functional programming, recursion has emerged as a natural method for describing loops in programs. However, there does often exist a substantial cognitive distance between the recursive definition and the simplest…

In the paper the problem of verification of functional programs (FPs) over strings is considered, where specifications of properties of FPs are defined by other FPs, and a FP S1 meets a specification defined by another FP S2 iff a…

We know extensions of first order logic by quantifiers of the kind "there are uncountable many ...", "most ..." with new axioms and appropriate semantics. Related are operations such as "set of x, such that ...", Hilbert's…

Natural language syntax yields an unbounded array of hierarchically structured expressions. We claim that these are used in the service of active inference in accord with the free-energy principle (FEP). While conceptual advances alongside…

We define higher order infinitesimal noncommutative probability space and infinitesimal non-crossing cumulant functionals. In this framework, we generalize to higher order the notion of infinitesimal freeness, via a vanishing of mixed…

We give a new, direct proof of the tetrachotomy classification for the model-checking problem of positive equality-free logic parameterised by the model. The four complexity classes are Logspace, NP-complete, co-NP-complete and…

Model-checking is one of the most powerful techniques for verifying systems and programs, which since the pioneering results by Knapik et al., Ong, and Kobayashi, is known to be applicable to functional programs with higher-order types…

We present a logical system CFP (Concurrent Fixed Point Logic) supporting the extraction of nondeterministic and concurrent programs that are provably total and correct. CFP is an intuitionistic first-order logic with inductive and…

We prove that the first-order theory of any function field K of characteristic p>2 is undecidable in the language of rings without parameters. When K is a function field in one variable whose constant field is algebraic over a finite field,…