En poursuivant votre navigation sur ce site, vous acceptez l'utilisation d'un simple cookie d'identification. Aucune autre exploitation n'est faite de ce cookie. OK

Documents Critères de recherche : "2016" 246 résultats

Filtrer
Sélectionner : Tous / Aucun
Q
Déposez votre fichier ici pour le déplacer vers cet enregistrement.
y

Proof and computation in Coq - Théry, Laurent (Auteur de la Conférence) | CIRM H

Multi angle

In this talk, we are going to show on some elementary examples how computation can easily be incorporated inside proof in a proof system like Coq.

68N30 ; 68Q60 ; 68T15

Sélection Signaler une erreur
Déposez votre fichier ici pour le déplacer vers cet enregistrement.
y

Formal verification of numerical analysis programs - Boldo, Sylvie (Auteur de la Conférence) | CIRM H

Multi angle

From a (partial) differential equation to an actual program is a long road. This talk will present the formal verification of all the steps of this journey. This includes the mathematical error due to the numerical scheme (method error), that is usually bounded by pen-and-paper proofs. This also includes round-off errors due to the floating-point computations.
The running example will be a C program that implements a numerical scheme for the resolution of the one-dimensional acoustic wave equation. This program is annotated to specify both method error and round-off error, and formally verified using interactive and automatic provers. Some work in progress about the finite element method will also be presented.[-]
From a (partial) differential equation to an actual program is a long road. This talk will present the formal verification of all the steps of this journey. This includes the mathematical error due to the numerical scheme (method error), that is usually bounded by pen-and-paper proofs. This also includes round-off errors due to the floating-point computations.
The running example will be a C program that implements a numerical scheme for the ...[+]

68N30 ; 68Q60 ; 68N15 ; 65Y04 ; 65G50

Sélection Signaler une erreur
Déposez votre fichier ici pour le déplacer vers cet enregistrement.
y

Verified numerics for ODEs in Isabelle/HOL - Immler, Fabian (Auteur de la Conférence) | CIRM H

Multi angle

This talk is about verified numerical algorithms in Isabelle/HOL, with a focus on guaranteed enclosures for solutions of ODEs. The enclosures are represented by zonotopes, arising from the use of affine arithmetic. Enclosures for solutions of ODEs are computed by set-based variants of the well-known Runge-Kutta methods.
All of the algorithms are formally verified with respect to a formalization of ODEs in Isabelle/HOL: The correctness proofs are carried out for abstract algorithms, which are specified in terms of real numbers and sets. These abstract algorithms are automatically refined towards executable specifications based on lists, zonotopes, and software floating point numbers. Optimizations for low-dimensional, nonlinear dynamics allow for an application highlight: the computation of an accurate enclosure for the Lorenz attractor. This contributes to an important proof that originally relied on non-verified numerical computations.[-]
This talk is about verified numerical algorithms in Isabelle/HOL, with a focus on guaranteed enclosures for solutions of ODEs. The enclosures are represented by zonotopes, arising from the use of affine arithmetic. Enclosures for solutions of ODEs are computed by set-based variants of the well-known Runge-Kutta methods.
All of the algorithms are formally verified with respect to a formalization of ODEs in Isabelle/HOL: The correctness proofs are ...[+]

68T15 ; 34-04 ; 34A12 ; 37D45 ; 65G20 ; 65G30 ; 65G50 ; 65L70 ; 68N15 ; 68Q60 ; 68N30 ; 65Y04

Sélection Signaler une erreur
Déposez votre fichier ici pour le déplacer vers cet enregistrement.
y

Interview au CIRM : David Ruelle - Ruelle, David (Personne interviewée) | CIRM H

Post-edited

David Ruelle est professeur honoraire de Physique Théorique à l'Institut des Hautes Études Scientifiques (IHÉS). Il a reçu la médaille Matteucci en 2004, en 2006 le Prix Henri-Poincaré et en 2014 la Médaille Max-Planck pour l'ensemble de ses travaux.

Sélection Signaler une erreur
Déposez votre fichier ici pour le déplacer vers cet enregistrement.
y
There are five superstring theories, all formulated in 9+1 spacetime dimensions; lower-dimensional theories are studied by taking some of the spatial dimensions to be compact (and small). One of the remarkable features of this setup is that the same lower-dimensional theory can often be realized by pairing different superstring theories with different geometries. The focus of these lectures will be on the mathematical implications of some of these physical “dualities.”
Our main focus from the string theory side will be the superstring theories known as type IIA and type IIB. The duality phenomenon occurs for compact spaces of various dimensions and types. We will begin by discussing “T-duality” which uses tori as the compact spaces. We will then digress to introduce M-theory as a strong-coupling limit of the type IIA string theory, and F-theory as a variant of the type IIB string theory whose existence is motivated by T-duality. The next topic is compactifying the type IIA and IIB string theories on K3 surfaces (where the duality involves a change of geometric parameters but not a change of string theory).
By the third lecture, we will have turned our attention to Calabi-Yau manifolds of higher dimension, and the “mirror symmetry” which relates pairs of them. Various aspects of mirror symmetry have various mathematical implications, and we will explain how these are conjecturally related to each other.[-]
There are five superstring theories, all formulated in 9+1 spacetime dimensions; lower-dimensional theories are studied by taking some of the spatial dimensions to be compact (and small). One of the remarkable features of this setup is that the same lower-dimensional theory can often be realized by pairing different superstring theories with different geometries. The focus of these lectures will be on the mathematical implications of some of ...[+]

14J32 ; 14J33 ; 81T30

Sélection Signaler une erreur
Déposez votre fichier ici pour le déplacer vers cet enregistrement.
2y

Interview at CIRM: Pavel Exner - Exner, Pavel (Personne interviewée) | CIRM H

Post-edited

Pavel Exner from the Academy of Sciences of the Czech Republic in Prague is president of the European Mathematical Society (2015-2018). He's currently also the scientific director at the Doppler Institute for Mathematical Physics and Applied Mathematics in Prague.

Sélection Signaler une erreur
Déposez votre fichier ici pour le déplacer vers cet enregistrement.
y

A derivation on the field of d.c.e.reals - Miller, Joseph (Auteur de la Conférence) | CIRM H

Multi angle

Barmpalias and Lewis-Pye recently proved that if $\alpha$ and $\beta$ are (Martin-Löf) random left-c.e. reals with left-c.e. approximations $\{\alpha_s \}_{s \in\ omega}$ and $\{\beta_s \}_{s \in\ omega}$, then
\[
\begin{equation}
\frac{\partial\alpha}{\partial\beta} = \lim_{s\to\infty} \frac{\alpha-\alpha_s}{\beta-\beta_s}.
\end{equation}
\]
converges and is independent of the choice of approximations. Furthermore, they showed that $\partial\alpha/\partial\beta = 1$ if and only if $\alpha-\beta$ is nonrandom; $\partial\alpha/\partial\beta>1$ if and only if $\alpha-\beta$ is a random left-c.e. real; and $\partial\alpha/\partial\beta<1$ if and only if $\alpha-\beta$ is a random right-c.e. real.

We extend their results to the d.c.e. reals, which clarifies what is happening. The extension is straightforward. Fix a random left-c.e. real $\Omega$ with approximation $\{\Omega_s\}_{s\in\omega}$. If $\alpha$ is a d.c.e. real with d.c.e. approximation $\{\alpha_s\}_{s\in\omega}$, let
\[
\partial\alpha = \frac{\partial\alpha}{\partial\Omega} = \lim_{s\to\infty} \frac{\alpha-\alpha_s}{\Omega-\Omega_s}.
\]
As above, the limit exists and is independent of the choice of approximations. Now $\partial\alpha=0$ if and only if $\alpha$ is nonrandom; $\partial\alpha>0$ if and only if $\alpha$ is a random left-c.e. real; and $\partial\alpha<0$ if and only if $\alpha$ is a random right-c.e. real.

As we have telegraphed by our choice of notation, $\partial$ is a derivation on the field of d.c.e. reals. In other words, $\partial$ preserves addition and satisfies the Leibniz law:
\[
\partial(\alpha\beta) = \alpha\,\partial\beta + \beta\,\partial\alpha.
\]
(However, $\partial$ maps outside of the d.c.e. reals, so it does not make them a differential field.) We will see how the properties of $\partial$ encapsulate much of what we know about randomness in the left-c.e. and d.c.e. reals. We also show that if $f\colon\mathbb{R}\rightarrow\mathbb{R}$ is a computable function that is differentiable at $\alpha$, then $\partial f(\alpha) = f'(\alpha)\,\partial\alpha$. This allows us to apply basic identities from calculus, so for example, $\partial\alpha^n = n\alpha^{n-1}\,\partial\alpha$ and $\partial e^\alpha = e^\alpha\,\partial\alpha$. Since $\partial\Omega=1$, we have $\partial e^\Omega = e^\Omega$.

Given a derivation on a field, the elements that it maps to zero also form a field: the $ \textit {field of constants}$. In our case, these are the nonrandom d.c.e. reals. We show that, in fact, the nonrandom d.c.e. reals form a $ \textit {real closed field}$. Note that it was not even known that the nonrandom d.c.e. reals are closed under addition, and indeed, it is easy to prove the convergence of [1] from this fact. In contrast, it has long been known that the nonrandom left-c.e. reals are closed under addition (Demuth [2] and Downey, Hirschfeldt, and Nies [3]). While also nontrivial, this fact seems to be easier to prove. Towards understanding this difference, we show that the real closure of the nonrandom left-c.e. reals is strictly smaller than the field of nonrandom d.c.e. reals. In particular, there are nonrandom d.c.e. reals that cannot be written as the difference of nonrandom left-c.e. reals; despite being nonrandom, they carry some kind of intrinsic randomness.[-]
Barmpalias and Lewis-Pye recently proved that if $\alpha$ and $\beta$ are (Martin-Löf) random left-c.e. reals with left-c.e. approximations $\{\alpha_s \}_{s \in\ omega}$ and $\{\beta_s \}_{s \in\ omega}$, then
\[
\begin{equation}
\frac{\partial\alpha}{\partial\beta} = \lim_{s\to\infty} \frac{\alpha-\alpha_s}{\beta-\beta_s}.
\end{equation}
\]
converges and is independent of the choice of approximations. Furthermore, they showed that $\p...[+]

03D28 ; 03D80 ; 03F60 ; 68Q30

Sélection Signaler une erreur
Déposez votre fichier ici pour le déplacer vers cet enregistrement.
y

Challenges in the management of ecological populations - Hastings, Alan (Auteur de la Conférence) | CIRM H

Multi angle

I will focus both on two specific examples, coral reefs and management of an invasive cordgrass as well as more general issues. The challenges will include understanding the time scales of responses that result from biological constraints, the presence of multiple objectives, the difficulty of dealing with tipping points, and the desirability of minimizing cost.

92D40 ; 37N25

Sélection Signaler une erreur
Déposez votre fichier ici pour le déplacer vers cet enregistrement.
y

Les mobiles au sein d'un réseau de laboratoire - Bordères, Serge (Auteur de la Conférence) | CIRM H

Multi angle

Le contexte particulier introduit par les BYOD (Bring Your Own Device).
Connaissance utiles pour l'administrateur réseau : structure du système et sécurité.
Mise en oeuvre de services (Wifi, certificats, vpn, impressions...).

68U35 ; 68P25 ; 68M10

Sélection Signaler une erreur
Déposez votre fichier ici pour le déplacer vers cet enregistrement.
2y
Let $p$ be a prime number and $F$ be a non-archimedean field with finite residue class field of characteristic $p$. Understanding the category of Iwahori-Hecke modules for $SL_2(F)$ is of great interest in the study of $p$-modular smooth representations of $SL_2(F)$, as these modules naturally show up as spaces of invariant vectors under the action of the standard pro-$p$-Iwahori subgroup. In this talk, we will discuss a work in progress in which we aim to classify all non-trivial extensions between these modules and to compare them with their analogues for $p$-modular smooth representations of $SL_2(F)$ and with their Galois counterpart in the setting of the local Langlands correspondences in natural characteristic.[-]
Let $p$ be a prime number and $F$ be a non-archimedean field with finite residue class field of characteristic $p$. Understanding the category of Iwahori-Hecke modules for $SL_2(F)$ is of great interest in the study of $p$-modular smooth representations of $SL_2(F)$, as these modules naturally show up as spaces of invariant vectors under the action of the standard pro-$p$-Iwahori subgroup. In this talk, we will discuss a work in progress in ...[+]

11F70 ; 11F85 ; 20C08 ; 20G05 ; 22E50

Sélection Signaler une erreur