Dans cette thèse, nous visons à formaliser les effets calculatoires. En effet, les langages de programmation les plus utilisés impliquent différentes sortes d'effets de bord: changement d'état, exceptions, entrées / sorties, non-déterminisme, etc. Ils peuvent apporter facilité et flexibilité dans le processus de codage. Cependant, le problème est de prendre en compte les effets lorsque l'on veut prouver des propriétés de programmes. La principale difficulté dans ce genre de preuve de programmes est le décalage entre la syntaxe des opérations avec effets de bord et leur interprétation. Typiquement, un fragment de programme avec des arguments de type X qui retourne une valeur de type Y n'est pas interprété comme une fonction de X vers Y , à cause des effets.L'approche algébrique la plus connue pour ce problème permet une interprétation des programmes, y compris ceux comportant des effets, en utilisant des monades : l'interprétation est une fonction de X vers T (Y ) où T est une monade. Cette approche a été étendue aux théories de Lawvere et aux "gestionnaires algébriques" (algebraic handlers). Une autre approche, appelée logique décorée, fournit une sémantique équationnelle pour ces programmes. Nous spécialisons l'approche de la logique décorée pour les effets liés à l'état de la mémoire et à la gestion des exceptions en définissant la logique décorée pour les états (L_st) et la logique décorée pour les exceptions (L_exc), respectivement. Elles nous permettent de prouver des propriétés de programmes impliquant de tels effets. Ensuite, nous formalisons ces logiques en Coq et certifions les preuves associées. Ces logiques sont construites de manière à être correctes. En outre, nous introduisons une notion de complétude syntaxique relative d'une théorie dans une logique donnée par rapport à une sous-logique. Nous montrons que la théorie décorée pour les états globaux ainsi que deux théories décorées pour les exceptions sont relativement complets relativement à leur sous-logique pure. Non seulement nous pouvons utiliser le système développé pour prouver des programmes comportant des effets, mais également nous utilisons cette formalisation pour certifier les résultats de complétude obtenus. / In this thesis, we aim to formalize the effects of a computation. Indeed, most used programming languages involve different sorts of effects: state change, exceptions, input/output, non-determinism, etc. They may bring ease and flexibility to the coding process. However, the problem is to take into account the effects when proving the properties of programs. The major difficulty in such kind of reasoning is the mismatch between the syntax of operations with effects and their interpretation. Typically, a piece of program with arguments in X that returns a value in Y is not interpreted as a function from X to Y , due to the effects. The best-known algebraic approach to the problem interprets programs including effects with the use of monads: the interpretation is a function from X to T(Y) where T is a monad. This approach has been extendedto Lawvere theories and algebraic handlers. Another approach called, the decorated logic, provides a sort of equational semantics for reasoning about programs with effects. We specialize the approach of decorated logic to the state and the exceptions effects by defining the decorated logic for states (L_st) and the decorated logic for exceptions (L_exc), respectively. This enables us to prove properties of programs involving such effects. Then, we formalize these logics in Coq and certify the related proofs. These logics are built so as to be sound. In addition, we introduce a relative notion of syntactic completeness of a theory in a given logic with respect to a sublogic. We prove that the decorated theory for the global states as well as two decorated theories for exceptions are syntactically complete relatively to their pure sublogics. These proofs are certified in Coq as applications of ourgeneric frameworks.

This dissertation aims at presenting and discussing the proofs for immortality of the soul in Book I of the Tusculan Disputations by Cicero, a philosophical work written in the form of a dialogue in which why man must not fear death is discussed. Before directly approaching the theme, in the proem to Book I, Cicero presents his conception about philosophy and about the requirement of producing philosophy in Latin. Concerning its subject, the dialogue of Book 1 can be divided into two great parts: the first one consisting of an argumentation favourable to the immortality of the soul, that proves death is something good (18-71), and the second one, consisting of a reservation that death is not only something good, but it cannot be something bad (82-119). In accordance to the main goal of this work and based on several different translations which allowed us to do the work with a philological stance where necessary, and which guided a great part of our investigation through notes and valued suggestions of a secondary bibliography we analysed the first part of Book 1, showing that the argumentation in favour of the immortality of the soul, is according to Cicero, absolute and praiseworthy to the best philosophers. We also noticed that the immortality of the soul had been denied as an axiom of ancient philosophy by Hellenistic thought, such as Stoicism and Epicureanism. Cicero refuses the Stoic views about duration of the souls and despises the Epicurean concept on the proof of the mortality of the soul. There are four proofs of immortality of the soul in Book 1, in which we can find the following discussions: the argument consensus omnium gentium, the soul as warm air, the soul as the principle of movement and the soul as the fifth nature (quinta natura). For this work the last discussions are the most important ones: the discussion of the soul as a principle of movement, from Phaidro by Plato and the discussion of the soul as the fifth nature from the lost dialogues of Aristotle, by means of which, Cicero demonstrates that the soul is eternal and divine, thus, establishing a difference between the nature of the soul and the nature of the body. As it may be seen in the conclusion of this work, the immortality of the soul is restricted to the mind, a part of the soul, provided with reason. Remaining after death of the material body, the soul owns perception and intelligence, as it presents the same nature of god, thus pertaining to the celestial realms. / Esta dissertação tem como objetivo principal apresentar e discutir as provas da imortalidade da alma no Livro I das Discussões Tusculanas, de Cícero, uma obra filosófica escrita em forma de diálogo em que se discute, dentre outras coisas, por que o homem não deve temer a morte. Antes de abordar o tema de forma direta, Cícero apresenta no proêmio ao Livro I sua concepção acerca da filosofia e da necessidade de produzir filosofia em latim. Quanto a seu tema, o diálogo do Livro I pode ser dividido em dois grandes momentos: o primeiro consiste numa argumentação favorável à imortalidade da alma, que prova que a morte é um bem (parágrafos 18 a 71); e o segundo consiste na ressalva de que a morte não apenas é um bem, mas sequer pode ser um mal (parágrafos 82 a 119). Alinhados ao objetivo principal deste trabalho e munidos de diferentes traduções que nos permitiram o trabalho de cunho filológico, quando necessário, e nortearam, pelas notas e indicações de bibliografia secundária, grande parte de nossa pesquisa, analisamos a primeira parte do Livro I, mostrando que, para Cícero, a argumentação em favor da imortalidade da alma é primorosa e digna de filósofos superiores (Platão e Aristóteles). Constatamos, também, que a imortalidade da alma, como uma doutrina da filosofia antiga, havia sido negada pelas correntes helenistas, o estoicismo e o epicurismo. Cícero rejeita o ponto de vista do estoicismo sobre a duração das almas e despreza a prova da mortalidade de Epicuro. Quatro são as provas da imortalidade da alma encontradas no Livro I. Delas constam os seguintes argumentos: consensus omnium gentium, a alma como ar aquecido, a alma como princípio de movimento e a alma como quinta natureza. Para este trabalho, os dois últimos são de maior importância: o argumento da alma como princípio de movimento, extraído do diálogo Fedro, de Platão; e o argumento da alma como quinta natureza, noção retirada dos diálogos perdidos de Aristóteles, já que, com eles, Cícero demonstra que a alma é eterna e divina, estabelecendo uma diferença entre a natureza da alma e a natureza do corpo. Como poderá ser visto na conclusão, a imortalidade da alma restringe-se à mente, parte da alma provida de razão. Permanecendo após a morte do corpo, a alma possui percepção e é dotada de inteligência, tem a mesma natureza de deus e, assim, pertence à região celeste. / Mestre em Filosofia

Submitted by Jean Medeiros (jeanletras@uepb.edu.br) on 2017-12-05T12:03:24Z No. of bitstreams: 2 PDF - Anderson de Araújo Nascimento.pdf: 46622103 bytes, checksum: d60f09812020a13c3cb13ccf0c932c21 (MD5) Produto - Anderson de Araújo Nascimento.pdf: 2173471 bytes, checksum: a461965985df3647cd94256a818a4661 (MD5) / Approved for entry into archive by Secta BC (secta.csu.bc@uepb.edu.br) on 2017-12-06T18:38:49Z (GMT) No. of bitstreams: 2 PDF - Anderson de Araújo Nascimento.pdf: 46622103 bytes, checksum: d60f09812020a13c3cb13ccf0c932c21 (MD5) Produto - Anderson de Araújo Nascimento.pdf: 2173471 bytes, checksum: a461965985df3647cd94256a818a4661 (MD5) / Made available in DSpace on 2017-12-06T18:38:49Z (GMT). No. of bitstreams: 2 PDF - Anderson de Araújo Nascimento.pdf: 46622103 bytes, checksum: d60f09812020a13c3cb13ccf0c932c21 (MD5) Produto - Anderson de Araújo Nascimento.pdf: 2173471 bytes, checksum: a461965985df3647cd94256a818a4661 (MD5) Previous issue date: 2017-08-21 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - CAPES / The present research work investigated the level of geometric thinking and the types of mathematical proofs by 1st year high school students from the application of a Didactic Proposal. This research was constituted as a qualitative one, and as case study, having instruments of the application an essay with the theme Proofs and Mathematical Demonstrations, Didactic Proposal developed by a team of five members who worked collaboratively, inserted in the Project CAPES/OBEDUC/UFMS/UEPB/UFAL Edital 2012, participant observation and audio recording. We developed the didactic proposal with 18 activities, divided into four parts, which stimulated students to reflect, justify, prove and demonstrate. The application of this proposal occurred in June 2015 for 1st year high school students in a public school in the city of Areia, Paraíba. Our research took place in three moments. In the first moment, we apply the essay on the subject mathematical proofs and demonstrations. In the second moment we did a didactic intervention approaching definitions, theorems, proofs and mathematical demonstrations with the objective of taking to the students this knowledge. In the third moment, Part I and II of the Didactic Proposal were applied, involving activities to conjecture and demonstrate the Pythagorean Theorem, Internal Angle Sum Theorem and External Angle Theorem. This proposal helped in the investigation of the mathematical knowledge of the 1st year high school students, divided into 8 pairs and one trio, chosen freely. The two pairs of students who achieved the best performance in our Didactic Proposal were chosen for our case study and the one of better performance had its dialogue recorded and transcribed as a source of evidence of our case study. In our research we analyzed the answers given by the two pairs on Activities 1 and 3 (Part II) and Activity 2 (Part III), totaling in 3 questions. We used the data triangulation method for our case study. Firstly, we draw the profile of the two pairs of students in relation to Proofs and Mathematical Demonstrations. Next, we investigate the types of mathematical proofs used by them and their geometric thinking. To do so, we use discussions about the levels of geometric thinking proposed by Van Hiele and the types of evidence. From our results we can conclude that the pairs of students were able to develop informal justifications, that is, informal proofs. Thus, the pairs presented pragmatic evidence and the types of evidence Pragmatic Justification and Crucial Example. Regarding the geometric thinking proposed by Van Hiele, only one pair could be classified in one of the levels of development of geometric thinking, Level 3, informal deduction. Therefore, we come to the end of this research convinced that it is necessary to start working mathematical proofs and demonstrations in the basic education level, adapting its teaching to the degree of maturity and to the mathematical knowledge of the students, since our results point out that this subject is not approached properly in the classroom. / A presente pesquisa investigou o nível do pensamento geométrico e os tipos de provas matemáticas de alunos do 1º ano do Ensino Médio a partir da aplicação de uma Proposta Didática. Esta pesquisa se constituiu como qualitativa, e estudo de caso, tendo como instrumentos a aplicação de uma redação com o tema Provas e Demonstrações Matemáticas, Proposta Didática desenvolvida por uma equipe de cinco membros que trabalhou de forma colaborativa, inserida no Projeto CAPES/OBEDUC/UFMS/UEPB/ UFAL Edital 2012, observação participante e gravação em audio do diálgo de umas das duplas participantes da pesquisa. Elaboramos uma proposta didática com 18 atividades, dividida em quatro partes, que estimulavam aos alunos refletirem, justificarem, provarem e demonstrarem. A aplicação dessa proposta se deu em junho de 2015 para alunos do 1º ano do Ensino Médio de uma escola pública da cidade de Areia, Paraíba. Nossa pesquisa se deu em três momentos. No primeiro momento, aplicamos a redação sobre o tema provas e demonstrações matemáticas. No segundo momento realizamos uma intervenção didática abordando definições, teoremas, provas e demonstrações matemáticas com o objetivo de levar aos alunos esses conhecimentos. No terceiro momento foi aplicado a Parte I e II da Proposta Didática, envolvendo atividades de conjecturar e demonstrar o Teorema de Pitágoras, Teorema da Soma dos Ângulos Internos e Teorema dos Ângulo Externo. Essa proposta auxiliou na investigação do conhecimento matemático dos alunos do 1º ano do Ensino Médio, divididos em 8 duplas e um trio, escolhidos livremente. As duas duplas de alunos que obteveram melhores desempenhos em nossa Proposta Didática foram escolhidas para o nosso estudo de caso e a de melhor desenpenho teve seu diálogo gravado e transcrito como fonte de evidência de nosso estudo de caso. Em nossa pesquisa analisamos as respostas dadas pelas duas duplas sobre Atividades 1 e 3 (Parte II) e Atividade 2 (Parte III), totalizando em 3 questões. Utilizamos o método de triângulação de dados para nosso estudo de caso. Primeiramente, traçamos o perfil das duas duplas de alunas com relação às Provas e Demonstrações Matemáticas. Em seguida, investigamos os tipos de provas matemáticas utilizadas por elas e o seu pensamento geométrico. Para tanto, utilizamos as discussões sobre os níveis do pensamento geométrico proposto por Van Hiele e os tipos de provas. A partir de nossos resultados pudemos concluir que as duplas de alunas conseguiram desenvolver justificativas informais, ou seja, provas informais. Assim, as duplas apresentaram provas pragmáticas e os tipos de provas Justificativa Pragmática e Exemplo Crucial. Com relação ao pensamento geométrico proposto por Van Hiele, apenas uma dupla pôde ser classificada em um dos níveis de desenvolvimento do pensamento geométrico, o Nível 3, dedução informal. Portanto, chegamos ao final desta pesquisa convictos de que é preciso iniciar o trabalho das provas e demonstrações matemáticas na Educação Básica, adequando seu ensino ao grau de maturidade e aos conhecimentos matemáticos dos alunos, visto que nossos resultados apontam que esse tema não é abordado adequadamente em sala de aula.

Orientador: José Plínio de Oliveira Santos / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Matemática Estatística e Computação Científica / Made available in DSpace on 2018-08-25T04:32:08Z (GMT). No. of bitstreams: 1 BrasilJunior_NelsonGomes_M.pdf: 980636 bytes, checksum: dd8d61baeb633d5f598abc3523def800 (MD5) Previous issue date: 2014 / Resumo: Neste trabalho, estudamos a sequência dos Números de Catalan, uma sequência que aparece como solução de vários problemas de contagem envolvendo árvores, palavras, grafos e outras estruturas combinatórias. Atualmente, são conhecidas cerca de 200 interpretações combinatórias distintas para os Números de Catalan, o que motiva o estudo de relações entre estas interpretações, isto é, entre conjuntos cuja cardinalidade é dada pelos termos desta sequência. O principal objetivo do nosso trabalho é, portanto, mostrar bijeções entre esses conjuntos. No início do texto fazemos uma pequena introdução histórica aos números de Catalan, assim como definimos algumas formas de representar a sequência estudada. Depois mostramos algumas bijeções clássicas entre conjuntos contados pela sequência de Catalan. Além disso, apresentamos outras bijeções entre conjuntos envolvendo diversos objetos combinatórios. No total, são exibidas 29 bijeções / Abstract: In this work, we study the sequence of Catalan Numbers, which appears as a solution of many counting problems involving trees, words, graphs and other combinatorial structures. Nowadays, about 200 different combinatorial interpretations of the Catalan Numbers are known and that motivates the study between them, i. e., the study between sets whose cardinality is given by the terms of this sequence. The main objective of our work is therefore to show bijections between these sets. In the beginning, we make a short historical introduction of the Catalan Numbers and define some ways to represent the sequence. After that, we show some classical bijections between sets counted by the Catalan Numbers. Additionally, we exhibit other bijections between sets involving several combinatorial objects. Altogether, 29 bijections are presented / Mestrado / Matematica Aplicada / Mestre em Matemática Aplicada

Les méthodes formelles ont atteint un degré de maturité conduisant à la conception de systèmes de preuves généralistes, permettant à la fois de vérifier la correction de systèmes logiciels complexes ou de formaliser des mathématiques avancées. Mais souvent, l'accent est mis davantage sur la facilité du raisonnement sur les programmes plutôt que sur leur exécution efficace. L'antagonisme entre ces deux aspects est particulièrement sensible pour les algorithmes de calcul formel, dont la correction repose habituellement sur des concepts mathématiques élaborés, mais dont l'efficacité pratique est une préoccupation importante. Cette thèse développe des approches à l'étude formelle et l'exécution efficace de programmes en théorie des types, et plus précisément dans l'assistant à la preuve \coq{}. Dans un premier temps, nous présentons un environnement d'exécution permettant de compiler en code natif de tels programmes tout en conservant la généralité et l'expressivité du formalisme. Puis, nous nous intéressons aux représentations de données et plus particulièrement au lien formellement vérifié et automatisé entre représentations adaptées aux preuves ou au calcul. Ensuite, nous mettons à profit ces techniques pour l'étude d'algorithmes en algèbre linéaire, comme le produit matriciel de Strassen, le procédé d'élimination de Gauss ou la mise en forme canonique de matrices, dont notamment la forme de Smith pour les matrices sur un anneau euclidien. Enfin, nous ouvrons le champ des applications à la formalisation et au calcul certifié des groupes d'homologie de complexes simpliciaux issus d'images numériques. / Formal methods have reached a degree of maturity leading to the design of general-purpose proof systems, enabling both to verify the correctness of complex software systems and to formalize advanced mathematics. However, the ease of reasoning on programs is often emphasized more than their efficient execution. The antagonism between these two aspects is particularly significant for computer algebra algorithms, whose correctness usually relies on elaborate mathematical concepts, but whose practical efficiency is an important matter of concern. This thesis develops approaches to the formal study and the efficient execution of programs in type theory, and more precisely in the proof assistant \coq{}. In a first part, we introduce a runtime environment enabling the native code compilation of such programs while retaining the generality and expressiveness of the formalism. Then, we focus on data representations and in particular on the formally verified and automatized link between proof-oriented and computation-oriented representations. Then, we take advantage of these techniques to study linear algebra algorithms, like Strassen's matrix product, Gaussian elimination or matrix canonical forms, including the Smith normal form for matrices over a Euclidean ring. Finally, we open the field of applications to the formalization and certified computation of homology groups of simplicial complexes arising from digital images.

Exprimer le parallélisme dans la programmation de manière simple et performante est un défi auquel l'informatique fait face, en raison de l'évolution actuelle des architectures matérielles. BSML est un langage permettant une programmation parallèle de haut niveau, structurée, qui participe à cette recherche. En s'appuyant sur le coeur du langage existant, cette thèse propose d'une part des extensions qui en font un langage plus général et plus simple (traits impératifs tels que références et exceptions, syntaxe spécifique...) tout en conservant et étendant sa sûreté (sémantiques formelles, système de types...) et d'autre part une méthodologie de développement d'applications parallèles certifiées / Finding a good paradigm to represent parallel programming in a simple and efficient way is a challenge currently faced by computer science research, mainly due to the evolution of machine architectures towards multi-core processors. BSML is a high level, structured parallel programming language that takes part in the research in an original way. By building upon existing work, this thesis extends the language and makes it more general, simple and usable with added imperative features such as references and exceptions, a specific syntax, etc. The existing formal and safety characteristics of the language (semantics, type system...) are preserved and extended. A major application is given in the form of a methodology for the development of fully proved parallel programs

Cette thèse présente des résultats appartenant aux trois thèmes fondamentaux de la cryptographie à clé publique : l’intégrité, l’authentification et la confidentialité. Au sein de chaque thème nous concevons des nouvelles primitives et améliorons des primitives existantes. Le premier chapitre, dédié à l’intégrité, introduit une preuve non-interactive de génération appropriée de clés publiques RSA et un protocole de co-signature dans lequel tout irrespect de l’équité laisse automatiquement la partie lésée en possession d’une preuve de culpabilité incriminant la partie tricheuse. Le second chapitre, ayant pour sujet l’authentification, montre comme une mesure de temps permet de raccourcir les engagements dans des preuves à divulgation nulle et comment des biais, introduits à dessin dans le défi, permettent d’accroitre l’efficacité de protocoles. Ce chapitre généralise également le protocole de Fiat-Shamir à plusieurs prouveurs et décrit une fraude très sophistiquée de cartes-à-puce illustrant les dangers de protocoles d’authentification mal-conçus. Au troisième chapitre nous nous intéressons à la confidentialité. Nous y proposons un cryptosystème à clé publique où les hypothèses de complexité traditionnelles sont remplacées par un raffinement du concept de CAPTCHA et nous explorons l’application du chiffrement-pot-de-miel au langage naturel. Nos dernières contributions concernent le chiffrement basé sur l’identité (IBE). Nous montrerons comment ajouter des fonctions d’émission à l’IBE hiérarchique et comment l’IBE permet de réduire la fenêtre temporelle de risque lors de la diffusion de mises à jour logicielles. / This thesis presents new results in three fundamental areas of public-key cryptography: integrity, authentication and confidentiality. In each case we design new primitives or improve the features of existing ones. The first chapter, dealing with integrity, introduces a non-interactive proof for proper RSA public key generation and a contract co-signature protocol in which a breach in fairness provides the victim with transferable evidence against the cheater. The second chapter, focusing on authentication, shows how to use time measurements to shorten zeroknowledge commitments and how to exploit bias in zero-knowledge challenges to gain efficiency. This chapter also generalizes Fiat-Shamir into a one-to-many protocol and describes a very sophisticated smart card fraud illustrating what can happen when authentication protocols are wrongly designed. The third chapter is devoted to confidentiality. We propose public-key cryptosystems where traditional hardness assumptions are replaced by refinements of the CAPTCHA concept and explore the adaptation of honey encryption to natural language messages. Our final contributions focus on identity-based encryption (IBE) showing how to add broadcast features to hierarchical IBE and how to use IBE to reduce vulnerability exposure time of during software patch broadcast.

Dans la classe de complexité QMA – la généralisation quantique de la classe NP – un état quantique est fourni comme preuve à un algorithme de vérification pour l’aider à résoudre un problème. Cette classe de complexité a un problème complet naturel, le problème des Hamiltoniens locaux. Inspiré par la Physique de la matière condensée, ce problème concerne l’énergie de l’état fondamental d’un système quantique. Dans le cadre de cette thèse, nous étudions quelques problèmes liés à la classe QMA et au problème des Hamiltoniens locaux. Premièrement, nous étudions la différence de puissance si au lieu d’une preuve quantique, l’algorithme de vérification quantique reçoit une preuve classique. Nous proposons un cadre intermédiaire à ces deux cas, où la preuve consiste en un état quantique “plus simple” et nous arrivons à démontrer que ces états plus simples sont suffisants pour résoudre tous les problèmes dans QMA. À partir de ce résultat, nous obtenons un nouveau problème QMA-complet et nous étudions aussi la version de notre nouvelle classe de complexité avec erreur unilatérale. Ensuite, nous proposons le premier schéma de délégation vérifiable relativiste de calcul quantique. Dans ce cadre, un client classique délègue son calcul quantique à deux serveurs quantiques intriqués. Ces serveurs peuvent communiquer entre eux en respectant l’hypothèse que l’information ne peut pas être propagé plus vite que la vitesse de la lumière. Ce protocole a été conçu à partir d’un jeu non-local pour le problème des Hamiltoniens locaux avec deux prouveurs et un tour de communication. Dans ce jeu, les prouveurs exécutent des calculs quantiques de temps polynomiaux sur des copies de l’état fondamental du Hamiltonien. Finalement, nous étudions la conjecture PCP quantique, où l’on demande si tous les problèmes dans la classe QMA acceptent un système de preuves où l’algorithme de vérification a accès à un nombre constant de qubits de la preuve quantique. Notre première contribution consiste à étendre le modèle QPCP avec une preuve auxiliaire classique. Pour attaquer le problème, nous avons proposé une version plus faible de la conjecture QPCP pour ce nouveau système de preuves. Nous avons alors montré que cette nouvelle conjecture peut également être exprimée dans le contexte des problèmes des Hamiltoniens locaux et ainsi que dans lecadre de la maximisation de la probabilité de acceptation des jeux quantiques. Notre résultat montre la première équivalence entre un jeu multi-prouveur et une conjecture QPCP. / In QMA, the quantum generalization of the complexity class NP, a quantum state is provided as a proof of a mathematical statement, and this quantum proof can be verified by a quantum algorithm. This complexity class has a very natural complete problem, the Local Hamiltonian problem. Inspired by Condensed Matters Physics, this problem concerns the groundstate energy of quantum systems. In this thesis, we study some problems related to QMA and to the Local Hamiltonian problem. First, we study the difference of power when classical or quantum proofs are provided to quantum verification algorithms. We propose an intermediate setting where the proof is a “simpler” quantum state, and we manage to prove that these simpler states are enough to solve all problems in QMA. From this result, we are able to present a new QMA-complete problem and we also study the one-sided error version of our new complexity class. Secondly, we propose the first relativistic verifiable delegation scheme for quantum computation. In this setting, a classical client delegates her quantumcomputation to two entangled servers who are allowed to communicate, but respecting the assumption that information cannot be propagated faster than speed of light. This protocol is achieved through a one-round two-prover game for the Local Hamiltonian problem where provers only need polynomial time quantum computation and access to copies of the groundstate of the Hamiltonian. Finally, we study the quantumPCP conjecture, which asks if all problems in QMA accept aproof systemwhere only a fewqubits of the proof are checked. Our result consists in proposing an extension of QPCP proof systems where the verifier is also provided an auxiliary classical proof. Based on this proof system, we propose a weaker version of QPCP conjecture. We then show that this new conjecture can be formulated as a Local Hamiltonian problem and also as a problem involving the maximum acceptance probability of multi-prover games. This is the first equivalence of a multi-prover game and some QPCP statement.

Dans cette thèse, nous étudions les preuves à divulgation nulle de connaissance, une primitive cryptographique permettant de prouver une assertion en ne révélant rien de plus que sa véracité, et leurs applications au calcul sécurisé. Nous introduisons tout d’abord un nouveau type de preuves à divulgation nulle, appelées arguments implicites à divulgation nulle, intermédiaire entre deux notions existantes, les preuves interactives et les preuves non interactives à divulgation nulle. Cette nouvelle notion permet d’obtenir les mêmes bénéfices en terme d’efficacité que les preuves non-interactives dans le contexte de la construction de protocoles de calcul sécurisé faiblement interactifs, mais peut être instanciée à partir des mêmes hypothèses cryptographiques que les preuves interactives, permettant d’obtenir de meilleures garanties d’efficacité et de sécurité. Dans un second temps, nous revisitons un système de preuves à divulgation nulle de connaissance qui est particulièrement utile dans le cadre de protocoles de calcul sécurisé manipulant des nombres entiers, et nous démontrons que son analyse de sécurité classique peut être améliorée pour faire reposer ce système de preuve sur une hypothèse plus standard et mieux connue. Enfin, nous introduisons une nouvelle méthode de construction de systèmes de preuves à divulgation nulle sur les entiers, qui représente une amélioration par rapport aux méthodes existantes, tout particulièrement dans un modèle de type client-serveur, où un client à faible puissance de calcul participe à un protocole de calcul sécurisé avec un serveur à forte puissance de calcul. / In this thesis, we study zero-knowledge proofs, a cryptographic primitive that allows to prove a statement while yielding nothing beyond its truth, and their applications to secure computation. Specifically, we first introduce a new type of zero-knowledge proofs, called implicit zero-knowledge arguments, that stands between two existing notions, interactive zeroknowledge proofs and non-interactive zero-knowledge proofs. Our new notion provides the same efficiency benefits than the latter when used to design roundefficient secure computation protocols, but it can be built from essentially the same cryptographic assumptions than the former, which allows to get improved efficiency and security guarantees. Second, we revisit a zero-knowledge proof system that is particularly useful for secure computation protocols manipulating integers, and show that the known security analysis can be improved to base the proof system on a more wellstudied assumption. Eventually, we introduce a new method to build zero-knowledge proof systems over the integers, which particularly improves over existing methods in a client-server model, where a weak client executes a secure computation protocol with a powerful server.

Les programmes informatiques sont rarement écrits d'un seul coup, et sont au contraire composés de changements successifs. Il est également fréquent qu'un logiciel soit mis à jour après sa sortie initiale. De tels changements peuvent avoir lieu pour diverses raisons, comme l'ajout de fonctionnalités ou la correction de bugs. Il est en tout cas important d'être capable de représenter ces changements et de raisonner à leur propos pour s'assurer qu'ils implémentent les changements voulus.En pratique, les différences entre programmes sont très souvent représentées comme des différences textuelles sur le code source, listant les lignes de textes ajoutées, supprimées ou modifiées. Cette représentation, bien qu'exacte, ne dit rien de leurs conséquences sémantiques. Pour cette raison, il existe un besoin pour de meilleures représentations des différences sémantiques entre programmes.Notre première contribution est un algorithme de construction de programmes de corrélation, c'est-à-dire, des programmes entrelaçant les instructions de deux autres programmes de telle sorte qu'ils simulent leur sémantiques. Ces programmes de corrélation peuvent alors être analysés pour calculer une sur-approximation des différences sémantiques entre les deux programmes d'entrée. Ce travail est directement inspiré d'un article de Partush et Yahav, qui décrit un algorithme similaire, mais incorrect en présence de boucles avec des instructions `break` ou `continue`. Pour garantir la correction de notre algorithme, nous l'avons formalisé et prouvé à l'aide de l'assistant de preuve Coq.Notre seconde et plus importante contribution est un cadre formel permettant de décrire précisément et de formellement vérifier des différences sémantiques. Ce cadre, complètement formalisé en Coq, représente la différence entre deux programmes à l'aide d'un troisième programme que nous appelons oracle. Contrairement à un programme de corrélation, un oracle n'entrelace pas nécessairement les instructions des deux programmes à comparer, et peut « sauter » des calculs intermédiaires.Un tel oracle est généralement écrit dans un langage de programmation différent des programmes à comparer, ce qui permet de concevoir des langages d'oracles spécifiques à certaines classes de différences, capables de mettre en relation des programmes qui plantent avec des programmes qui s'exécutent correctement.Nous avons conçu de tels langages d'oracles pour couvrir un large éventail de différences sur un langage impératif jouet. Nous avons également prouvé que notre cadre est au moins aussi expressif que celui de la Logique Relationnelle de Hoare en encodant plusieurs variantes de cette dernière sous forme de langages d'oracles, prouvant leur correction dans la foulée. / Computer programs are rarely written in one fell swoop. Instead, they are written in a series of incremental changes.It is also frequent for software to get updated after its initial release. Such changes can occur for various reasons, such as adding features, fixing bugs, or improving performances for instance. It is therefore important to be able to represent and reason about those changes, making sure that they indeed implement the intended modifications.In practice, program differences are very commonly represented as textual differences between a pair of source files, listing text lines that have been deleted, inserted or modified. This representation, while exact, does not address the semantic implications of those textual changes. Therefore, there is a need for better representations of the semantics of program differences.Our first contribution is an algorithm for the construction of a correlating program, that is, a program interleaving the instructions of two input programs in such a way that it simulates theirsemantics. Further static analysis can be performed on such correlating programs to compute an over-approximation of the semantic differences between the two input programs. This work draws direct inspiration from an article by Partush and Yahav, that describes a correlating program construction algorithm which we show to be unsound on loops that include `break` or `continue`statements. To guarantee its soundness, our alternative algorithm is formalized and mechanically checked within the Coq proof assistant.Our second and most important contribution is a formal framework allowing to precisely describe and formally verify semantic changes.This framework, fully formalized in Coq, represents the difference between two programs by a third program called an oracle.Unlike a correlating program, such an oracle is not required to interleave instructions of the programs under comparison, and may “skip” intermediate computation steps. In fact, such an oracle is typically written in a different programming language than the programs it relates, which allows designing correlating oracle languages specific to certain classes of program differences, andcapable of relating crashing programs with non-crashing ones.We design such oracle languages to cover a wide range of program differences on a toy imperative language. We also prove that our framework is at least as expressive as Relational Hoare Logic by encoding several variants as correlating oracle languages, proving their soundness in the process.