Séminaire interuniversitaire de logique mathématique (3ème cycle FNRS) Sauf mention contraire, le cours de DEA et les séminaires du jeudi après-midi ont lieu à l'ULB, Campus de la Plaine, au local 2NO906. Un itinéraire (bilingue) est disponible. Les exposés du vendredi ont lieu à l'UMH, Campus de la Plaine. | |
Programme 2004-2005
Pour recevoir le programme par email lors de ses mises à jour,
laissez-nous vos coordonnées à l'adresse
http://www.umh.ac.be/math/logic/logicdb/inscription.php
Programme ULB-UMH
Second semestre (Janvier-Mars)
2005 |
Cours du matin (11h - 12h30) |
Exposés de l'après-midi (14h30 - 16h) |
20 janvier, ULB, |
Pas de séance
|
Thomas Brihaye (UMH) |
03 février, ULB, |
Pas de séance |
Roland Hinnion (ULB) |
10 février, ULB, |
Pas de séance |
Sonja Smets (VUB) |
17 févier, ULB, |
Pas de séance |
M.Schellekens (Cork) |
24 février, ULB, |
Pas de séance |
Georges Hansoul (ULg) |
03 mars, ULB, |
Pas de séance |
Léon Horsten (KUL) |
10 mars, ULB, |
Pas de séance |
Bruno Teheux (ULg) |
17 mars, ULB, |
Pas de séance |
Philippe Kreutz (ULB) |
24 mars,ULB, |
Pas de séance |
Marc Peeters (ULB) |
14 avril, ULB, |
Pas de séance |
Michel Rigo (Ulg) |
21 avril, ULB, |
Pas de séance |
Emilie Charlier (ULg) |
28 avril, ULB, |
Pas de séance |
Jacques Riche (KUL) |
5 mai |
Congé |
Congé |
12 mai, ULB, |
Pas de séance |
Pas de séance |
19 mai, ULb, |
Pas de séance |
Pas de séance |
!!! du vendredi 20 mai au dimanche 22 mai à Gand !!! |
||
26 mai, ULB, |
Pas de séance |
Marc Dominicy (ULB) |
2 juin, ULB, |
Pas de séance |
Pas de séance |
9 juin, ULB, |
Pas de séance |
D. Niwinski (Warsaw University) |
16 juin, ULB, |
K.Meer (Odense) |
Pas de séance |
Résumés:
Damian Niwinski (Warsaw) "On
the complexity of infinite computations"
Finite-state automata constitute the very basic level in classical
complexity theory. In contrast, when applied to infinite words and
trees, they reveal a remarkable definability power, going beyond the
Borel hierarchy. Still, some good properties of finite automata
remain, like decidability of normal forms. The talk will compare
various complexity hierarchies with the emphasis on decidability
questions, and present some recent results obtained by the author in
collaboration with Igor Walukiewicz and Filip Murlak.
The transparencies are available here.
Klaus Meer (Odense) "Real
number models and probabilistically checkable proofs"
Probabilistically checkable proofs (PCPs) represent one of the most
important recent areas in theoretical computer science . The idea is
to make verification proofs of NP-problems more stable: Reading only
a {\em constant}number of data units in such a potential proof will
be sufficient to detect faults with high probability.
In this talk we introduce the PCP notion for the real number model of
Blum, Shub, and Smale. We then study the existence of certain such
``transparent'' proofs for the class NP$_{\mathbb R}$ of real number
decision problems verifiable in polynomial time.
Jacques Riche (KUL) "Logiques relevantes"
Dans une première partie, on pourra expliquer ce qu'il faut
entendre par "Logique Relevante" en présentant les
motivations historiques à partir des paradoxes classiques
liés à l'implication matérielle, depuis Lewis et
l'implication stricte jusqu'à Church, Ackermann et
l'Entailment de Anderson & Belnap. Pour situer ces logiques en
termes plus familiers, on pourrait dire qu'elles sont non-classiques,
non-monotones et paraconsistantes.
Si ces motivations reposent sur des arguments aussi bien
philosophiques que logiques, une approche plus neutre,
algébrique, du genre Curry, permet de la comparer à
l'algèbre booléenne, par exemple, et d'arriver à
une caractérisation algébrique de différents
systèmes de ces logiques (groupoïdes
résidués, monoïdes de De Morgan,
distributoïdes etc.). L'intérêt de cette
caractérisation est de montrer que ces logiques, dotées
d'une sémantique appropriée, dite "de
Routley-Meyer", ont une contrepartie algébrique
naturelle. Une théorie de la représentation permet
alors de relier leurs aspects sémantiques et algébriques
et d'éclairer ainsi la partie logique qui concerne la
relation d'implication ou de conséquence logique. Puisque
c'est de cela qu'il s'agit.
Dans une seconde partie, on évoquera de manière plus ou
moins détaillée quelques questions particulières
liées à ces logiques. Par exemple, leurs rapports avec
la logique classique, avec la logique combinatoire et le lambda
calcul, les questions de décision et de complexité;
leurs rapports avec l'arithmétique, l'algèbre, la
théorie des nombres, la théorie des modèles etc.
Ou encore certaines caractéristiques propres qui les
distinguent dans le domaine plus général de la logique.
Marc Peeters (ULB) "Présentation
de la méréologie de Lesniewski"
Après une présentation de l'auteur, je traiterai de la
solution que Lesniewski a apportée à l'antinomie de
Russell, résolution qui débouche sur la
méréologie. Ensuite, j'aborderai quelques pistes contemporaines.
Marc Dominicy (ULB): En quoi les langages naturels sont-ils « informels »?
Philippe Kreutz (ULB) "L'extensionalité
des rapports de perception"
Il est bien connu que des verbes tels que voir et entendre
possèdent un sens perceptuel dans les énoncés
avec construction infinitivale mais éventuellement un sens
épistémique dans les énoncés avec une
complétive en «que». Les premiers, au contraire des
seconds, respectent (sauf vis-à-vis des expressions
propositionnelles) le principe de substitution salva veritate des
expressions co-référentielles. La distinction classique
entre les attributions de re et de dicto savère
insatisfaisante pour rendre compte de cette donnée et ce,
aussi bien dans une perspective frégéenne que dans une
approche millienne de la référence. A la lumière
des travaux de [Dretske, 1981] et de [Stenning & Inder, 1995),
nous montrerons que cette divergence de comportement à
légard du principe de substitution sexplique
plutôt par la nature respective (analogique Vs non-analogique)
des représentations liées aux modalités
perceptuelles et épistémiques.
Bruno Teheux(ULg): Dualité
pour des MV-algèbres à opérateurs
Nous commencerons par définir une notion
d'opérateur sur les MV-algèbres en discutant des
différentes axiomatisations qu'il aurait été
possible d'utiliser. Nous construirons ensuite une dualité
pour la classe des MV-algèbres à opérateurs dont
la MV-algèbre sous-jacente est dans une variété
finiment engendrée déterminée. Cette
dualité est une extension de la dualité connue pour les
algèbres de Boole à opérateurs. Nous obtiendrons
une axiomatisation de la catégorie duale et nous
intéresserons à la construction des sommes dans cette
catégorie. Enfin, nous aborderons le problème de
l'extension d'un opérateur défini sur l'algèbre
de Boole des idempotents d'une MV-algèbre en un
opérateur sur la MV-algèbre.
Léon
Horsten (KUL):"Partial Kripke-Feferman (joint work
with Volker Halbach, Oxford University)"
Feferman and Reinhardt have formalized Kripke's semantical partial
inductive theory of truth in classical logic. The resulting system,
KF (Kripke-Feferman), has been extensively studied. We argue that for
philosophical reasons, Kripke's semantical theory should be
formalized in partial logic. We undertake this task, and investigate
the proof-theoretical strength of the resulting proof system.
Georges Hansoul (ULg)
"Bisimulations en algèbre universelle"
Des disciplines mathématiques variées ont eu recours
sous des dénominations diverses à ce qui est maintenant
à la mode sous le nom de bisimulation.Il s'agit tout
simplement de l'usuel concept d'homomorphisme pour des structures
où les fonctions peuvent prendre plusieurs valeurs en un
point.Cette simple observation permet un petit traitement
algébrique du concept, que nous présentons ici, ainsi
que deux applications: algèbres de Boole et logique modale.
M.Schellekens (Cork):"Towards
a Calculus for Modular Software Timing"
The Centre for Efficiency-Oriented Languages CEOL
(http://www.ceol.ucc.ie/) was set up with initial funding of Euro 1M
from Science Foundation Ireland and collaborates with Sun
Microsystems. Software Timing is crucial for many Computer Science
applications. Yet timing is well known to quickly lead to difficult
mathematical problems. CEOL focuses on the development of a new
programming language ACETT: the Average-Case Execution Time Tool.
ACETT is currently implemented at CEOL in Java 5.0 In this talk we
outline the new mathematical principles which have led to the
development of ACETT and how this approach affects four mainstream
Computer Science areas: Automated Average-Case Analysis, Semantics
& Complexity, Random Structures and Real-Time Languages.
Average-Case Time Analysis is one of the most thoroughly studied
areas of Computer Science and is notoriously difficult, involving a
variety of techniques which, typically, do not allow for automation.
Currently algorithms must be analyzed on a case-by-case basis, and it
is not feasible in general to express the Average-Case time of
algorithms via a recurrence equation, though excellent techniques are
available to solve these recurrences. A well-known example of an
algorithm for which the exact average-case time is not known is the
sorting algorithh Heapsort, as discussed by Knuth, Edelkamp and Flajolet.
We introduce a new unified approach to Average-Case Time analysis and
outline the mathematical ideas which led to this development. The
novel programming language ACETT is proposed for which the
Average-Case Time Complexity is shown to be Linearly-Compositional;
i.e. the Average-Case Time of ACETT-programs can be expressed as
linear combinations of the Average-Case Time of their basic
components. This considerably simplifies the Average-Case Time
analysis of ACETT-programs and opens the way for (semi-)automation
via modular timing. We discuss a new ACETT-version of Heapsort,
Percolating Heapsort, for which the exact time analysis is possible
(as opposed to classical Heapsort). Finally, we give an overview of
future work in this area.
Sonja Smets (VUB) "On Quantum
Transition Systems and Quantum Dynamic Algebra" (Joint work
with A. Baltag, Comlab, Oxford University)
I will first introduce the classical setting of Propositional Dynamic
Logic (PDL). This classical setting will be compared to a Quantum
version of Propositional Dynamic Logic (called QPDL). I will focus
mainly on the Kripke style semantics for QPDL, i.e. on Quantum
Transition Systems. Next I will give (short) outlines of the Proof
System and of the Dynamic Algebra. These axiomatizations of QPDL
solve a lot of problems: 1) These axiomatizations are complete with
respect to infinite Hilbert spaces endowed with (phase-free) quantum
actions! 2) QPDL supports my previous work on this issue by providing
a clear and intuitive dynamic-operational meaning to key postulates
such as Orthomodularity and the Covering Law. 3) QPDL provides a link
between traditional quantum logic and the needs of quantum computation.
Roland Hinnion (ULB): "Un
modèle de termes pour une théorie predicative,
intensionnelle des ensembles partiels"
Il est bien connu que, parmi les théories
ensemblistes basées sur une forme de compréhension
(/abstraction) "positive", celles qui sont
"classiques" et celles qui sont "paraconsistantes"
ont été étudiées avec succès, et
que l'on dispose de modèles (entre autres topologiques)
très riches. Par contre, la version "ensembles
partiels" (/ensembles naifs dans des logiques
"paracomplètes"ou "partielles")
résiste étrangement aux techniques connues. Cet
exposé montrera que la technique de "forcing"
employée pour les ensembles positifs fournit un résultat
dans le cas "partiel" également.
Thomas
Brihaye (UMH): "Vérification
d'automates temporisés avec poids" (travail en
collaboration avec Véronique Bruyère et
Jean-François Raskin)
Dans cet exposé, on étudiera le
problème de "model checking" (vérification)
sur le modèle des automates temporisés avec poids
(weighted timed automata) pour la logique WCTL. On commencera par
rappeler et illustrer les notions suivantes: automates
temporisés (introduits par Alur et Dill en 90), logique CTL
(introduite par Clarke, Emerson, Halpren au début des
années 80). Ensuite, on expliquera comment et pourquoi, on
introduit les automates temporisés avec poids et la logique
WCTL. On se consacrera ensuite à l'étude de la
décidabilité de WCTL. Cette étude
nécessitera l'utilisation de l'outil bisimulation que l'on
rappelera au préalable.
Premier semestre (Octobre-Décembre)
2004 |
Cours du matin (11h - 12h30), sauf mention contraire |
Exposés de l'après-midi (14h30 - 16h), sauf mention contraire |
7 octobre |
Fundamental Computer Science F.N.R.S. Contact Group
Meeting on Constraints in Computer Science |
Fundamental Computer Science F.N.R.S. Contact Group Meeting on Constraints in Computer Science |
14 octobre |
cours de DEA : Logique et Géométrie |
|
21 octobre |
suite du cours de DEA par C. Michaux. |
Bisimulations de systèmes dynamiques et combinatoire des mots |
28 octobre |
exceptionnellement, pas de séance à l'ULB. |
suite du cours de DEA par C. Michaux, |
4 novembre |
pas de séance |
Topologie et modèle de termes dans NF |
5 novembre |
vv |
suite du cours de DEA par C. Michaux, |
11 novembre |
Congé |
Congé |
18 novembre |
TBA |
Intensional positive sets |
19 novembre |
vv |
suite du cours de DEA par C. Michaux, |
25 novembre |
TBA |
Corps de Hardy |
2 décembre |
TBA |
Sémantique sans coupures |
3 décembre
|
TBA |
Relations d'équivalence définissables dans les structures o-minimales et élimination des imaginaires (d'après A. Pillay) |
9 décembre |
TBA |
Nicolas Guzy (UMH) |
16 décembre |
TBA |
Des modèles topologiques pour l'abstraction positive et l'élimination des quantificateurs |
13 --17 décembre |
||
23 décembre |
Congé |
Congé |
Résumés:
Cédric Rivière (UMH):"Relations
d'équivalence définissables dans les structures
o-minimales et élimination des imaginaires (d'après A. Pillay)"
Nous exposerons l'article de Anand Pillay : Some remarks on definable
equivalence relation in o-minimal structures, paru dans le JSL, 51,
3, 1986.
Thierry Libert (ULB):"Des
modèles topologiques pour l'abstraction positive et
l'élimination des quantificateurs"
Le sujet de l'exposé est l'abstraction positive en
théorie des ensembles. Par "abstraction" - au lieu
de "compréhension" - il est sous-entendu que le
langage est muni d'un abstracteur "{-|-}" permettant la
formation de termes primitifs. Je démonterai ici l'existence
de modèles $\kappa$-topologiques, pour tout cardinal
régulier $\kappa$. Une propriété
caractéristique des modèles canoniques nous
amènera alors à prouver l'élimination des
quantificateurs pour les formules positives de la théorie.
Enfin, nous illustrerons aussi l'utilité des modèles
topologiques pour établir de simples résultats d'indépendance.
Nicolas Guzy (UMH): "Corps
de séries logarithmique-exponentielles"
Suite à l'exposé du 25/10, nous allons introduire un
autre exemple de corps valué différentiel qui joue un
rôle central en algèbre différentielle
ordonnée: le corps des séries
logarithmiques-exponentielles. Il s'agit d'étendre le corps
des séries de Laurent sur les réels de façon
canonique afin de le munir d'une exponentiation qui "se comporte
bien". Nous allons dans cet exposé confronter les
différentes approches (van den Dries, Marker, Macintyre et
Kulhmann) de ce problème.
Nicolas Guzy (UMH):
"Corps de Hardy"
Rosenlicht a introduit dans les années 70 la notion de corps
valué différentiel, c'est-à-dire un corps muni
d'une dérivation et d'une valuation qui interragissent
fortement (en particulier la dérivation est continue pour la
topologie de la valuation). Nous allons, au fil d'exemples canoniques
tels que les corps de Hardy, développer les notions naturelles
liées à ces valuations. Nous parlerons ainsi des
couples asymptotiques étudiés récemment de
façons modèle-théorique par van den Dries et Aschenbrenner.
Marcel Crabbé (UCL):"Sémantique
sans coupures"
Nous caractériserons la validité relativement aux
modèles véritablement gloutons pour des schémas
de compréhension. Nous proposerons ainsi un autre regard sur
le phénomène d'absorption des coupures. Nous
terminerons en indiquant une raison pour laquelle l'axiome
d'extensionnalité écrit sans égalité
(avoir les mêmes éléments implique avoir les
mêmes propriétés) est fragile à l'extrême.
Roland Hinnion (ULB): "Intensional positive sets"
Positive extensional set theory is well-known nowadays; here we
discuss the possibility of replacing extensionality by
intensionality; we compare the systems, and discuss also the
compatibility with ordinary (ZF-) sets. The main construction is a
(rather) simple forcing;the hope is to apply that later to analogue
(but still open) problems concerning partial sets...
Olivier Esser (ULB): "Topologie
et modèle de termes dans NF"
Dans cet exposé, nous étudierons diverses topologies
associées à NF et plus particulièrement la
topologie de Stone associée aux modèles de permutations
de NF: pour un modèle V de NF et une formule \phi, on
déclare ouvert les ensembles suivants {\sigma | V^{\sigma} |= \phi}
Thomas
Brihaye (UMH): "Bisimulations de
systèmes dynamiques et combinatoire des mots"
Dans cet exposé, je commencerai par rappeler la notion de
bisimulation entre deux systèmes de transition. Je la
comparerai ensuite avec la notion d'equivalence de langage (dans le
cas de systèmes finis). Le reste de l'exposé sera
consacré à une analyse combinatoire de la notion de
bisimulation entre systèmes dynamiques. On expliquera entre
autre comment encoder des trajectoires de systèmes continus
à travers des mots. Enfin, on donnera une étude
systématique de cette technique qui a été
introduite dans le but d'étudier les automates hybrides o-minimaux.
Felix
Klaedtke (ETH Zurich): "On the
Automata Size for Presburger Arithmetic"
Presburger arithmetic is the first-order theory with
addition and the ordering over the integers. Its decidability was
first proved independently by Presburger and Skolem by the method of
quantifier elimination. Its complexity has been investigated
intensively since. Due to the applicability of Presburger arithmetic
in various domains (e.g., system verification and compiler
optimization) it is important to have effective decision procedure
for Presburger arithmetic or fragments of it.
Recently, it has become popular to use automata for
deciding Presburger arithmetic. An idea that goes at least back to an
article by Buechi in 1960: Integers are represented as words (e.g.,
using the 2's complement representation), and the automata are
recursively constructed from the formulas. The constructed automaton
for a formula precisely accepts the words representing integers which
make the formula true. A crude complexity analysis on such an
automata-based decision procedure leads to a non-elementary
worst-case complexity. However, empirical results show that
automata-based decision procedures are competitive to other methods.
In this talk we analyze this automata-based approach.
Our analysis provides a triple exponential upper bound on the size of
the minimal deterministic automaton for a Presburger arithmetic
formula, and it partly explains the "good" empirical
results. Our analysis is based on a comparison of automata and
quantifier-free formulas that are obtained by an improvement of
Cooper's quantifier elimination method for Presburger arithmetic.
Moreover, we give an example showing that this triple exponential
upper bound on the automata size is tight (even for nondeterministic
automata). Slides
of the talk.
cours de DEA : Logique et Géométrie
Christian Michaux (UMH)
"Espaces définissables et quotients dans les
structures o-minimales, d'après van den Dries".
Dans cette série de lectures, nous introduirons la
catégorie d'espaces définissables dans le cadre des
structures o-minimales. Nous commencerons par montrer que cette
notion est indépendante de l'atlas sous-jacent et est
caractérisée par le faisceau induit. On montrera que
les espaces définissables affines sont exactement ceux dont la
topologie est régulière. Cette étendue sera
ensuite étendue aux groupes définissables (en
particulier linéaires algébriques) et à leur
quotients (sous une action). Ces résultats constituent une
extension de résultats de la géométrie
semi-algébrique réelle.
Fundamental Computer Science F.N.R.S. Contact Group:
The theme of the day will be « Constraints in
Computer Science ». This includes constraints in databases,
constraint programming, constraints in verification, constraints for
the modeling of combinatorial problems, constraints and logic.
Registration : registration is by email. If you wish
to participate in this FNRS day, please send your name and surname,
affiliation and email to the secretary of the group Prof. J.-F.
Raskin (jraskin@ulb.ac.be). There are no registration fees. The
closing date for registrations is october 1, 2004.
The schedule of the day is as follows:
9h : Welcome
9h15 - 10h : Alexander Serebrenik, "On
termination of binary CLP programs"
10h - 10h30 : Coffie break
10h30 -11h30 : Invited talk. Prof. B. Kuijpers
(University of Limburg) "Constraint Databases, Data Structures
and Efficient Query Evaluation"
11h30 - 12h15 : Floris Geert, "On the
decidability of termination of query evaluation in transitive closure
logics for polynomial constraint databases"
12h15 - 14h : Lunch break
14h -14h45 : Isabelle Dony, "A Program
Verification System Based on Oz"
14h45-15h30 : Louis Latour, "From Automata
to Formulas: Convex Integer Polyhedra"
15h30 - 16h : Coffie break
16h - 16h45 : Axel Legay, "Boolean Binary
Decision Diagrams (ongoing work)"
16h45-17h30 : Hadrien Mélot,
"Discovering optimal inequalities among graph invariants with
the help of a computer"
Here are the abstracts of the talks :
Alexander Serebrenik, "On termination
of binary CLP programs"
Termination of binary CLP programs has recently become
an important question in the termination analysis community. The
reason for this is due to the fact that some of the recent approaches
to termination of logic programs abstract the input program to a
binary CLP program and conclude termination of the input program from
termination of the abstracted program.
In this paper we introduce a class of binary CLP
programs such that their termination can be proved by using linear
level mappings. We show that membership to this class is decidable
and present a decision procedure.
Further, we extend this class to programs such that
their termination proofs require a combination of linear functions.
In particular we consider as level mappings tuples of linear
functions and piecewise linear functions.
Geert Floris: "On the decidability of
termination of query evaluation in transitive closure logics for
polynomial constraint databases".
In this talk we present extensions of first-order
logic with different types of transitive-closure operators and report
on decidability results related to the termination of the evaluation
of queries expressible in these transitive-closure logics on
constraint databases.
It turns out that termination is undecidable in
general. However, we identify some cases where the decision problem
becomes decidable, and even expressible in first-order logic over the
reals. Based on this result, we identify a particular
transitive-closure logic for which termination of query evaluation is
decidable and which is more expressive than first-order logic over
the reals.
Furthermore, we can define a guarded fragment in which
exactly the terminating queries of this language are expressible.
Isabelle Dony, "A Program Verification
System Based on Oz"
We present an imperative program verification system
that exploits many powerful aspects of Oz. Our verification system
supports an expressive assertion language for writing specifications
and loop invariants. It is able to prove the correctness of
elaborated imperative programs consisting of several subproblems that
are checked independently.
We illustrate the functionalities of our system on a
few non trivial examples. Then, we explain that, using Oz constraint
programming and other convenient programming mechanisms of Oz, the
implementation of the system is straightforward. We also provide
information about the efficiency of our implementation.
Louis Latour, "From Automata to
Formulas: Convex Integer Polyhedra"
Automata-based representations have recently been
investigated as a tool for representing and manipulating sets of
integer vectors. In this talk, we study some structural properties of
automata accepting the encodings (most significant digit first) of
the solutions of systems of linear Diophantine inequations, i.e.,
convex polyhedra in $\Z^n$. Based on those structural properties, we
develop an algorithm that takes as input an automaton and generates a
quantifier-free formula that represents exactly the set of integer
vectors accepted by the automaton.
Axel Legay, "Boolean Binary Decision
Diagrams (ongoing work)"
Verification of computer systems is now widely done
with the help of symbolic representations which allow the
manipulation of impressively large (or even infinite) sets of
configurations. Amount all symbolic representations, the BDD
representation is certainly the most used when considering systems
whose set of configurations can be encoded using a finite memory (for
example, bounded integers). One of the main advantages of the BDD
representation is that it allows to implement efficiently all
operations and tests needed by the state-space exploration process.
Hadrien Mélot, "Discovering
optimal inequalities among graph invariants
with the help of a computer"
During the last two decades, several attempts to
develop computer systems have been made in order to obtain new
conjectures in graph theory. These systems can be divided in two
classes : automated systems if they provide conjectures without human
intervention - except for the problem statement ? and computer-assisted
systems otherwise.
We present a new computer-assisted system (GraPHedron)
which uses a polyhedral approach to discover optimal linear
inequalities under certain constraints defined by a given class of
graphs and a selected set of graph invariants. Of course, the meaning
of "optimal inequality" will be precised and we will show
how the system can be used to identify such relations.
Archive des séminaires passés
Retour à la page de garde / Back to the homepage Page maintenue par Cédric Rivière