882 research outputs found
Funiculaire Neuveville-Saint-Pierre Fribourg : étude technique et financière
No full textpar les concessionnaires Blancpain & fils, E. Strub, E. LommelGeschenkexlibris-Etikette: "Geschenk aus dem Nachlasse von August Waldner" 002230365_0001 Exemplar der ETH-BIBIndirektes handschriftliches Exlibris: "1907, 136", das ist August Waldner 002194263_0003 Exemplar der ETH-BI
Coq Modulo Theory
No full textInternational audienceCoq Modulo Theory (CoqMT) is an extension of the Coq proof assistant incorporating, in its computational mechanism, validity entailment for user-defined first-order equational theories. Such a mechanism strictly enriches the system (more terms are typable), eases the use of dependent types and provides more automation during the development of proofs. CoqMT improves over the Calculus of Congruent Inductive Constructions by getting rid of various restrictions and simplifying the type-checking algorithm and the integration of first-order decision procedures. We present here CoqMT, and outline its meta-theoretical study. We also give a brief description of our CoqMT implementation
Implementing a term rewriting engine for the EasyCrypt framework
No full textLa sociedad depende hoy más que nunca de la tecnología, pero la inversión en seguridad
es escasa y los sistemas informáticos siguen estando muy lejos de ser seguros.
La criptografía es una de las piedras angulares de la seguridad en este ámbito, por
lo que recientemente se ha dedicado una cantidad considerable de recursos al desarrollo
de herramientas que ayuden en la evaluación y mejora de los algoritmos
criptográficos. EasyCrypt es uno de estos sistemas, desarrollado recientemente en
el Instituto IMDEA Software en respuesta a la creciente necesidad de disponer de
herramientas fiables de verificación formal de criptografía.
En este trabajo se abordará la implementación de una mejora en el reductor de términos
de EasyCrypt, sustituyéndolo por una máquina abstracta simbólica. Para ello
se estudiarán e implementarán previamente dos máquinas abstractas muy conocidas,
la Máquina de Krivine y la ZAM, introduciendo variaciones sobre ellas y estudiando
sus diferencias desde un punto de vista práctico.---ABSTRACT---Today, society depends more than ever on technology, but the investment in security
is still scarce and using computer systems are still far from safe to use. Cryptography
is one of the cornerstones of security, so there has been a considerable amount
of effort devoted recently to the development of tools oriented to the evaluation
and improvement of cryptographic algorithms. One of these tools is EasyCrypt,
developed recently at IMDEA Software Institute in response to the increasing need
of reliable formal verification tools for cryptography.
This work will focus on the improvement of the EasyCrypt’s term rewriting system,
replacing it with a symbolic abstract machine. In order to do that, we will previously
study and implement two widely known abstract machines, the Krivine Machine and
the ZAM, introducing some variations and studying their differences from a practical
point of view
Pour une agriculture durable et solidaire: Soirée-débat organisée à Melesse (Ille-et-Vilaine) par le Conseil de développement de la Communauté de communes Val-d’Ille-Aubigné (Codevia) autour du film « La révolution verte. Europe, un continent bouleversé » et du projet « Terres de Sources », dans le cadre du festival Alimenterre
No full textActivité de valorisation scientifique et d'échange autour de projets locaux à l'intention de la population.A l’invitation du Conseil de développement de la Communauté de communes Val-d’Ille-Aubigné (Codevia), dans le cadre du festival Alimenterre, un buffet proposé par la ferme Pradenn, une projection du film ‘La révolution verte. Europe, un continent bouleversé’ et une présentation de ‘Terres de Sources’ outil économique pour la transition agroécologique et alimentaire des territoires porté par la Collectivité Eau du Bassin Rennais (CEBR) ont donné lieu à un échange entre une assistance nombreuse (environ 70 personnes) et quatre intervenant-e-s : Véronique Chable (agronome au laboratoire INRAe Bagap et membre du réseau Semences paysannes), Aulne Sauvée (artisan charcutier-cuisinier à la ferme Pradenn), Pierre Strub (chargé de mission Terres de sources à la CEBR) et Yvon Le Caro (géographe au laboratoire CNRS Espaces et sociétés, Université Rennes 2). La soirée a été animée par le Codevia.Trois principaux thèmes ont été abordés. D’une part l’évolution de l’agriculture dans son rapport à la nature, à la population urbaine, à l’alimentation, en mettant en relation le contexte de la Politique agricole commune (PAC) et les pratiques des agriculteurs. D’autre part les facteurs qui soutiennent ou qui freinent la nécessaire ‘transition’ en cours dans les systèmes agri-alimentaires européens, dans le contexte mondial du réchauffement climatique, de la perte de biodiversité et de l’épuisement des ressources. Enfin le rôle des citoyens, des consommateurs et des collectivités a été discuté, les pistes d’actions concrètes ne pouvant ignorer les contradictions d’une société devenue urbaine et consumériste
Pour une agriculture durable et solidaire: Soirée-débat organisée à Melesse (Ille-et-Vilaine) par le Conseil de développement de la Communauté de communes Val-d’Ille-Aubigné (Codevia) autour du film « La révolution verte. Europe, un continent bouleversé » et du projet « Terres de Sources », dans le cadre du festival Alimenterre
No full textActivité de valorisation scientifique et d'échange autour de projets locaux à l'intention de la population.A l’invitation du Conseil de développement de la Communauté de communes Val-d’Ille-Aubigné (Codevia), dans le cadre du festival Alimenterre, un buffet proposé par la ferme Pradenn, une projection du film ‘La révolution verte. Europe, un continent bouleversé’ et une présentation de ‘Terres de Sources’ outil économique pour la transition agroécologique et alimentaire des territoires porté par la Collectivité Eau du Bassin Rennais (CEBR) ont donné lieu à un échange entre une assistance nombreuse (environ 70 personnes) et quatre intervenant-e-s : Véronique Chable (agronome au laboratoire INRAe Bagap et membre du réseau Semences paysannes), Aulne Sauvée (artisan charcutier-cuisinier à la ferme Pradenn), Pierre Strub (chargé de mission Terres de sources à la CEBR) et Yvon Le Caro (géographe au laboratoire CNRS Espaces et sociétés, Université Rennes 2). La soirée a été animée par le Codevia.Trois principaux thèmes ont été abordés. D’une part l’évolution de l’agriculture dans son rapport à la nature, à la population urbaine, à l’alimentation, en mettant en relation le contexte de la Politique agricole commune (PAC) et les pratiques des agriculteurs. D’autre part les facteurs qui soutiennent ou qui freinent la nécessaire ‘transition’ en cours dans les systèmes agri-alimentaires européens, dans le contexte mondial du réchauffement climatique, de la perte de biodiversité et de l’épuisement des ressources. Enfin le rôle des citoyens, des consommateurs et des collectivités a été discuté, les pistes d’actions concrètes ne pouvant ignorer les contradictions d’une société devenue urbaine et consumériste
Pour une agriculture durable et solidaire: Soirée-débat organisée à Melesse (Ille-et-Vilaine) par le Conseil de développement de la Communauté de communes Val-d’Ille-Aubigné (Codevia) autour du film « La révolution verte. Europe, un continent bouleversé » et du projet « Terres de Sources », dans le cadre du festival Alimenterre
No full textActivité de valorisation scientifique et d'échange autour de projets locaux à l'intention de la population.A l’invitation du Conseil de développement de la Communauté de communes Val-d’Ille-Aubigné (Codevia), dans le cadre du festival Alimenterre, un buffet proposé par la ferme Pradenn, une projection du film ‘La révolution verte. Europe, un continent bouleversé’ et une présentation de ‘Terres de Sources’ outil économique pour la transition agroécologique et alimentaire des territoires porté par la Collectivité Eau du Bassin Rennais (CEBR) ont donné lieu à un échange entre une assistance nombreuse (environ 70 personnes) et quatre intervenant-e-s : Véronique Chable (agronome au laboratoire INRAe Bagap et membre du réseau Semences paysannes), Aulne Sauvée (artisan charcutier-cuisinier à la ferme Pradenn), Pierre Strub (chargé de mission Terres de sources à la CEBR) et Yvon Le Caro (géographe au laboratoire CNRS Espaces et sociétés, Université Rennes 2). La soirée a été animée par le Codevia.Trois principaux thèmes ont été abordés. D’une part l’évolution de l’agriculture dans son rapport à la nature, à la population urbaine, à l’alimentation, en mettant en relation le contexte de la Politique agricole commune (PAC) et les pratiques des agriculteurs. D’autre part les facteurs qui soutiennent ou qui freinent la nécessaire ‘transition’ en cours dans les systèmes agri-alimentaires européens, dans le contexte mondial du réchauffement climatique, de la perte de biodiversité et de l’épuisement des ressources. Enfin le rôle des citoyens, des consommateurs et des collectivités a été discuté, les pistes d’actions concrètes ne pouvant ignorer les contradictions d’une société devenue urbaine et consumériste
Pour une agriculture durable et solidaire: Soirée-débat organisée à Melesse (Ille-et-Vilaine) par le Conseil de développement de la Communauté de communes Val-d’Ille-Aubigné (Codevia) autour du film « La révolution verte. Europe, un continent bouleversé » et du projet « Terres de Sources », dans le cadre du festival Alimenterre
No full textActivité de valorisation scientifique et d'échange autour de projets locaux à l'intention de la population.A l’invitation du Conseil de développement de la Communauté de communes Val-d’Ille-Aubigné (Codevia), dans le cadre du festival Alimenterre, un buffet proposé par la ferme Pradenn, une projection du film ‘La révolution verte. Europe, un continent bouleversé’ et une présentation de ‘Terres de Sources’ outil économique pour la transition agroécologique et alimentaire des territoires porté par la Collectivité Eau du Bassin Rennais (CEBR) ont donné lieu à un échange entre une assistance nombreuse (environ 70 personnes) et quatre intervenant-e-s : Véronique Chable (agronome au laboratoire INRAe Bagap et membre du réseau Semences paysannes), Aulne Sauvée (artisan charcutier-cuisinier à la ferme Pradenn), Pierre Strub (chargé de mission Terres de sources à la CEBR) et Yvon Le Caro (géographe au laboratoire CNRS Espaces et sociétés, Université Rennes 2). La soirée a été animée par le Codevia.Trois principaux thèmes ont été abordés. D’une part l’évolution de l’agriculture dans son rapport à la nature, à la population urbaine, à l’alimentation, en mettant en relation le contexte de la Politique agricole commune (PAC) et les pratiques des agriculteurs. D’autre part les facteurs qui soutiennent ou qui freinent la nécessaire ‘transition’ en cours dans les systèmes agri-alimentaires européens, dans le contexte mondial du réchauffement climatique, de la perte de biodiversité et de l’épuisement des ressources. Enfin le rôle des citoyens, des consommateurs et des collectivités a été discuté, les pistes d’actions concrètes ne pouvant ignorer les contradictions d’une société devenue urbaine et consumériste
Théorie des Types et Procédures de Décision
No full textThe goal of this thesis is to develop a logical system in which formal proofs of mathematical statements can be carried out in a way which is close to mathematical practice. Our main contribution is the definition and study of a new calculus, the Calculus of Congruent and Inductive Constructions, an extension of the Calculus of Inductive Constructions (CIC) integrating in its computational part the entailment relation - via decision procedures - of a first order theory over equality. A major technical innovation of this work lies in the computational mechanism: goals are sent to the decision procedure together with a set of user hypotheses available from the current context. Our main results show that this extension of CIC does not compromise its main properties: confluence, strong normalization, consistency and decidability of proof checking are all preserved (as soon as the incorporated theory is itself decidable). As such, our calculus can be seen as a decidable restriction of the Extensional Calculus of Constructions. It can therefore serve as the basis for an extension of the Coq proof assistant.Le but de cette thèse est l'étude d'un système logique formel dans lequel les preuves formelles de propriétés mathématiques sont menées dans un style plus proches des pratiques des mathématiciens. Notre principal apport est la définition et l'étude du Calcul des Constructions Inductives Congruentes, une extension du Calcul des Constructions Inductives (CIC), intégrant au sein de son mécanisme de calcul des procédures de décisions pour des théories equationnelles au premier ordre. Nous montrons que ce calcul possède toutes les propriétés attendues: confluence, normalisation forte, cohérence logique et décidabilité de la vérification de types sont préservées. En tant que tel, notre calcul peut être vu comme une restriction décidable du Calcul des Constructions Extentionnelles et peut servir comme base pour l'extension de l'assistant à la preuve Coq
*-Liftings for Differential Privacy
No full textRecent developments in formal verification have identified approximate liftings (also known as approximate couplings) as a clean, compositional abstraction for proving differential privacy. There are two styles of definitions for this construction. Earlier definitions require the existence of one or more witness distributions, while a recent definition by Sato uses universal quantification over all sets of samples. These notions have different strengths and weaknesses: the universal version is more general than the existential ones, but the existential versions enjoy more precise composition principles.
We propose a novel, existential version of approximate lifting, called *-lifting, and show that it is equivalent to Sato's construction for discrete probability measures. Our work unifies all known notions of approximate lifting, giving cleaner properties, more general constructions, and more precise composition theorems for both styles of lifting, enabling richer proofs of differential privacy. We also clarify the relation between existing definitions of approximate lifting, and generalize our constructions to approximate liftings based on f-divergences
Unsolvability of the Quintic Formalized in Dependent Type Theory
No full textInternational audienceIn this paper, we describe an axiom-free Coq formalization that there does not exists a general method for solving by radicals polynomial equations of degree greater than 4. This development includes a proof of Galois’ Theorem of the equivalence between solvable extensions and extensionssolvable by radicals. The unsolvability of the general quintic follows from applying this theorem to a well chosen polynomial with unsolvable Galois group
- …
