Jurnal Edukasi
Not a member yet
4879 research outputs found
Sort by
Certification of real inequalities: templates and sums of squares
No full textAlso arXiv:1403.5899International audienceWe consider the problem of certifying lower bounds for real-valued multivariate transcendental functions. The functions we are dealing with are nonlinear and involve semialgebraic operations as well as some transcendental functions like cos, arctan, exp, etc. Our general framework is to use different approximation methods to relax the original problem into polynomial optimization problems, which we solve by sparse sums of squares relaxations. In particular, we combine the ideas of the maxplus approximations (originally introduced in optimal control) and of the linear templates (originally introduced in static analysis by abstract interpretation). The nonlinear templates control the complexity of the semialgebraic relaxations at the price of coarsening the maxplus approximations. In that way, we arrive at a new—template based—certified global optimization method, which exploits both the precision of sums of squares relaxations and the scalability of abstraction methods. We analyze the performance of the method on problems from the global optimization literature, as well as medium-size inequalities issued from the Flyspeck project
A minimum effort optimal control problem for the wave equation.
No full textInternational audienceA minimum effort optimal control problem for the undamped waveequation is considered which involves L∞–control costs. Since the problem isnon-differentiable a regularized problem is introduced. Uniqueness of the solu-tion of the regularized problem is proven and the convergence of the regularizedsolutions is analyzed. Further, a semi-smooth Newton method is formulatedto solve the regularized problems and its superlinear convergence is shown.Thereby special attention has to be paid to the well-posedness of the Newtoniteration. Numerical examples confirm the theoretical results
Polarities & Focussing: a journey from Realisability to Automated Reasoning
No full textThis dissertation explores the roles of polarities and focussing in various aspects of Computational Logic.These concepts play a key role in the the interpretation of proofs as programs, a.k.a. the Curry-Howard correspondence, in the context of classical logic. Arising from linear logic, they allow the construction of meaningful semantics for cut-elimination in classical logic, some of which relate to the Call-by-Name and Call-by-Value disciplines of functional programming. The first part of this dissertation provides an introduction to these interpretations, highlighting the roles of polarities and focussing. For instance: proofs of positive formulae provide structured data, while proofs of negative formulae consume such data; focussing allows the description of the interaction between the two kinds of proofs as pure pattern-matching. This idea is pushed further in the second part of this dissertation, and connected to realisability semantics, where the structured data is interpreted algebraically, and the consumption of such data is modelled with the use of an orthogonality relation. Most of this part has been proved in the Coq proof assistant.Polarities and focussing were also introduced with applications to logic programming in mind, where computation is proof-search. In the third part of this dissertation, we push this idea further by exploring the roles that these concepts can play in other applications of proof-search, such as theorem proving and more particularly automated reasoning. We use these concepts to describe the main algorithm of SAT-solvers and SMT-solvers: DPLL. We then describe the implementation of a proof-search engine called Psyche. Its architecture, based on the concept of focussing, offers a platform where smart techniques from automated reasoning (or a user interface) can safely and trustworthily be implemented via the use of an API
A Storage-Efficient and Robust Private Information Retrieval Scheme Allowing Few Servers
No full textInternational audienceSince the concept of locally decodable codes was introduced by Katz and Trevisan in 2000, it is well-known that information the-oretically secure private information retrieval schemes can be built using locally decodable codes. In this paper, we construct a Byzantine ro-bust PIR scheme using the multiplicity codes introduced by Kopparty et al. Our main contributions are on the one hand to avoid full replica-tion of the database on each server; this significantly reduces the global redundancy. On the other hand, to have a much lower locality in the PIR context than in the LDC context. This shows that there exists two different notions: LDC-locality and PIR-locality. This is made possible by exploiting geometric properties of multiplicity codes
Discretization Orders for Protein Side Chains
No full textInternational audienceProteins are important molecules that are widely studied in biology. Since their three-dimensional conformations can give clues about their function, an optimal methodology for the identification of such conformations has been researched for many years. Experiments of Nuclear Magnetic Resonance (NMR) are able to estimate distances between some pairs of atoms forming the protein, and the problem of identifying the possible conformations satisfying the available distance constraints is known in the scientific literature as the Molecular Distance Geometry Problem (MDGP). When some particular assumptions are satisfied, MDGP instances can be discretized, and solved by employing an ad-hoc algorithm, named the interval Branch & Prune (iBP). When dealing with molecules such as proteins, whose chemical structure is known, a priori information can be exploited for generating atomic orderings that allow for the discretization. In previous publications, we presented a handcrafted order for the protein backbones. In this work, we propose 20 new orders for the 20 side chains that can be present in proteins. Computational experiments on artificial and real instances from NMR show the usefulness of the proposed orders
Symmetric Normalisation for Intuitionistic Logic
No full textInternational audienceWe present two proof systems for implication-only intuitionistic logic in the calculus of structures. The first is a direct adaptation of the standard sequent calculus to the deep inference setting, and we describe a procedure for cut elimination, similar to the one from the sequent calculus, but using a non-local rewriting. The second system is the symmetric completion of the first, as normally given in deep inference for logics with a DeMorgan duality: all inference rules have duals, as cut is dual to the identity axiom. We prove a generalisation of cut elimination, that we call symmetric normalisation, where all rules dual to standard ones are permuted up in the derivation. The result is a decomposition theorem having cut elimination and interpolation as corollaries
Rayonnements Secondaires Cohérents Émis lors de la Filamentation Laser Femtoseconde
No full textLaser filamentation is a nonlinear optical phenomenon which appears spontaneously during the propagation of an intense ultrashort laser pulse in a transparent medium, when the pulse peak power exceeds a critical value (several Gigawatts in air). At such an intensity level the beam tends to collapse due to the optical Kerr self-focusing effect until the intensity is high enough to ionize the medium, giving rise to a defocusing plasma. Thereafter, a dynamic competition between these two effects takes place, leaving a thin and weakly ionized plasma channel in the wake of the pulse. Following its discovery in 1995, femtosecond laser filamentation in air has attracted considerable interest because of the rich physics involved in the process and the wide range of potential applications (remote sensing, light frequency conversion, laser-based weather control, Terahertz generation, etc.).This thesis is devoted to the study of the coherent secondary emission from femtosecond laser filaments in gases. First, the ultraviolet luminescence of plasma filaments, corresponding to transitions of excited neutral and ionic molecular Nitrogen, is studied. I demonstrate that this luminescence depends strongly on the polarization state of the incident laser pulses. I further report and interpret for the first time a strong optical gain in the backward direction from plasma filaments created by circularly polarized 800 nm femtosecond laser pulses at normal pressure. This effect is a significant step towards the realization of a “laser in the sky”. In the last part of the thesis, I discuss the Terahertz generation from multiple femtosecond laser filaments in air. The coherent synthesis of the Terahertz radiation from an array of filaments is demonstrated, showing the capability for energy scaling up and directionality control of the Terahertz emission.La filamentation laser est un phénomène optique non-linéaire qui apparaît spontanément au cours de la propagation d’une impulsion laser ultracourte intense dans un milieu transparent, quand sa puissance crête dépasse une valeur critique (quelques Gigawatts dans l’air). A un tel niveau d’intensité le faisceau a tendance à se contracter en raison de l’effet Kerr optique jusqu’à ce que l’intensité devienne suffisamment élevée pour ioniser le milieu, donnant naissance à un plasma de défocalisation. Par la suite, une compétition dynamique entre ces deux effets a lieu, produisant un canal de plasma mince et faiblement ionisé dans le sillage de l’impulsion. Depuis sa découverte en 1995, la filamentation laser femtoseconde dans l’air a suscité un intérêt considérable en raison de la physique riche impliquée dans ce processus et de la large gamme d’applications potentielles (détection à distance, conversion de fréquences optiques, contrôle atmosphérique par laser, génération d’ondes Térahertz, etc.).Cette thèse est consacrée principalement à l’étude des rayonnements secondaires cohérents émis lors de la filamentation femtoseconde dans les gaz. Tout d’abord, je me suis intéressé à la luminescence ultraviolet des filaments de plasma, qui est associée à les transitions de l’azote moléculaire neutre et ionique dans un état excité. J’ai démontré que cette luminescence dépend fortement de l’état de polarisation des impulsions laser incidentes. J’ai ensuite décrit et interprété pour la première fois l’apparition d’un gain optique important observé vers l’arrière de la colonne de plasma dans l’azote. Ce gain apparait lorsque les impulsions laser femtoseconde à 800 nm sont polarisées circulairement et à pression atmosphérique. Cet effet constitue une étape importante vers la réalisation d’un “laser dans le ciel”. La dernière partie de la thèse, porte sur la génération du rayonnement Térahertz par plusieurs filaments laser femtoseconde. Par la synthèse cohérente du rayonnement Térahertz d’un réseau de filaments, j’ai ainsi démontré la possibilité d’accroitre l’intensité Térahertz et de contrôler la directivité de ce rayonnement par l’organisation de filaments multiples
Beta Reduction is Invariant, Indeed
No full textInternational audienceSlot and van Emde Boas' weak invariance thesis states that reasonable machines can simulate each other within a polynomially overhead in time. Is λ-calculus a reasonable machine? Is there a way to measure the computational complexity of a λ-term? This paper presents the first complete positive answer to this long-standing problem. Moreover, our answer is completely machine-independent and based over a standard notion in the theory of λ-calculus: the length of a leftmost-outermost derivation to normal form is an invariant cost model. Such a theorem cannot be proved by directly relating λ-calculus with Turing machines or random access machines, because of the size explosion problem: there are terms that in a linear number of steps produce an exponentially long output. The first step towards the solution is to shift to a notion of evaluation for which the length and the size of the output are linearly related. This is done by adopting the linear substitution calculus (LSC), a calculus of explicit substitutions modelled after linear logic and proof-nets and admitting a decomposition of leftmost-outermost derivations with the desired property. Thus, the LSC is invariant with respect to, say, random access machines. The second step is to show that LSC is invariant with respect to the λ-calculus. The size explosion problem seems to imply that this is not possible: having the same notions of normal form, evaluation in the LSC is exponentially longer than in the λ-calculus. We solve such an impasse by introducing a new form of shared normal form and shared reduction, deemed useful. Useful evaluation avoids those steps that only unshare the output without contributing to β-redexes, i.e., the steps that cause the blow-up in size
A Two-Level Logic Approach to Reasoning about Typed Specification Languages
No full textInternational audienceThe two-level logic approach (2LL) to reasoning about computational specifications, as implemented by the Abella theorem prover, represents derivations of a specification language as an inductive definition in a reasoning logic. This approach has traditionally been formulated with the specification and reasoning logics having the same type system, and only the formulas being translated. However, requiring identical type systems limits the approach in two important ways: (1) every change in the specification language's type system requires a corresponding change in that of the reasoning logic, and (2) the same reasoning logic cannot be used with two specification languages at once if they have incompatible type systems. We propose a technique based on adequate encodings of the types and judgements of a typed specification language in terms of a simply typed higher-order logic program, which is then used for reasoning about the specification language in the usual 2LL. Moreover, a single specification logic implementation can be used as a basis for a number of other specification languages just by varying the encoding. We illustrate our technique with an implementation of the LF dependent type theory as a new specification language for Abella, co-existing with its current simply typed higher-order hereditary Harrop specification logic, without modifying the type system of its reasoning logic
Random maps
No full textInternational audienceThis is a quick survey on some recent works done in the field of random maps