Related papers: Indexed realizability for bounded-time programming…
Runtime efficiency and termination are crucial properties in the studies of program verification. Instead of dealing with these issues in an ad hoc manner, it would be useful to develop a robust framework in which such properties are…
Motivated by algorithmic information theory, the problem of program discovery can help find candidates of underlying generative mechanisms of natural and artificial phenomena. The uncomputability of such inverse problem, however,…
Indexed languages are a classical notion in formal language theory, which has attracted attention in recent decades due to its role in higher-order model checking: They are precisely the languages accepted by order-2 pushdown automata. The…
We describe a realizability framework for classical first-order logic in which realizers live in (a model of) typed {\lambda}{\mu}-calculus. This allows a direct interpretation of classical proofs, avoiding the usual negative translation to…
Linear temporal logic (LTL) is a specification language for finite sequences (called traces) widely used in program verification, motion planning in robotics, process mining, and many other areas. We consider the problem of learning LTL…
This is the author's Ph.D. Thesis. It contains results from four years of research into realizability and categorical logic. The main subjects are the axiomatisation of realizable propositions, and a characterization of realizability…
One of the aims of Implicit Computational Complexity is the design of programming languages with bounded computational complexity; indeed, guaranteeing and certifying a limited resources usage is of central importance for various aspects of…
The class of Basic Feasible Functionals BFF$_2$ is the type-2 counterpart of the class FP of type-1 functions computable in polynomial time. Several characterizations have been suggested in the literature, but none of these present a…
Probabilistic team semantics is a framework for logical analysis of probabilistic dependencies. Our focus is on the axiomatizability, complexity, and expressivity of probabilistic inclusion logic and its extensions. We identify a natural…
We propose to consider non confluence with respect to implicit complexity. We come back to some well known classes of first-order functional program, for which we have a characterization of their intentional properties, namely the class of…
It is well-known that constructing models of higher-order probabilistic programming languages is challenging. We show how to construct step-indexed logical relations for a probabilistic extension of a higher-order programming language with…
In this paper we study the complexity of the problems: given a loop, described by linear constraints over a finite set of variables, is there a linear or lexicographical-linear ranking function for this loop? While existence of such…
We exhibit a sound and complete implicit-complexity formalism for functions feasibly computable by structural recursions over inductively defined data structures. Feasibly computable here means that the structural-recursive definition runs…
We present a new type system with support for proofs of programs in a call-by-value language with control operators. The proof mechanism relies on observational equivalence of (untyped) programs. It appears in two type constructors, which…
We give new proofs of soundness (all representable functions on base types lies in certain complexity classes) for Elementary Affine Logic, LFPL (a language for polytime computation close to realistic functional programming introduced by…
The authors' ATR programming formalism is a version of call-by-value PCF under a complexity-theoretically motivated type system. ATR programs run in type-2 polynomial-time and all standard type-2 basic feasible functionals are ATR-definable…
Functional programming languages are particularly well-suited for building automated reasoning systems, since (among other reasons) a logical term is well modeled by an inductive type, traversing a term can be implemented generically as a…
The ramification method in Implicit Computational Complexity has been associated with functional programming, but adapting it to generic imperative programming is highly desirable, given the wider algorithmic applicability of imperative…
Reasoning under uncertainty is a fundamental challenge in Artificial Intelligence. As with most of these challenges, there is a harsh dilemma between the expressive power of the language used, and the tractability of the computational…
We explain how recent developments in the fields of realisability models for linear logic -- or geometry of interaction -- and implicit computational complexity can lead to a new approach of implicit computational complexity. This…