Emmanuel Hainry, Bruce M. Kapron, Jean-Yves Marion, and Romain Péchoux.
Declassification Policy for Program Complexity Analysis.
In LICS '24: 39th Annual ACM/IEEE Symposium on Logic in
Computer Science, pages 1--14, Tallinn Estonia, France, july 2024. ACM.
[ bib |
DOI |
http |
.pdf ]
Keywords: Theory of computation -> Complexity theory and logic ; Type theory ; Noninterference ; Declassification ; Polynomial time ; Basic Feasible Functionals ; Complexity analysis
Emmanuel Hainry, Romain Péchoux, and Mário Silva.
A programming language characterizing quantum polynomial time.
In Foundations of Software Science and Computation Structures
(FoSSaCS 2023), Paris, France, april 2023.
[ bib |
DOI |
http |
.pdf ]
Emmanuel Hainry and Romain Péchoux.
A general noninterference policy for polynomial time.
In Principles of Programming Languages, POPL 2023, volume 7 of
Proc. ACM Program. Lang., pages 806--832. ACM, 2023.
[ bib |
DOI |
http |
.pdf ]
We introduce a new noninterference policy to capture the class of functions computable in polynomial time on an object-oriented programming language. This policy makes a clear separation between the standard noninterference techniques for the control flow and the layering properties required to ensure that each “security” level preserves polynomial time soundness, and is thus very powerful as for the class of programs it can capture. This new characterization is a proper extension of existing tractable characterizations of polynomial time based on safe recursion. Despite the fact that this noninterference policy is Π10-complete, we show that it can be instantiated to some decidable and conservative instance using shape analysis techniques.
Keywords: Polynomial time, Noninterference, Shape Analysis, Computational Complexity
Emmanuel Hainry, Bruce M. Kapron, Jean-Yves Marion, and Romain Péchoux.
A tier-based typed programming language characterizing feasible
functionals.
Logical Methods in Computer Science, 18(1), 2022.
[ bib |
DOI |
http |
.pdf ]
Emmanuel Hainry, Bruce M. Kapron, Jean-Yves Marion, and Romain Péchoux.
Complete and tractable machine-independent characterizations of
second-order polytime.
In Foundations of Software Science and Computation Structures
(FoSSaCS 2022), Lecture Notes in Computer Science, pages 368--388. Springer,
2022.
[ bib |
DOI |
http |
.pdf ]
Emmanuel Hainry, Emmanuel Jeandel, Romain Péchoux, and Olivier Zeyen.
Complexityparser: An automatic tool for certifying poly-time
complexity of java programs.
In Antonio Cerone and Peter Csaba Ölveczky, editors,
ICTAC 2021 - 18th International Colloquium on Theoretical Aspects of
Computing, volume 12819 of Lecture Notes in Computer Science, pages
357--365, Nur-Sultan, Kazakhstan, september 2021. Springer.
[ bib |
DOI |
http |
.pdf ]
Emmanuel Hainry and Romain Péchoux.
Theory of Higher Order Interpretations and Application to Basic
Feasible Functions.
Logical Methods in Computer Science, 16(4):25, december 2020.
[ bib |
DOI |
http |
.pdf ]
Emmanuel Hainry, Damiano Mazza, and Romain Péchoux.
Polynomial time over the reals with parsimony.
In Functional and Logic Programming (FLOPS 2020), Akita, Japan,
april 2020.
[ bib |
DOI |
http |
.pdf ]
Emmanuel Hainry, Bruce M. Kapron, Jean-Yves Marion, and Romain Péchoux.
A tier-based typed programming language characterizing Feasible
Functionals.
In Logic in Computer Science, LICS 2020, pages 535--549,
Saarbrücken, Germany, july 2020. ACM.
[ bib |
DOI |
http |
.pdf ]
Keywords: Feasible functionals ; BFF ; implicit computational complexity ; tiering ; type-2 ; type system
Emmanuel Hainry and Romain Péchoux.
A Type-Based Complexity Analysis of Object Oriented Programs.
Information and Computation, 261(1):78--115, august 2018.
[ bib |
DOI |
http |
.pdf ]
Keywords: Object Oriented Program ; Type system ; complexity ; polynomial time
Emmanuel Hainry and Romain Péchoux.
Higher order interpretation for higher order complexity.
In Thomas Eiter and David Sands, editors, LPAR-21. 21st
International Conference on Logic for Programming, Artificial Intelligence
and Reasoning, volume 46 of EPiC Series in Computing, pages 269--285,
2017.
[ bib |
DOI ]
We design an interpretation-based theory of higher-order functions that is well-suited for the complexity analysis of a standard higher- order functional language a` la ml. We manage to express the interpretation of a given program in terms of a least fixpoint and we show that when restricted to functions bounded by higher-order polynomials, they characterize exactly classes of tractable functions known as Basic Feasible Functions at any order.
Emmanuel Hainry and Romain Péchoux.
Objects in Polynomial Time.
In Xinyu Feng and Sungwoo Park, editors, APLAS 2015, volume
9458 of Lecture Notes in Computer Science, pages 387--404, Pohang,
South Korea, november 2015. Springer.
[ bib |
DOI |
http |
.pdf ]
Hugo Férée, Emmanuel Hainry, Mathieu Hoyrup, and Romain
Péchoux.
Characterizing polynomial time complexity of stream programs using
interpretations.
Theoretical Computer Science, 585:41--54, 2015.
[ bib |
DOI ]
Olivier Bournez, Daniel Graça, and Emmanuel Hainry.
Computation with perturbed dynamical systems.
Journal of Computer and System Sciences, 79(5):714--724, 2013.
[ bib |
DOI |
http ]
Keywords: robustness ; Dynamical systems ; reachability ; computational power ; verification
Olivier Bournez, Walid Gomaa, and Emmanuel Hainry.
Algebraic Characterizations of Complexity-Theoretic Classes of Real
Functions.
International Journal of Unconventional Computing,
7(5):331--351, 2011.
[ bib |
http ]
Keywords: Recursive Analysis ; Polynomial Time ; Algebraic Characterization ; Real Computation ; Oracle Turing Machines
Hugo Férée, Emmanuel Hainry, Mathieu Hoyrup, and Romain
Péchoux.
Interpretation of stream programs: characterizing type 2 polynomial
time complexity.
In Ottfried Cheong, Kyung-Wong Chwa, and Kunsoo Park, editors,
International Symposium on Algorithms and Computation (ISAAC),
volume 6506 of Lecture Notes in Computer Science, pages 291--303,
Jeju Island, South Korea, 2010. Springer.
[ bib |
DOI ]
We study polynomial time complexity of type
2 functionals. For that purpose, we introduce a first order
functional stream language. We give criteria, named
well-founded, on such programs relying on second order
interpretation that characterize two variants of type 2
polynomial complexity including the Basic Feasible
Functions (BFF). These characterizations provide a new
insight on the complexity of stream programs. Finally, we
adapt these results to functions over the reals, a particular
case of type 2 functions, and we provide a characterization of
polynomial time complexity in Recursive Analysis.
Olivier Bournez, Daniel S. Graça, and Emmanuel Hainry.
Robust computations with dynamical systems.
In Petr Hliněný and Antonín Kučera, editors,
Mathematical Foundations of Computer Science, MFCS 2010, volume 6281 of
Lecture Notes in Computer Science, pages 198--208. Springer, 2010.
[ bib |
DOI ]
In this paper we discuss the computational
power of Lipschitz dynamical systems which are robust to
infinitesimal perturbations. Whereas the study in [1] was done
only for not-so-natural systems from a classical mathematical
point of view (discontinuous differential equation systems,
discontinuous piecewise affine maps, or perturbed Turing
machines), we prove that the results presented there can be
generalized to Lipschitz and computable dynamical systems. In
other words, we prove that the perturbed reachability problem
(i.e. the reachability problem for systems which are subjected
to infinitesimal perturbations) is co-recursively enumerable
for this kind of systems. Using this result we show that if
robustness to infinitesimal perturbations is also required, the
reachability problem becomes decidable. This result can be
interpreted in the following manner: undecidability of
verification doesn't hold for Lipschitz, computable and robust
systems. We also show that the perturbed reachability problem
is co-r.e. complete even for C-systems.
Emmanuel Hainry.
Decidability and Undecidability in Dynamical Systems.
Research report, CARTE - INRIA Lorraine - LORIA - CNRS :
UMR7503 - INRIA - Université Henri Poincaré - Nancy I -
Université Nancy II - Institut National Polytechnique de
Lorraine, 2009.
[ bib |
http ]
A computing system can be modelized in
various ways: one being in analogy with transfer functions,
this is a function that associates to an input and optionally
some internal states, an output ; another being focused on the
behaviour of the system, that is describing the sequence of
states the system will follow to get from this input to produce
the output. This second kind of system can be defined by
dynamical systems. They indeed describe the “local”
behaviour of a system by associating a configuration of the
system to the next configuration. It is obviously interesting
to get an idea of the “global” behaviour of such a dynamical
system. The questions that it raises can be for example
related to the reachability of a certain configuration or set
of configurations or to the computation of the points that will
be visited infinitely often. Those questions are
unfortunately very complex: they are in most cases undecidable.
This article will describe the fundamental problems on
dynamical systems and exhibit some results on decidability and
undecidability in various kinds of dynamical systems.
Olivier Bournez, Walid Gomaa, and Emmanuel Hainry.
Implicit complexity in recursive analysis.
In LCC'09 - Logic and Computational Complexity, Los
Angeles États-Unis d'Amérique, august 2009.
[ bib |
http ]
Recursive analysis is a model of analog
computation which is based on type 2 Turing machines.
Various classes of functions computable in recursive analysis
have recently been characterized in a machine independent and
algebraical context. In particular nice connections between
the class of computable functions (and some of its sub and
sup-classes) over the reals and algebraically defined (sub- and
sup-) classes of R-recursive functions à la Moore have
been obtained. We provide in this paper a framework that
allows to dive into complexity for functions over the reals.
It indeed relates classical computability and complexity
classes with the corresponding classes in recursive analysis.
This framework opens the field of implicit complexity of
functions over the reals. While our setting provides a new
reading of some of the existing characterizations, it also
provides new results: inspired by Bellantoni and Cook's
characterization of polynomial time computable functions, we
provide the first algebraic characterization of polynomial time
computable functions over the reals.
Emmanuel Hainry.
Computing omega-limit sets in linear dynamical systems.
In Cristian S. Calude, José Félix Costa, Rudolf Freund,
Marion Oswald, and Grzegorz Rozenberg, editors, Unconventional
Computing, UC 2008, volume 5204 of Lecture Notes in Computer Science,
pages 83--95, 2008.
[ bib |
DOI ]
Dynamical systems allow to modelize various phenomena or
processes by only describing their local behaviour. It is an important
matter to study the global and the limit behaviour of such systems.
A possible description of this limit behaviour is via the
omega-limit set: the set of points that can be limit of
subtrajectories. The omega-limit set is in general uncomputable. It
can be a set highly difficult to apprehend. Some systems have for
example a fractal omega-limit set. However, in some specific cases,
this set can be computed. This problem is important to verify
properties of dynamical systems, in particular to predict its
collapse or its infinite expansion. We prove in this paper that
for linear continuous time dynamical systems, it is in fact
computable. More, we also prove that the ω-limit set is
a semi-algebraic set. The algorithm to compute this set can
easily be derived from this proof.
Emmanuel Hainry.
Reachability in linear dynamical systems.
In Arnold Beckmann, Costas Dimitracopoulos, and Benedikt Löwe,
editors, CiE 2008: Logic and Theory of Algorithms, volume 5028 of
Lecture Notes in Computer Science, pages 241--250, 2008.
[ bib |
DOI ]
Dynamical systems allow to modelize various phenomena or
processes by only describing their local behaviour. The study of
dynamical systems aims at knowing more on the global behaviour.
Checking the reachability of a point is a fundamental problem. In
this document, using results from the algebraic numbers theory such
as Gelfond-Schneider's theorem, we will show that this problem that
is undecidable in the general case is in fact decidable for a
natural class of continuous-time dynamical systems: linear
systems.
Olivier Bournez and Emmanuel Hainry.
On the computational capabilities of several models.
In Jérôme Durand-Lose and Maurice Margenstern, editors,
Machines, Computations, and Universality - MCU 2007, Orléans, France,
volume 4664 of Lecture Notes in Computer Science, pages 12--23.
Springer, 2007.
[ bib |
DOI ]
We review some results about the computational
power of several computational models. Considered models have in common
to be related to continuous dynamical systems.
Olivier Bournez, Manuel L. Campagnolo, Daniel S. Graça, and Emmanuel
Hainry.
Polynomial differential equations compute all real computable
functions on computable compact intervals.
Journal of Complexity, 23(3):317--335, 2007.
[ bib |
DOI ]
In the last decade, there have been several attempts to
understand the relations between the many models of analog computation.
Unfortunately, most models are not equivalent. Euler's Gamma
function, which is computable according to computable analysis, but
that cannot be generated by Shannon's General Purpose Analog
Computer (GPAC), has often been used to argue that the GPAC is less
powerful than digital computation. However, when computability with
GPACs is not restricted to real-time generation of functions, it
has been shown recently that Gamma becomes computable by a GPAC.
Here we extend this result by showing that, in an appropriate
framework, the GPAC and computable analysis are actually equivalent
from the computability point of view, at least in compact
intervals. Since GPACs are equivalent to systems of polynomial
differential equations then we show that all real computable
functions over compact intervals can be defined by such models.
Keywords: Analog computation; Computable analysis; General Purpose Analog Computer; Church--Turing thesis; Differential equations
Emmanuel Hainry.
Modèles de calcul sur les réels, résultats de
comparaison.
PhD thesis, Institut National Polytechnique de Lorraine, december
2006.
[ bib |
.pdf ]
Il existe de nombreux modèles de calcul sur les réels. Ces
différents modèles calculent diverses fonctions, certains sont plus
puissants que d'autres, certains sont deux à deux incomparables. Le
calcul sur les réels est donc de ce point de vue bien différent du
calcul sur les entiers qui est unifié par la thèse de Church-Turing
qui affirme que tous les modèles raisonnables calculent les m^emes
fonctions.
Les résultats de cette thèse sont de deux sortes. Premièrement,
nous montrons des équivalences entre les fonctions récursivement
calculables et une certaine classe de fonctions
R-récursives et entre les fonctions GPAC-calculables et
les fonctions récursivement calculables. Ces deux résultats ne sont
cependant valables que si les fonctions présentent quelques
caractéristiques : elles doivent ^etre définies sur un compact et dans
le premier cas ^etre de classe C2. Deuxièmement, nous
montrons également une hiérarchie de classes de fonctions
R-récursives qui caractérisent les fonctions
élémentairement calculables, les fonctions En-calculables
pour n>=3 (où les En sont les fonctions de la
hiérarchie de Grzegorczyk), et des fonctions récursivement
calculables. Ce résultat utilise un opérateur de limite dont nous
avons prouvé la généralité en montrant qu'il transfère une inclusion
sur la partie discrète des fonctions en une inclusion sur les
fonctions sur les réels elles-m^emes.
Ces résultats constituent donc une avancée vers une éventuelle
unification des modèles de calcul sur les réels.
Keywords: Analyse récursive, calculabilité réelle, fonctions élémentaires, hiérarchie de Grzegorczyk, General Purpose Analog Computer
Olivier Bournez and Emmanuel Hainry.
Recursive analysis characterized as a class of real recursive
functions.
Fundamenta Informaticae, 74(4):409--433, 2006.
[ bib |
http ]
Recently, using a limit schema, we presented an analog and
machine independent algebraic characterization of elementarily
computable functions over the real numbers in the sense of
recursive analysis. In a dierent and orthogonal work, we proposed a
minimization schema that allows to provide a class of real
recursive functions that corresponds to extensions of computable
functions over the integers. Mixing the two approaches we prove
that computable functions over the real numbers in the sense of
recursive analysis can be characterized as the smallest class of
functions that contains some basic functions, and closed by
composition, linear integration, minimization and limit schema.
Olivier Bournez, Manuel L. Campagnolo, Daniel S. Graça, and Emmanuel
Hainry.
The general purpose analog computer and computable analysis are two
equivalent paradigms of analog computation.
In Jin-Yi Cai, S. Barry Cooper, and Angsheng Li, editors, Theory
and Applications of Models of Computation, TAMC 2006, volume 3959 of
Lecture Notes in Computer Science, pages 631 -- 643. Springer, 2006.
[ bib |
DOI ]
In this paper we revisit one of the first models of analog
computation, Shannon's General Purpose Analog Computer (GPAC). The GPAC
has often been argued to be weaker than computable analysis. As
main contribution, we show that if we change the notion of
GPAC-computability in a natural way, we compute exactly all real
computable functions (in the sense of computable analysis).
Moreover, since GPACs are equivalent to systems of polynomial
differential equations then we show that all real computable
functions can be defined by such models.
Olivier Bournez and Emmanuel Hainry.
Elementary computable functions over the real numbers and
R-sub-recursive functions.
Theoretical Computer Science, 348(2-3):130--147, december 2005.
[ bib |
DOI ]
We present an analog and machine-independent algebraic
characterization of elementarily computable functions over the real
numbers in the sense of recursive analysis: we prove that they
correspond to the smallest class of functions that contains some
basic functions, and closed by composition, linear integration, and
a simple limit schema. We generalize this result to all higher levels
of the Grzegorczyk Hierarchy. This paper improves several previous
partial characterizations and has a dual interest:
* Concerning recursive analysis, our results provide
machine-independent characterizations of natural classes of
computable functions over the real numbers, allowing to define
these classes without usual considerations on higher-order (type 2)
Turing machines.
* Concerning analog models, our results provide a characterization
of the power of a natural class of analog models over the real
numbers and provide new insights for understanding the relations
between several analog computational models.
Keywords: Analog computation; Recursive analysis; Real recursive functions; Computability; Analysis
Olivier Bournez and Emmanuel Hainry.
Real recursive functions and real extentions of recursive functions.
In Maurice Margenstern, editor, Machines, Computations, and
Universality, MCU 2004, volume 3354 of Lecture Notes in Computer
Science, pages 116--127. Springer, 2005.
[ bib |
DOI ]
Recently, functions over the reals that extend elementarily
computable functions over the integers have been proved to correspond
to the smallest class of real functions containing some basic
functions and closed by composition and linear integration. We
extend this result to all computable functions: functions over the
reals that extend total recursive functions over the integers are
proved to correspond to the smallest class of real functions
containing some basic functions and closed by composition, linear
integration and a very natural unique minimization schema.
Olivier Bournez and Emmanuel Hainry.
An analog characterization of elementary computable functions over
the real numbers.
In Josep Díaz, Juhani Karhumäki, Arto Lepistö, and Donald
Sannella, editors, International Colloquium on Automata, Languages and
Programming (ICALP 2004), volume 3142 of Lecture Notes in Computer
Science, pages 269--280, 2004.
[ bib |
DOI ]
We present an analog and machine-independent algebraic
characterization of elementarily computable functions over the real
numbers in the sense of recursive analysis: we prove that they
correspond to the smallest class of functions that contains some
basic functions, and closed by composition, linear integration, and
a simple limit schema. We generalize this result to all higher
levels of the Grzegorczyk Hierarchy. Concerning recursive
analysis, our results provide machine-independent characterizations
of natural classes of computable functions over the real numbers,
making it possible to define these classes without usual considerations
on higher-order (type 2) Turing machines. Concerning analog models,
our results provide a characterization of the power of a natural class
of analog models over the real numbers.
Olivier Bournez and Emmanuel Hainry.
An analog characterization of elementarily computable functions over
the real numbers.
In 2nd APPSEM II Workshop - APPSEM'2004, Tallinn, Estonia,
april 2004.
[ bib |
.ps ]
We present an analog and machine-independent algebraic
characterizations of elementarily computable functions over the real
numbers in the sense of recursive analysis: we prove that they
correspond to the smallest class of functions that contains some
basic functions, and closed by composition, linear integration, and
a simple limit schema. We generalize this result to all higher
levels of the Grzegorczyk Hierarchy. Concerning recursive analysis,
our results provide machine-independent characterizations of natural
classes of computable functions over the real numbers, allowing to
define these classes without usual considerations on higher-order
(type 2) Turing machines. Concerning analog models, our results
provide a characterization of the power of a natural class of
analog models over the real numbers.
Keywords: analog models, complexity, computability
Emmanuel Hainry.
Fonctions réelles calculables et fonctions R-récursives.
Stage de dea, ENS Lyon, july 2003.
[ bib |
.ps ]
On définit des opérateurs de limites sur les
fonctions. A l'aide de ces opérateurs, on définit de nouvelles
classes de fonctions par clôture. On compare ces classes avec
les fonctions élémentairement calculables (définies
à partir de machines de Turing). On obtient ainsi une
caractérisation des fonctions élémentairement calculables
sous forme de clôture.
Keywords: computability, computation over reals, elementary functions, real rcomputable functions